Satisfiability checking: theory and applications

DOI10.1007/978-3-319-41591-8_2MaRDI QIDQ4571125zbMATH OpenOpenAlexFDO

Authors Erika Ábrahám, Gereon Kremer

Publication date 6 July 2018

Published in Software Engineering and Formal Methods (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-41591-8_2

Mathematics Subject Classification ID

Recommendations

• A Tutorial on Satisfiability Modulo Theories
• Satisfiability modulo theories
• Computer Aided Verification
• Foundations of satisfiability modulo theories
• A survey of satisfiability modulo theory

Cites work

• \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
• A Computing Procedure for Quantification Theory
• A Decision Procedure for Bit-Vectors and Arrays
• A machine program for theorem-proving
• Building bridges between symbolic computation and satisfiability checking
• Computer Aided Verification
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• GRASP: a search algorithm for propositional satisfiability
• scientific article; zbMATH DE number 3177183 (Why is no real title available?)
• scientific article; zbMATH DE number 3497890 (Why is no real title available?)
• scientific article; zbMATH DE number 1157666 (Why is no real title available?)
• scientific article; zbMATH DE number 5263038 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• Interval-based relaxation for general numeric planning
• Nagoya termination tool
• Program synthesis using dual interpretation
• Proving termination of programs automatically with AProVE
• Quantifier elimination for real algebra -- the quadratic case and beyond
• raSAT: An SMT Solver for Polynomial Constraints
• SAT-Based Model Checking without Unrolling
• Simplification by Cooperating Decision Procedures
• SMT-based analysis of virtually synchronous distributed hybrid systems
• Solving non-linear arithmetic
• Symbolic optimization with SMT solvers
• The MathSAT5 SMT solver
• The strategy challenge in SMT solving

Cited in

(19)

• Simplification in a satisfiability checker for VLSI applications
• Satisfiability modulo bounded checking
• \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
• Building bridges between symbolic computation and satisfiability checking
• MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
• Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver
• Taking satisfiability to the next level with Z3 (abstract)
• scientific article; zbMATH DE number 6528599 (Why is no real title available?)
• Beyond satisfiability: extensions and applications
• Satisfiability modulo theories: an appetizer
• scientific article; zbMATH DE number 1241716 (Why is no real title available?)
• Testing satisfiability
• Satisfiability: where Theory meets Practice (Invited Talk).
• The problem of checking the satisfiability of formulae of decidable theories (survey)
• Satisfiability checking and symbolic computation
• A Tutorial on Satisfiability Modulo Theories
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• Computer Aided Verification
• Satisfiability Checking of Non-clausal Formulas Using General Matings

Describes a project that uses

Uses Software

• SMTInterpol
• SYMBA
• z3
• Tyrolean
• CBMC
• Azure

This page was built for publication: Satisfiability checking: theory and applications

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