Sciweavers

Share
FAC
2007

Are the Logical Foundations of Verifying Compiler Prototypes Matching user Expectations?

9 years 9 months ago
Are the Logical Foundations of Verifying Compiler Prototypes Matching user Expectations?
Abstract. The Verifying Compiler (VC) project proposals suggest that mainstream software developers are its targeted end-users. Like other software engineering efforts, the VC project success depends on appropriate end-user consultation. Industrial use of program assertions for the purpose of Run-time Assertion Checking (RAC) is becoming commonplace. A likely next step on the path to VC adoption is the use of assertions in Extended Static Checking (ESC), a fully automated form of Static Program Verification (SPV). Unfortunately, all current VC prototypes supporting SPV, adopt a semantics which is unsound relative to the standard run-time interpretation of assertions. In this article, we report on the results of a survey in which we asked industrial developers what logical semantics they want program assertions to have, and whether consistency across RAC and SPV tools is important. Survey results indicate that developers are in favor of a semantics for assertions that is compatible with...
Patrice Chalin
Added 14 Dec 2010
Updated 14 Dec 2010
Type Journal
Year 2007
Where FAC
Authors Patrice Chalin
Comments (0)
books