Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Lazy Annotation Revisited

Kenneth L. McMillan

Abstract

Lazy Annotation is a method of software model checking that performs a backtracking search for a symbolic counterexample. When the search backtracks, the program is annotated with a learned fact that constrains future search. In this sense, the method is closely analogous to conflict-driven clause learning in SAT solvers.

In this paper, we develop several improvements to the basic Lazy Annotation approach. The resulting algorithm is compared both conceptually and experimentally to two approaches based on similar principles but using different learning strategies: unfolding-based Bounded Model Checking and Property-Driven Reachability.

Details

Publication typeTechReport
NumberMSR-TR-2014-65
> Publications > Lazy Annotation Revisited