File(s) under permanent embargo
Safety verification and refutation by k-invariants and k-induction
conference contribution
posted on 2023-06-09, 00:30 authored by Martin Brain, Saurabh Joshi, Daniel Kroening, Peter SchrammelMost software verification tools can be classified into one of a number of established families, each of which has their own focus and strengths. For example, concrete counterexample generation in model checking, invariant inference in abstract interpretation and completeness via annotation for deductive verification. This creates a significant and fundamental usability problem as users may have to learn and use one technique to find potential problems but then need an entirely different one to show that they have been fixed. This paper presents a single, unified algorithm kIkI, which strictly generalises abstract interpretation, bounded model checking and k-induction. This not only combines the strengths of these techniques but allows them to interact and reinforce each other, giving a ‘single-tool’ approach to verification.
History
Publication status
- Published
File Version
- Published version
Journal
Static Analysis. SAS 2015ISSN
0302-9743Publisher
SpringerExternal DOI
Volume
9291Page range
145-161Pages
333.0Event name
Static Analysis Symposium, SAS 2015Event location
Saint-Maol, FranceEvent type
conferenceEvent date
9-11 September 2015Book title
Static analysis : 22nd International Symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015, ProceedingsISBN
9783662482872Series
Lecture Notes in Computer ScienceDepartment affiliated with
- Informatics Publications
Full text available
- No
Peer reviewed?
- Yes
Editors
Thomas Jensen, Sandrine BlazyLegacy Posted Date
2016-05-09First Compliant Deposit (FCD) Date
2016-05-09Usage metrics
Categories
No categories selectedLicence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC