scientific article; zbMATH DE number 1979549

MaRDI QIDQ4427902zbMATH OpenFDO

Authors Ofer Strichman

Publication date 14 September 2003

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2517/25170160.htm

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• On satisfiability problems with a linear structure
• A practical approach to satisfiability modulo linear integer arithmetic
• Computer Aided Verification
• On Some SAT-Variants over Linear Formulas
• A theory of satisfiability-preserving proofs in SAT solving
• SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
• scientific article; zbMATH DE number 2090300
• SAT modulo linear arithmetic for solving polynomial constraints
• Linear satisfiability preserving assignments
• Theory and Applications of Satisfiability Testing

Cited in

(22)

• Efficiently checking propositional refutations in HOL theorem provers
• A framework for satisfiability modulo theories
• Zero, successor and equality in BDDs
• Solving the resolution-free SAT problem by submodel propagation in linear time
• A reduction from unbounded linear mixed arithmetic problems into bounded problems
• Efficient theory combination via Boolean search
• Combining preorder and postorder resolution in a satisfiability solver
• Presburger arithmetic in memory access optimization for data-parallel languages
• Satisfiability modulo theories
• Linear Arithmetic with Stars
• On the Satisfiability of Modular Arithmetic Formulae
• A Pearl on SAT Solving in Prolog
• Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
• Effective Quantifier Elimination for Presburger Arithmetic with Infinity
• scientific article; zbMATH DE number 1903355 (Why is no real title available?)
• Classical logic, classical probability, and quantum mechanics
• Integrated and automated abstract interpretation, verification and testing of C/C++ modules
• Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
• Computer Aided Verification
• Synthesising programs with non-trivial constants
• Solving \(\mathrm{LIA}^\star\) using approximations
• M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures

Describes a project that uses

Uses Software

• Chaff

This page was built for publication:

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