Skip to Main content Skip to Navigation
New interface
Conference papers

On Quantitative Software Verification

Abstract : Software verification has made great progress in recent years, resulting in several tools capable of working directly from source code, for example, SLAM and Astree. Typical properties that can be verified are expressed as Boolean assertions or temporal logic properties, and include whether the program eventually terminates, or the executions never violate a safety property. The underlying techniques crucially rely on the ability to extract from programs, using compiler tools and predicate abstraction, finite-state abstract models, which are then iteratively refined to either demonstrate the violation of a safety property (e.g. a buffer overflow) or guarantee the absence of such faults. An established method to achieve this automatically executes an abstraction-refinement loop guided by counterexample traces [1].
Document type :
Conference papers
Complete list of metadata

Cited literature [4 references]  Display  Hide  Download
Contributor : Brigitte Briot Connect in order to contact the contributor
Submitted on : Thursday, February 18, 2010 - 1:26:36 PM
Last modification on : Tuesday, September 8, 2020 - 4:58:02 PM
Long-term archiving on: : Friday, June 18, 2010 - 9:18:35 PM


Files produced by the author(s)




Marta Kwiatkowska. On Quantitative Software Verification. SPIN 2009 : Model Checking Software, 16th International SPIN Workshop, Jun 2009, Grenoble, France. pp.2-3, ⟨10.1007/978-3-642-02652-2⟩. ⟨inria-00457746⟩



Record views


Files downloads