The MathSAT5 SMT Solver
From MaRDI portal
Publication:5326318
DOI10.1007/978-3-642-36742-7_7zbMath1381.68153OpenAlexW221832247WikidataQ62041183 ScholiaQ62041183MaRDI QIDQ5326318
Bastiaan Joost Schaafsma, Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
Publication date: 5 August 2013
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-36742-7_7
Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
Related Items
An approximation framework for solvers and decision procedures ⋮ Infinite-state invariant checking with IC3 and predicate abstraction ⋮ Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic ⋮ Safe Decomposition of Startup Requirements: Verification and Synthesis ⋮ Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays ⋮ Optimization modulo non-linear arithmetic via incremental linearization ⋮ Implicit semi-algebraic abstraction for polynomial dynamical systems ⋮ Causality-based game solving ⋮ The map equality domain ⋮ SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving ⋮ Search-Space Partitioning for Parallelizing SMT Solvers ⋮ Satisfiability Modulo Theories ⋮ What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms ⋮ Automatic discovery of fair paths in infinite-state transition systems ⋮ Incremental design-space model checking via reusable reachable state approximations ⋮ Correct approximation of IEEE 754 floating-point arithmetic for program verification ⋮ Diagnosability of fair transition systems ⋮ Satisfiability Checking: Theory and Applications ⋮ Solving linear optimization over arithmetic constraint formula ⋮ Craig interpolation with clausal first-order tableaux ⋮ Optimization Modulo Theories with Linear Rational Costs ⋮ Modular strategic SMT solving with \textbf{SMT-RAT} ⋮ Verification Modulo theories ⋮ An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ New techniques for linear arithmetic: cubes and equalities ⋮ Propagation based local search for bit-precise reasoning ⋮ Proving correctness of imperative programs by linearizing constrained Horn clauses ⋮ Local Search For Satisfiability Modulo Integer Arithmetic Theories ⋮ Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test ⋮ Verification of SMT systems with quantifiers ⋮ SMT sampling via model-guided approximation ⋮ Analysis of cyclic fault propagation via ASP ⋮ Unnamed Item ⋮ Unnamed Item ⋮ An extension of lazy abstraction with interpolation for programs with arrays ⋮ Deciding floating-point logic with abstract conflict driven clause learning ⋮ Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas ⋮ Formal reliability analysis of redundancy architectures ⋮ Deductive verification of floating-point Java programs in KeY ⋮ Syntax-guided synthesis for lemma generation in hardware model checking ⋮ Strong temporal planning with uncontrollable durations ⋮ Parallelizing SMT solving: lazy decomposition and conciliation ⋮ Symbolic trajectory evaluation for word-level verification: theory and implementation ⋮ Embedding equality constraints of optimization problems into a quantum annealer ⋮ Sharpening constraint programming approaches for bit-vector theory ⋮ Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions ⋮ Counterexample-guided prophecy for model checking modulo the theory of arrays ⋮ Abstraction refinement and antichains for trace inclusion of infinite state systems ⋮ Algorithmic reduction of biological networks with multiple time scales ⋮ A conflict-driven solving procedure for poly-power constraints ⋮ \textsc{OptiMathSAT}: a tool for optimization modulo theories ⋮ $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation ⋮ Fast Cube Tests for LIA Constraint Solving ⋮ Deciding Bit-Vector Formulas with mcSAT ⋮ SPASS-SATT. A CDCL(LA) solver ⋮ Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic ⋮ Certifying proofs for SAT-based model checking ⋮ A complete and terminating approach to linear integer solving ⋮ MathSAT5 ⋮ A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic ⋮ Advanced SMT techniques for weighted model integration ⋮ New records of pre-image search of reduced SHA-1 using SAT solvers ⋮ Compositional construction of control barrier functions for continuous-time stochastic hybrid systems ⋮ Translation-based approaches for solving disjunctive temporal problems with preferences ⋮ An SMT theory of fixed-point arithmetic ⋮ Removing algebraic data types from constrained Horn clauses using difference predicates ⋮ Automated verification and synthesis of stochastic hybrid systems: a survey ⋮ Solving strong controllability of temporal problems with uncertainty using SMT ⋮ Flexible proof production in an industrial-strength SMT solver ⋮ Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description) ⋮ \textsc{LTL} falsification in infinite-state systems ⋮ Smt-Switch: a solver-agnostic C++ API for SMT solving
Uses Software
This page was built for publication: The MathSAT5 SMT Solver
