Safety verification and refutation by k-invariants and k-induction

Brain, Martin, Joshi, Saurabh, Kroening, Daniel and Schrammel, Peter (2015) Safety verification and refutation by k-invariants and k-induction. Static Analysis Symposium, SAS 2015, Saint-Maol, France, 9-11 September 2015. Published in: Blazy, Sandrine and Jensen, Thomas, (eds.) Static Analysis. SAS 2015. 9291 145-161. Springer ISSN 0302-9743 ISBN 9783662482872

[img] PDF (For REF only) - Published Version
Restricted to SRO admin only

Download (416kB)

Abstract

Most 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.

Item Type: Conference Proceedings
Keywords: verification, bounded model checking, k-induction, abstract interpretation
Schools and Departments: School of Engineering and Informatics > Informatics
Subjects: Q Science > QA Mathematics > QA0075 Electronic computers. Computer science
Depositing User: Peter Schrammel
Date Deposited: 09 May 2016 05:47
Last Modified: 08 Mar 2021 15:41
URI: http://sro.sussex.ac.uk/id/eprint/59918

View download statistics for this item

📧 Request an update