swMATH4886MaRDI QIDQ17038FDOQ17038
Author name not available (Why is that?)
Official website: http://www.cs.nyu.edu/acsys/cvc3/
Cited In (only showing first 100 items - show all)
- Title not available (Why is that?)
- Extending Sledgehammer with SMT solvers
- Minimal counterexamples for linear-time probabilistic verification
- Towards Automatic Stability Analysis for Rely-Guarantee Proofs
- SMELS: Satisfiability Modulo Equality with Lazy Superposition
- An experiment with satisfiability modulo SAT
- Rewriting Induction + Linear Arithmetic = Decision Procedure
- New results on rewrite-based satisfiability procedures
- Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis
- SAT modulo linear arithmetic for solving polynomial constraints
- The complexity of reversal-bounded model-checking
- iProver-Eq: An Instantiation-Based Theorem Prover with Equality
- Expressing polymorphic types in a many-sorted language
- Lazy satisfiability modulo theories
- A FORMAL SYSTEM FOR EUCLID’SELEMENTS
- Computing small unsatisfiable cores in satisfiability modulo theories
- Cuts from proofs: a complete and practical technique for solving linear inequalities over integers
- Solving quantified verification conditions using satisfiability modulo theories
- A formal semantics of extended hierarchical state transition matrices using CSP\#
- Don't care words with an application to the automata-based approach for real addition
- Behavioral interface specification languages
- A unified framework for DPLL(T) + certificates
- Efficiently solving quantified bit-vector formulas
- Abstract domains for automated reasoning about list-manipulating programs with infinite data
- GNT
- HOL-Boogie
- ACSL
- SMT-LIB
- Caduceus
- Why3
- Yices
- Alt-Ergo
- Gappa
- ISP
- UCLID
- SIMPLIFY
- TASS_
- z3
- COMICS
- GiNaCRA
- FADAlib
- Zap
- ESC4
- TaPAS
- Title not available (Why is that?)
- Collective assertions
- Verification conditions for source-level imperative programs
- CVC Lite
- CLSAT
- Interproc
- CVC
- MathSAT
- DiPro
- HighSpec
- CVT
- VeriCool
- Monotonox
- CSIsat
- MUP
- Jahob
- RSat
- I-RiSC
- Combining theories with shared set operations
- Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
- LASH
- LIRA
- H-PILoT
- KLEE-FP
- Nemerle
- Robbins Conjecture
- STP
- Satisfiability modulo theories
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
- Challenges in Satisfiability Modulo Theories
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- Extending Sledgehammer with SMT solvers
- SMT proof checking using a logical framework
- Multi-prover verification of floating-point programs
- Cooperating theorem provers: a case study combining HOL-Light and CVC Lite
- Model-based theory combination
- E-matching for fun and profit
- Satisfiability solving and model generation for quantified first-order logic formulas
- Dafny: an automatic program verifier for functional correctness
- Automatic proof and disproof in Isabelle/HOL
- Conflict Resolution
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- TASS: the toolkit for accurate scientific software
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
- Heaps and Data Structures: A Challenge for Automated Provers
- Verifying Whiley programs with Boogie
- Being careful about theory combination
- checkbashisms
- Formal analysis of the compact position reporting algorithm
- SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
- Automating theorem proving with SMT
- Volume Computation for Boolean Combination of Linear Arithmetic Constraints
- Formal proof of SCHUR conjugate function
- The strategy challenge in SMT solving
This page was built for software: cvc3
