Anzeige
Erschienen in:
2010 | OriginalPaper | Buchkapitel
Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis
verfasst von : Isil Dillig, Thomas Dillig, Alex Aiken
Erschienen in: Static Analysis
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
Static analysis techniques that represent program states as formulas typically generate a large number of redundant formulas that are incrementally constructed from previous formulas. In addition to querying satisfiability and validity, analyses perform other operations on formulas, such as quantifier elimination, substitution, and instantiation, most of which are highly sensitive to formula size. Thus, the scalability of many static analysis techniques requires controlling the size of the generated formulas throughout the analysis. In this paper, we present a practical algorithm for reducing SMT formulas to a
simplified form
containing no redundant subparts. We present experimental evidence that on-line simplification of formulas dramatically improves scalability.