Conference
Analysis of Invariants for Efficient Bounded Verification
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 error is exhibited. Code involving linked data structures with intricate invariants is particularly hard to analyze using these techniques. In this article we present TACO, a …
Authors
Galeotti JP; Rosner N; López Pombo CG; Frias MF
Series
ISSTA ’10
Pagination
pp. 25-36
Publisher
ACM
Publication Date
2010
ISBN-13
9781605588230
DOI
10.1145/1831708.1831712
Conference proceedings
Proceedings of the 19th International Symposium on Software Testing and Analysis