The following pages link to CVC4 (Q21467):
Displaying 50 items.
- Extensional higher-order paramodulation in Leo-III (Q2666959) (← links)
- A process calculus for privacy-preserving protocols in location-based service systems (Q2669244) (← links)
- Towards more efficient methods for solving regular-expression heavy string constraints (Q2680985) (← links)
- Polyhedral Approximation of Multivariate Polynomials Using Handelman’s Theorem (Q2796046) (← links)
- $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation (Q2817292) (← links)
- A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT (Q2817912) (← links)
- Congruence Closure in Intensional Type Theory (Q2817913) (← links)
- Fast Cube Tests for LIA Constraint Solving (Q2817914) (← links)
- Model Finding for Recursive Functions in SMT (Q2817915) (← links)
- Effective Normalization Techniques for HOL (Q2817937) (← links)
- Translating Scala Programs to Isabelle/HOL (Q2817953) (← links)
- Deciding Bit-Vector Formulas with mcSAT (Q2818018) (← links)
- Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams (Q2818019) (← links)
- Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers (Q2818024) (← links)
- Building bridges between symbolic computation and satisfiability checking (Q2819729) (← links)
- A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic (Q2830009) (← links)
- Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages (Q2849482) (← links)
- Two Decades of Maude (Q2945709) (← links)
- Matching Multiplications in Bit-Vector Formulas (Q2961559) (← links)
- Solving Nonlinear Integer Arithmetic with MCSAT (Q2961575) (← links)
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic (Q2961583) (← links)
- Satisfiability Modulo Theories (Q3176369) (← links)
- Chain-Free String Constraints (Q3297597) (← links)
- Synthesis of distributed algorithms with parameterized threshold guards (Q3300835) (← links)
- Counterexample-Guided Model Synthesis (Q3303898) (← links)
- Congruence Closure with Free Variables (Q3303931) (← links)
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP (Q3453107) (← links)
- TIP: Tons of Inductive Problems (Q3453129) (← links)
- SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving (Q3453240) (← links)
- Search-Space Partitioning for Parallelizing SMT Solvers (Q3453241) (← links)
- A Decision Procedure for (Co)datatypes in SMT Solvers (Q3454092) (← links)
- Beagle – A Hierarchic Superposition Theorem Prover (Q3454107) (← links)
- MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers (Q3454125) (← links)
- Integrating Simplex with Tableaux (Q3455763) (← links)
- Extensional Crisis and Proving Identity (Q3457789) (← links)
- TIP: Tools for Inductive Provers (Q3460056) (← links)
- (Q4553283) (← links)
- SMT-Solvers in Action: Encoding and Solving Selected Problems in NP and EXPTIME (Q4621226) (← links)
- One Logic to Use Them All (Q4928425) (← links)
- Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers (Q4972164) (← links)
- (Q5020652) (← links)
- Verifying Catamorphism-Based Contracts using Constrained Horn Clauses (Q5038461) (← links)
- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays (Q5043584) (← links)
- Computing Parameterized Invariants of Parameterized Petri Nets (Q5044400) (← links)
- Set Constraints, Pattern Match Analysis, and SMT (Q5098738) (← links)
- On Symbolic Heaps Modulo Permission Theories (Q5136317) (← links)
- The CADE-27 Automated theorem proving System Competition – CASC-27 (Q5145460) (← links)
- Verifying and Synthesizing Software with Recursive Functions (Q5167727) (← links)
- (Q5219923) (← links)
- Loop Analysis by Quantification over Iterations (Q5222968) (← links)
