Sciweavers

ICSE
2007
IEEE-ACM

A Sound Assertion Semantics for the Dependable Systems Evolution Verifying Compiler

14 years 3 months ago
A Sound Assertion Semantics for the Dependable Systems Evolution Verifying Compiler
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, one of the most fully developed VC prototypes. Preliminary results demonstrate the effectiveness of the new semantics at uncovering previously...
Patrice Chalin
Added 09 Dec 2009
Updated 09 Dec 2009
Type Conference
Year 2007
Where ICSE
Authors Patrice Chalin
Comments (0)