Journal article
TACO: Efficient SAT-Based Bounded Verification Using Symmetry Breaking and Tight Bounds
Abstract
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 failure is exhibited. Code involving linked data structures with intricate invariants is particularly hard to analyze using these techniques. In this paper, we present …
Authors
Galeotti JP; Rosner N; Pombo CGL; Frias MF
Journal
IEEE Transactions on Software Engineering, Vol. 39, No. 9, pp. 1283–1307
Publisher
Institute of Electrical and Electronics Engineers (IEEE)
DOI
10.1109/tse.2013.15
ISSN
0098-5589