MathSAT5

swMATH9569MaRDI QIDQ21550FDOQ21550

Author name not available (Why is that?)

Described by source

• The MathSAT5 SMT Solver

Cited In (70)

• Translation-based approaches for solving disjunctive temporal problems with preferences
• Abstraction refinement and antichains for trace inclusion of infinite state systems
• Craig interpolation with clausal first-order tableaux
• Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic
• Safe Decomposition of Startup Requirements: Verification and Synthesis
• Reducing crash recoverability to reachability
• Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
• Analysis of cyclic fault propagation via ASP
• A complete and terminating approach to linear integer solving
• Modular strategic SMT solving with \textbf{SMT-RAT}
• Fast Cube Tests for LIA Constraint Solving
• Proving the Incompatibility of Efficiency and Strategyproofness via SMT Solving
• 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
• What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms
• Title not available (Why is that?)
• $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation
• Building bridges between symbolic computation and satisfiability checking
• A Modular Approach to MaxSAT Modulo Theories
• Embedding equality constraints of optimization problems into a quantum annealer
• Deductive verification of floating-point Java programs in KeY
• SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
• Strong temporal planning with uncontrollable durations
• Parallelizing SMT solving: lazy decomposition and conciliation
• Fairness modulo theory: a new approach to LTL software model checking
• An extension of lazy abstraction with interpolation for programs with arrays
• Deciding floating-point logic with abstract conflict driven clause learning
• Algorithmic reduction of biological networks with multiple time scales
• Certifying proofs for SAT-based model checking
• An SMT theory of fixed-point arithmetic
• Cutting the mix
• 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
• Diagnosability of fair transition systems
• Deciding Bit-Vector Formulas with mcSAT
• A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic
• An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty
• Solving linear optimization over arithmetic constraint formula
• SMT-Solvers in Action: Encoding and Solving Selected Problems in NP and EXPTIME
• Positive solutions of systems of signed parametric polynomial inequalities
• A reduction from unbounded linear mixed arithmetic problems into bounded problems
• Exploring approximations for floating-point arithmetic using UppSAT
• Search-Space Partitioning for Parallelizing SMT Solvers
• Title not available (Why is that?)
• Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
• Proving correctness of imperative programs by linearizing constrained Horn clauses
• An approximation framework for solvers and decision procedures
• New techniques for linear arithmetic: cubes and equalities
• Propagation based local search for bit-precise reasoning
• Infinite-state invariant checking with IC3 and predicate abstraction
• A conflict-driven solving procedure for poly-power constraints
• 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
• Satisfiability Modulo Theories
• Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas
• Formal reliability analysis of redundancy architectures
• Decision procedures. An algorithmic point of view
• 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

This page was built for software: MathSAT5