Analysis of invariants for efficient bounded verification
Juan Pablo Galeotti, Nicolás Rosner, Carlos G. López Pombo, Marcelo Fabian Frias · 2010
SAT-based bounded verification of annotated code consists of translating the code together with the annotations to a propositional formula, and analyzing the formula for specification violations using a SAT-solver. If a violation is found, an execution trace exposing the error is exhibited. Code involving linked data structures with intricate invariants is particularly hard to analyze using these techniques.