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