MathSAT5
From MaRDI portal
Software:21550
No author found.
Related Items (70)
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 ⋮ Optimization modulo non-linear arithmetic via incremental linearization ⋮ Implicit semi-algebraic abstraction for polynomial dynamical systems ⋮ Causality-based game solving ⋮ 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 ⋮ Proving the Incompatibility of Efficiency and Strategyproofness via SMT Solving ⋮ A Modular Approach to MaxSAT Modulo Theories ⋮ Solving linear optimization over arithmetic constraint formula ⋮ Craig interpolation with clausal first-order tableaux ⋮ Modular strategic SMT solving with \textbf{SMT-RAT} ⋮ An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty ⋮ 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 ⋮ Cutting the mix ⋮ Fairness modulo theory: a new approach to LTL software model checking ⋮ Analysis of cyclic fault propagation via ASP ⋮ Unnamed Item ⋮ Unnamed Item ⋮ SMT-Solvers in Action: Encoding and Solving Selected Problems in NP and EXPTIME ⋮ 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 ⋮ Strong temporal planning with uncontrollable durations ⋮ Parallelizing SMT solving: lazy decomposition and conciliation ⋮ Decision procedures. An algorithmic point of view ⋮ 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 ⋮ Positive solutions of systems of signed parametric polynomial inequalities ⋮ Exploring approximations for floating-point arithmetic using UppSAT ⋮ A reduction from unbounded linear mixed arithmetic problems into bounded problems ⋮ 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 ⋮ Building Bridges between Symbolic Computation and Satisfiability Checking ⋮ 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 ⋮ Reducing crash recoverability to reachability ⋮ A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic ⋮ 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 ⋮ Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages ⋮ 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
This page was built for software: MathSAT5
