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
|