Safety Verification and Refutation by k-Invariants and k-Induction

Conference/Journal
Springer
Authors
Martin Brain Saurabh Joshi Daniel Kroening
BibTex
Abstract
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 ...