The MathSAT5 SMT solver
From MaRDI portal
Publication:5326318
DOI10.1007/978-3-642-36742-7_7zbMATH Open1381.68153DBLPconf/tacas/CimattiGSS13OpenAlexW221832247WikidataQ62041183 ScholiaQ62041183MaRDI QIDQ5326318FDOQ5326318
Authors: Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, 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
Recommendations
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Specification and verification (program logics, model checking, etc.) (68Q60)
Cited In (87)
- Mind the gap: bit-vector interpolation recast over linear integer arithmetic
- Safe decomposition of startup requirements: verification and synthesis
- Translation-based approaches for solving disjunctive temporal problems with preferences
- Analysis and Transformation of Constrained Horn Clauses for Program Verification
- Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test
- Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs
- Title not available (Why is that?)
- SMT sampling via model-guided approximation
- SAT meets tableaux for linear temporal logic satisfiability
- Local Search For Satisfiability Modulo Integer Arithmetic Theories
- Abstraction refinement and antichains for trace inclusion of infinite state systems
- Craig interpolation with clausal first-order tableaux
- Local Search for SMT on Linear Integer Arithmetic
- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
- Abstraction Modulo Stability for Reverse Engineering
- Enhancing SMT-based weighted model integration by structure awareness
- Analysis of cyclic fault propagation via ASP
- A conflict-driven solving procedure for poly-power constraints
- Bitwuzla
- Local search for solving satisfiability of polynomial formulas
- Commutativity for concurrent program termination proofs
- MDPs as distribution transformers: affine invariant synthesis for safety objectives
- Satisfiability modulo finite fields
- A complete and terminating approach to linear integer solving
- Modular strategic SMT solving with \textbf{SMT-RAT}
- Encoding RTL constructs for \textsc{MathSAT}: a preliminary report
- Flexible proof production in an industrial-strength SMT solver
- \textsc{LTL} falsification in infinite-state systems
- \textsc{OptiMathSAT}: a tool for optimization modulo theories
- Automatic discovery of fair paths in infinite-state transition systems
- Optimization modulo non-linear arithmetic via incremental linearization
- Causality-based game solving
- Implicit semi-algebraic abstraction for polynomial dynamical systems
- Title not available (Why is that?)
- SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
- Optimization modulo theories with linear rational costs
- Embedding equality constraints of optimization problems into a quantum annealer
- Deductive verification of floating-point Java programs in KeY
- Syntax-guided synthesis for lemma generation in hardware model checking
- Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
- The map equality domain
- Strong temporal planning with uncontrollable durations
- Parallelizing SMT solving: lazy decomposition and conciliation
- A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
- Search-space partitioning for parallelizing SMT solvers
- An extension of lazy abstraction with interpolation for programs with arrays
- Deciding floating-point logic with abstract conflict driven clause learning
- OpenSMT2: an SMT solver for multi-core and cloud computing
- Counterexample-guided prophecy for model checking modulo the theory of arrays
- Algorithmic reduction of biological networks with multiple time scales
- Certifying proofs for SAT-based model checking
- An SMT theory of fixed-point arithmetic
- SPASS-SATT. A CDCL(LA) solver
- Incremental design-space model checking via reusable reachable state approximations
- Automated verification and synthesis of stochastic hybrid systems: a survey
- Verification Modulo theories
- Diagnosability of fair transition systems
- Deciding Bit-Vector Formulas with mcSAT
- An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty
- MathSAT5
- Satisfiability checking: theory and applications
- Satisfiability modulo theories
- Solving linear optimization over arithmetic constraint formula
- Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
- Proving correctness of imperative programs by linearizing constrained Horn clauses
- M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures
- An approximation framework for solvers and decision procedures
- New techniques for linear arithmetic: cubes and equalities
- Propagation based local search for bit-precise reasoning
- Advanced SMT techniques for weighted model integration
- Infinite-state invariant checking with IC3 and predicate abstraction
- Fast cube tests for LIA constraint solving
- What you always wanted to know about model checking of fault-tolerant distributed algorithms
- 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
- Correct approximation of IEEE 754 floating-point arithmetic for program verification
- Sharpening constraint programming approaches for bit-vector theory
- Verification of SMT systems with quantifiers
- \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
- Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas
- \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
- Formal reliability analysis of redundancy architectures
- Smt-Switch: a solver-agnostic C++ API for SMT solving
- Solving strong controllability of temporal problems with uncertainty using SMT
- Removing algebraic data types from constrained Horn clauses using difference predicates
- Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
- Symbolic trajectory evaluation for word-level verification: theory and implementation
Uses Software
This page was built for publication: The MathSAT5 SMT solver
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5326318)
