Satisfiability Procedures for Combination of Theories Sharing Integer Offsets

DOI10.1007/978-3-642-00768-2_35zbMath1234.68262OpenAlexW1539567407MaRDI QIDQ3617773

Enrica Nicolini, Michaël Rusinowitch, Christophe Ringeissen

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) Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05)

Related Items

Modularity results for interpolation, amalgamation and superamalgamation, SMT-based verification of data-aware processes: a model-theoretic approach, Combinable Extensions of Abelian Groups, Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes), Model completeness, covers and superposition, Data Structures with Arithmetic Constraints: A Non-disjoint Combination

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Model-theoretic methods in combined constraint satisfiability
• A rewriting approach to satisfiability procedures.
• Efficient theory combination via Boolean search
• Combining Satisfiability Procedures for Unions of Theories with a Shared Counting Operator
• Noetherianity and Combination Problems
• Automatic Decidability and Combinability Revisited
• Deciding Combinations of Theories
• Simplification by Cooperating Decision Procedures
• A comprehensive combination framework
• New results on rewrite-based satisfiability procedures
• Theoretical Aspects of Computing – ICTAC 2005
• On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
• A Gröbner Basis Approach to CNF-Formulae Preprocessing