MathSAT5
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Beaver
- Boolector
- CoCoALib
- CPBPV
- MetiTarski
- iRankFinder
- Sally
- Btor2Tools
- BtorMC
- Pono
- Smt-Switch
- SDSAT
- Paradox
- SMT-LIB
- ECCE
- REDLOG
- Yices
- Solving linear optimization over arithmetic constraint formula
- SATIRE
- UCLID
- New techniques for linear arithmetic: cubes and equalities
- Propagation based local search for bit-precise reasoning
- Cutting the mix
- Fairness modulo theory: a new approach to LTL software model checking
- z3
- Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas
- Strong temporal planning with uncontrollable durations
- Parallelizing SMT solving: lazy decomposition and conciliation
- Orbital library
- libpoly
- 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
- COMICS
- GiNaCRA
- Princess
- E-SETHEO
- dReal
- veriT
- SMTInterpol
- Ultimate Automizer
- CPAchecker
- KRATOS
- SPNP
- Embedding equality constraints of optimization problems into a quantum annealer
- Sharpening constraint programming approaches for bit-vector theory
- CLSAT
- OpenSMT
- Algorithmic reduction of biological networks with multiple time scales
- SYMBA
- Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
- Certifying proofs for SAT-based model checking
- 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
- 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
- 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
- CVC4
- 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
- Cleaneling
- NuSMV3
- Ocelot
- Cumapz
- Eldarica
- TeMP
- Deductive verification of floating-point Java programs in KeY
- A conflict-driven solving procedure for poly-power constraints
- \textsc{OptiMathSAT}: a tool for optimization modulo theories
- SPASS-SATT. A CDCL(LA) solver
- A complete and terminating approach to linear integer solving
- Translation-based approaches for solving disjunctive temporal problems with preferences
- CSIsat
- Solving strong controllability of temporal problems with uncertainty using SMT
- An approximation framework for solvers and decision procedures
- Infinite-state invariant checking with IC3 and predicate abstraction
- SIMPLY
- Mcmt
- Skeptik
- Modular strategic SMT solving with \textbf{SMT-RAT}
- DFTCalc
- TopDeg
- FOCI
- CCASat
- ANML
- SMT-RAT
- CArL
- Cubicle
- Wolverine
- TRP++
- Craig interpolation with clausal first-order tableaux
- RATSY
- Analysis of cyclic fault propagation via ASP
- raSAT
This page was built for software: MathSAT5
