Data structures with arithmetic constraints: A non-disjoint combination

DOI10.1007/978-3-642-04222-5_20MaRDI QIDQ3655209zbMATH OpenOpenAlexFDO

Authors Enrica Nicolini, Christophe Ringeissen, 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

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

Recommendations

• Combining satisfiability procedures for unions of theories with a shared counting operator
• Combining nonstably infinite theories
• A polite non-disjoint combination method: theories with bridging functions revisited
• Unions of non-disjoint theories and combinations of satisfiability procedures
• Combining decision procedures.

Cites work

• A canonical form for generalized linear constraints
• A comprehensive combination framework
• A rewriting approach to satisfiability procedures.
• Automatic Decidability and Combinability Revisited
• Combinable Extensions of Abelian Groups
• Deciding Combinations of Theories
• Engineering DPLL(T) + Saturation
• scientific article; zbMATH DE number 3467028 (Why is no real title available?)
• Model-theoretic methods in combined constraint satisfiability
• New results on rewrite-based satisfiability procedures
• On Fourier's algorithm for linear arithmetic constraints
• On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
• Paramodulation-based theorem proving
• Satisfiability Procedures for Combination of Theories Sharing Integer Offsets
• 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)
• Modularity results for interpolation, amalgamation and superamalgamation
• A rewriting approach to the combination of data structures with bridging theories
• Combining satisfiability procedures for unions of theories with a shared counting operator
• Modular termination and combinability for superposition modulo counter arithmetic
• On deciding satisfiability by theorem proving with speculative inferences
• SMT-based verification of data-aware processes: a model-theoretic approach
• Automated Reasoning
• DNN verification, reachability, and the exponential function problem

This page was built for publication: Data structures with arithmetic constraints: A non-disjoint combination

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