|
Research
|
|
|
Incremental Verification
|
Verifying a program as a whole is hard. However, programs do not
appear out of nowhere --- they are developed in small, incremental steps.
Incremental verification techniques exploit this fact.
The concepts underpinning incremental verification
are differential analysis and incremental solving
of sequences of logical formulae.
The following publications show that constructing and solving
verification problems incrementally is advantageous with respect to
performance:
Peter Schrammel, Daniel Kroening, Martin Brain, Ruben Martins,
Tino Teige, Tom Bienmüller. Successful Use of Incremental BMC
in Automotive Industry. In Formal Methods for Industrial Critical Systems, FMICS'15, Vol. 9128 of LNCS, pp. 62-77, Springer, 2015.
[bibtex]
[link]
[website]
Martin Brain, Saurabh Joshi, Daniel Kroening, Peter Schrammel. Safety Verification and Refutation by k-Invariants and k-Induction. In Static Analysis, SAS'15, Vol. 9291 of LNCS, pp. 145-161, Springer, 2015.
[bibtex]
[link]
[website]
|
|
|
|
Peter Schrammel
|
|
|
|
|
|
|
|