King's College London

Research portal

Theory Refinement for Program Verification

Research output: Chapter in Book/Report/Conference proceedingConference paper

Antti Hyyvarinen, Sepideh Asadi, Karine Even Mendoza, Grigory Fedyukovich, Hana Chockler, Natasha Sharygina

Original languageEnglish
Title of host publication 20th International Conference on Theory and Applications of Satisfiability Testing (SAT)
PublisherSpringer
Pages347-363
Volume10491
ISBN (Electronic) 978-3-319-66263-3
ISBN (Print)978-3-319-66262-6
DOIs
Publication statusE-pub ahead of print - 9 Aug 2017

Documents

  • main

    main.pdf, 457 KB, application/pdf

    25/09/2017

King's Authors

Abstract

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.
\emph{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.

Download statistics

No data available

View graph of relations

© 2018 King's College London | Strand | London WC2R 2LS | England | United Kingdom | Tel +44 (0)20 7836 5454