Recent progress in automated formal verification is to a large degree due to the development of constraint languages that are sufficiently light-weight for reasoning but still expressive enough to prove properties of programs. Satisfiability modulo theories (SMT) solvers implement efficient decision procedures, but offer little direct support for adapting the constraint language to the task at hand. Theory refinement is a new approach that modularly adjusts the modeling precision based on the properties being verified through the use of combination of theories. We implement the approach using an augmented version of the theory of bit-vectors and uninterpreted functions capable of directly injecting non-clausal refinements to the inherent Boolean structure of SMT. In our comparison to a state-of-the-art model checker, our prototype implementation is in general competitive, being several orders of magnitudes faster on some instances that are challenging for flattening, while computing models that are significantly more succinct.
CITATION STYLE
Hyvärinen, A. E. J., Asadi, S., Even-Mendoza, K., Fedyukovich, G., Chockler, H., & Sharygina, N. (2017). Theory refinement for program verification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10491 LNCS, pp. 347–363). Springer Verlag. https://doi.org/10.1007/978-3-319-66263-3_22
Mendeley helps you to discover research relevant for your work.