Anzeige
Erschienen in:
2012 | OriginalPaper | Buchkapitel
A Solver for Reachability Modulo Theories
verfasst von : Akash Lal, Shaz Qadeer, Shuvendu K. Lahiri
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Consider a sequential programming language with control flow constructs such as assignments, choice, loops, and procedure calls. We restrict the syntax of expressions in this language to one that can be efficiently decided by a satisfiability-modulo-theories solver. For such a language, we define the problem of deciding whether a program can reach a particular control location as the reachability-modulo-theories problem. This paper describes the architecture of
Corral
, a semi-algorithm for the reachability-modulo-theories problem.
Corral
uses novel algorithms for inlining procedures on demand (Stratified Inlining) and abstraction refinement (Hierarchical Refinement). The paper also presents an evaluation of
Corral
against other related tools.
Corral
consistently outperforms its competitors on most benchmarks.