Engineering a Sound Assertion Semantics for the Verifying Compiler

10 years 11 months ago
Engineering a Sound Assertion Semantics for the 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. For decades there have been debates concerning the most appropriate semantics for program assertions. Our contribution here is unique in that we have applied fundamental software engineering techniques by asking primar...
Patrice Chalin
Added 31 Jan 2011
Updated 31 Jan 2011
Type Journal
Year 2010
Where TSE
Authors Patrice Chalin
Comments (0)