Combined Satisfiability Modulo Parametric Theories

DOI10.1007/978-3-540-71209-1_47MaRDI QIDQ5758134zbMATH OpenOpenAlexFDO

Authors Sava Krstić, Amit Goel, Jim Grundy, Cesare Tinelli

Publication date 3 September 2007

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-71209-1_47

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Computer Aided Verification
• Satisfiability modulo theories
• A survey of satisfiability modulo theory
• Combining Decision Procedures by (Model-)Equality Propagation
• Automatic decidability and combinability

Cited in

(22)

• Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
• Combination of convex theories: modularity, deduction completeness, and explanation
• Datatypes with shared selectors
• Politeness and stable infiniteness: stronger together
• Polite combination of algebraic datatypes
• Politeness for the theory of algebraic datatypes
• Metalevel algorithms for variant satisfiability
• Satisfiability on mixed instances
• Metalevel algorithms for variant satisfiability
• Sets with cardinality constraints in satisfiability modulo theories
• Satisfiability modulo theories
• Verifying Heap-Manipulating Programs in an SMT Framework
• Combining theories with shared set operations
• Building a calculus of data structures
• Variant-Based Satisfiability in Initial Algebras
• Theories, solvers and static analysis by abstract interpretation
• Automatic decidability and combinability
• Computer Aided Verification
• Combining stable infiniteness and (strong) politeness
• Combining combination properties. I: Nelson-Oppen and politeness
• Being polite is not enough (and other limits of theory combination)
• Satisfiability of mixed Horn formulas

This page was built for publication: Combined Satisfiability Modulo Parametric Theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5758134)