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]


Research Interests