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
• Interpolating Quantifier-Free Presburger Arithmetic
• eVolCheck: Incremental Upgrade Checker for C
• SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
• Fairness modulo theory: a new approach to LTL software model checking
• An interpolating sequent calculus for quantifier-free Presburger arithmetic
• An extension of lazy abstraction with interpolation for programs with arrays
• Integration of an LP Solver into Interval Constraint Propagation
• Improved Single Pass Algorithms for Resolution Proof Reduction
• dReal: An SMT Solver for Nonlinear Theories over the Reals
• δ-Complete Decision Procedures for Satisfiability over the Reals
• An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty
• OpenSMT2: An SMT Solver for Multi-core and Cloud Computing
• Search-Space Partitioning for Parallelizing SMT Solvers
• Simulating circuit-level simplifications on CNF
• Propagation based local search for bit-precise reasoning
• Reasoning about algebraic data types with abstractions
• Challenging SMT solvers to verify neural networks
• I-RiSC: An SMT-Compliant Solver for the Existential Fragment of Real Algebra
• Quantifier-free interpolation of a theory of arrays
• Automating Theorem Proving with SMT
• A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints
• Satisfiability Modulo Theories
• Solving strong controllability of temporal problems with uncertainty using SMT
• Rewriting-based Quantifier-free Interpolation for a Theory of Arrays.

This page was built for software: OpenSMT