Skip to Main content Skip to Navigation
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 metadatas

Cited literature [4 references]  Display  Hide  Download

https://hal.inria.fr/inria-00457746
Contributor : Brigitte Briot <>
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

File

spin09.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

110

Files downloads

256