Data Structures with Arithmetic Constraints: A Non-disjoint Combination

DOI10.1007/978-3-642-04222-5_20zbMath1193.68090OpenAlexW1716633099MaRDI QIDQ3655209

Christophe Ringeissen, Enrica Nicolini, Michaël Rusinowitch

Publication date: 7 January 2010

Published in: Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/inria-00397080/file/RR-6963.pdf

Mathematics Subject Classification ID

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

Related Items

Modular Termination and Combinability for Superposition Modulo Counter Arithmetic ⋮ Modularity results for interpolation, amalgamation and superamalgamation ⋮ On deciding satisfiability by theorem proving with speculative inferences ⋮ SMT-based verification of data-aware processes: a model-theoretic approach ⋮ Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)

Cites Work

• Unnamed Item
• Unnamed Item
• Model-theoretic methods in combined constraint satisfiability
• On Fourier's algorithm for linear arithmetic constraints
• A canonical form for generalized linear constraints
• A rewriting approach to satisfiability procedures.
• Engineering DPLL(T) + Saturation
• Automatic Decidability and Combinability Revisited
• Satisfiability Procedures for Combination of Theories Sharing Integer Offsets
• Deciding Combinations of Theories
• Simplification by Cooperating Decision Procedures
• Combinable Extensions of Abelian Groups
• 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