OpenSMT
From MaRDI portal
Cited in
(55)- Beaver
- Boolector
- BtorMC
- Pono
- Propagation based local search for bit-precise reasoning
- Reasoning about algebraic data types with abstractions
- Fairness modulo theory: a new approach to LTL software model checking
- FunFrog
- GiNaCRA
- Princess
- PeRIPLO
- TLAPS
- MathSAT5
- eVolCheck
- CSIsat
- Solving strong controllability of temporal problems with uncertainty using SMT
- MUP
- Mcmt
- CMU Benchmarks
- AMUSE
- SATLIB Benchmark Suite
- FOCI
- SMT-RAT
- CArL
- I-RiSC
- OpenSMT2: an SMT solver for multi-core and cloud computing
- Building bridges between symbolic computation and satisfiability checking
- Quantifier-free interpolation of a theory of arrays
- -complete decision procedures for satisfiability over the reals
- I-RiSC: an SMT-compliant solver for the existential fragment of real algebra
- OpenSMT2
- Challenging SMT solvers to verify neural networks
- A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints
- Satisfiability modulo theories
- RADA
- EUREKA
- \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
- Search-space partitioning for parallelizing SMT solvers
- Ultimate
- LTLAutomizer
- FuncTion
- Simulating circuit-level simplifications on CNF
- Guardol
- iSAT
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- Improved single pass algorithms for resolution proof reduction
- Resolution proof transformation for compression and interpolation
- An extension of lazy abstraction with interpolation for programs with arrays
- dReal: an SMT solver for nonlinear theories over the reals
- Interpolating quantifier-free Presburger arithmetic
- Integration of an LP solver into interval constraint propagation
- eVolCheck: incremental upgrade checker for C
- Automating theorem proving with SMT
- Rewriting-based quantifier-free interpolation for a theory of arrays
- An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty
This page was built for software: OpenSMT