Safety verification and refutation by k-invariants and k-induction
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 dedu...
| Main Authors: | , , , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Springer Berlin Heidelberg
2015
|
| _version_ | 1797107968079036416 |
|---|---|
| author | Brain, M Joshi, S Kroening, D Schrammel, P |
| author_facet | Brain, M Joshi, S Kroening, D Schrammel, P |
| author_sort | Brain, M |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-07T07:22:56Z |
| format | Conference item |
| id | oxford-uuid:755c64c5-fe70-4b5e-beaf-4757ec76cefd |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T07:22:56Z |
| publishDate | 2015 |
| publisher | Springer Berlin Heidelberg |
| record_format | dspace |
| spelling | oxford-uuid:755c64c5-fe70-4b5e-beaf-4757ec76cefd2022-10-28T10:12:01ZSafety verification and refutation by k-invariants and k-inductionConference itemhttp://purl.org/coar/resource_type/c_5794uuid:755c64c5-fe70-4b5e-beaf-4757ec76cefdEnglishSymplectic Elements at OxfordSpringer Berlin Heidelberg2015Brain, MJoshi, SKroening, DSchrammel, PMost 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. |
| spellingShingle | Brain, M Joshi, S Kroening, D Schrammel, P Safety verification and refutation by k-invariants and k-induction |
| title | Safety verification and refutation by k-invariants and k-induction |
| title_full | Safety verification and refutation by k-invariants and k-induction |
| title_fullStr | Safety verification and refutation by k-invariants and k-induction |
| title_full_unstemmed | Safety verification and refutation by k-invariants and k-induction |
| title_short | Safety verification and refutation by k-invariants and k-induction |
| title_sort | safety verification and refutation by k invariants and k induction |
| work_keys_str_mv | AT brainm safetyverificationandrefutationbykinvariantsandkinduction AT joshis safetyverificationandrefutationbykinvariantsandkinduction AT kroeningd safetyverificationandrefutationbykinvariantsandkinduction AT schrammelp safetyverificationandrefutationbykinvariantsandkinduction |