OpenSMT

swMATH8426MaRDI QIDQ20435FDOQ20435

Author name not available (Why is that?)

Cited In (26)

• 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
• An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty
• I-RiSC: an SMT-compliant solver for the existential fragment of real algebra
• 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
• 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
• 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