Satisfiability Procedures for Combination of Theories Sharing Integer Offsets

DOI10.1007/978-3-642-00768-2_35MaRDI QIDQ3617773zbMATH OpenOpenAlexFDO

Authors Enrica Nicolini, Christophe Ringeissen, Michaël Rusinowitch

Publication date 31 March 2009

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-642-00768-2_35

Mathematics Subject Classification ID

Logic in computer science (03B70) Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Unions of non-disjoint theories and combinations of satisfiability procedures
• scientific article; zbMATH DE number 1140674
• Model-theoretic methods in combined constraint satisfiability
• Combining satisfiability procedures for unions of theories with a shared counting operator
• Theory combination: beyond equality sharing

Cites work

• A comprehensive combination framework
• A Gröbner Basis Approach to CNF-Formulae Preprocessing
• A rewriting approach to satisfiability procedures.
• Automatic Decidability and Combinability Revisited
• Combining satisfiability procedures for unions of theories with a shared counting operator
• Deciding Combinations of Theories
• Efficient theory combination via Boolean search
• scientific article; zbMATH DE number 3467028 (Why is no real title available?)
• scientific article; zbMATH DE number 1903346 (Why is no real title available?)
• scientific article; zbMATH DE number 5194318 (Why is no real title available?)
• Model-theoretic methods in combined constraint satisfiability
• New results on rewrite-based satisfiability procedures
• Noetherianity and Combination Problems
• On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
• Paramodulation-based theorem proving
• Simplification by Cooperating Decision Procedures
• Theoretical Aspects of Computing – ICTAC 2005

Cited in

(9)

• Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)
• Model completeness, covers and superposition
• Modularity results for interpolation, amalgamation and superamalgamation
• Satisfiability on mixed instances
• Combining satisfiability procedures for unions of theories with a shared counting operator
• Data structures with arithmetic constraints: A non-disjoint combination
• SMT-based verification of data-aware processes: a model-theoretic approach
• Combinable Extensions of Abelian Groups
• Theoretical Aspects of Computing – ICTAC 2005

This page was built for publication: Satisfiability Procedures for Combination of Theories Sharing Integer Offsets

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