DocumentCode :
2744786
Title :
A Sound Assertion Semantics for the Dependable Systems Evolution Verifying Compiler
Author :
Chalin, Patrice
Author_Institution :
Dependable Software Res. Group, Concordia Univ., Montreal, QC
fYear :
2007
fDate :
20-26 May 2007
Firstpage :
23
Lastpage :
33
Abstract :
The verifying compiler (VC) project is a core component of the dependable systems evolution grand challenge. The VC offers the promise of automatically proving that a program or component is correct, where correctness is defined by program assertions. While several VC prototypes exist, all adopt a semantics for assertions that is unsound. This paper presents a consolidation of VC requirements analysis activities that, in particular, brought us to ask targeted VC customers what kind of semantics they wanted. Taking into account both practitioners´ needs and current technological factors, we offer recovery of soundness through an adjusted definition of assertion validity that matches user expectations and can be implemented practically using current prover technology. We describe how support for the new semantics has been added to ESC/Java2. Preliminary results demonstrate the effectiveness of the new semantics at uncovering previously indiscernible specification errors.
Keywords :
program compilers; program verification; dependable systems evolution; requirements analysis; sound assertion semantics; verifying compiler project; Costs; Error correction; Java; Performance analysis; Prototypes; Runtime; Software engineering; Software prototyping; Software tools; Virtual colonoscopy;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Software Engineering, 2007. ICSE 2007. 29th International Conference on
Conference_Location :
Minneapolis, MN
ISSN :
0270-5257
Print_ISBN :
0-7695-2828-7
Type :
conf
DOI :
10.1109/ICSE.2007.9
Filename :
4222565
Link To Document :
بازگشت