Cited in
(only showing first 100 items - show all)- Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis
- Lazy satisfiability modulo theories
- Verification conditions for source-level imperative programs
- Cooperating theorem provers: a case study combining HOL-Light and CVC Lite
- Extending Sledgehammer with SMT solvers
- A FORMAL SYSTEM FOR EUCLID’SELEMENTS
- Dafny: an automatic program verifier for functional correctness
- Towards Automatic Stability Analysis for Rely-Guarantee Proofs
- Efficiently solving quantified bit-vector formulas
- Conflict Resolution
- Behavioral interface specification languages
- Model-based theory combination
- Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
- SAT modulo linear arithmetic for solving polynomial constraints
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- An experiment with satisfiability modulo SAT
- Solving quantified verification conditions using satisfiability modulo theories
- Rewriting Induction + Linear Arithmetic = Decision Procedure
- Abstract domains for automated reasoning about list-manipulating programs with infinite data
- The complexity of reversal-bounded model-checking
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- E-matching for fun and profit
- Minimal counterexamples for linear-time probabilistic verification
- A formal semantics of extended hierarchical state transition matrices using CSP\#
- Automatic proof and disproof in Isabelle/HOL
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- New results on rewrite-based satisfiability procedures
- Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
- Combining theories with shared set operations
- Challenges in Satisfiability Modulo Theories
- Beaver
- Cocktail
- GNT
- HOL-Boogie
- BarcelogicTools
- TVOC
- SCHUR
- KRAKATOA
- ACSL
- LiQuor
- SMT-LIB
- Caduceus
- Why3
- Yices
- Alt-Ergo
- Gappa
- ISP
- UCLID
- SIMPLIFY
- TASS_
- z3
- COMICS
- GiNaCRA
- FADAlib
- Zap
- ESC4
- TaPAS
- CVC Lite
- CLSAT
- Interproc
- CVC
- MathSAT
- DiPro
- HighSpec
- CVT
- VeriCool
- Monotonox
- CSIsat
- MUP
- Jahob
- RSat
- I-RiSC
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- LASH
- LIRA
- H-PILoT
- KLEE-FP
- Nemerle
- Robbins Conjecture
- STP
- SMT proof checking using a logical framework
- TASS: the toolkit for accurate scientific software
- Multi-prover verification of floating-point programs
- Don't care words with an application to the automata-based approach for real addition
- iProver-Eq: An Instantiation-Based Theorem Prover with Equality
- A unified framework for DPLL(T) + certificates
- Expressing polymorphic types in a many-sorted language
- Extending Sledgehammer with SMT solvers
- scientific article; zbMATH DE number 5613976 (Why is no real title available?)
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
- Cuts from proofs: a complete and practical technique for solving linear inequalities over integers
- Computing small unsatisfiable cores in satisfiability modulo theories
- Satisfiability modulo theories
- Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis
- Translation validation of loop optimizations and software pipelining in the TVOC framework. In memory of Amir Pnueli
- SMELS: satisfiability modulo equality with lazy superposition
- The TPTP typed first-order form with arithmetic
- checkbashisms
- Trusting computations: a mechanized proof from partial differential equations to actual program
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
This page was built for software: cvc3
