swMATH7581MaRDI QIDQ19608FDOQ19608
Author name not available (Why is that?)
Official website: http://www.cs.nyu.edu/acsys/cvc3/
Cited In (80)
- Tools and Algorithms for the Construction and Analysis of Systems
- Automatic Refinement of Split Binary Semaphore
- Highly automated formal proofs over memory usage of assembly code
- Extending Sledgehammer with SMT solvers
- Scalable fine-grained proofs for formula processing
- Computer Aided Verification
- An abstract decision procedure for satisfiability in the theory of recursive data types
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Efficient theory combination via Boolean search
- Term Rewriting and Applications
- Automatic construction and verification of isotopy invariants
- Mining propositional simplification proofs for small validating clauses
- New results on rewrite-based satisfiability procedures
- Automated Deduction – CADE-20
- Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)
- Applying SAT solving in classification of finite algebras
- The SAT-based approach to separation logic
- Processes and continuous change in a SAT-based planner
- Classification results in quasigroup and loop theory via a combination of automated reasoning tools.
- Fast LCF-Style Proof Reconstruction for Z3
- Automatic Construction and Verification of Isotopy Invariants
- Predicate diagrams for the verification of real-time systems
- Efficiently checking propositional refutations in HOL theorem provers
- Rocket-Fast Proof Checking for SMT Solvers
- The RISC ProofNavigator: a proving assistant for program verification in the classroom
- A randomized satisfiability procedure for arithmetic and uninterpreted function symbols
- Modular SMT proofs for fast reflexive checking inside Coq
- HOL-Boogie
- QOCA
- Prosper
- cvc3
- UCLID
- zChaff
- Zap
- Eclat
- veriT
- CVC
- MathSAT
- Gandalf
- Dixit
- Equality detection for linear arithmetic constraints
- RSat
- Combining theories with shared set operations
- Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
- ICS
- SAPA
- Geo 2007F
- ModGen
- TSAT++
- C32SAT
- QAGen
- Zapato
- Calife
- clock synchronization
- Psyche
- Schneider clock synchronization
- Robbins Conjecture
- Theorem proving for classical logic with partial functions by reduction to Kleene logic
- Deciding Boolean algebra with Presburger arithmetic
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
- Model Checking Recursive Programs with Exact Predicate Abstraction
- Embedded software verification using symbolic execution and uninterpreted functions
- Cassowary
- Strategies for scalable symbolic execution-driven test generation for programs
- Programming Languages and Systems
- M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures
- Extending Sledgehammer with SMT solvers
- Goeland
- Verification of clock synchronization algorithms: experiments on a combination of deductive tools
- Cooperating theorem provers: a case study combining HOL-Light and CVC Lite
- Proceedings of the 3rd workshop on pragmatics of decision procedures in automated reasoning (PDPAR 2005), Edinburgh, UK, July12, 2005
- Rewrite-based decision procedures
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- Bounded model checking with parametric data structures
- Mothers of pipelines
- Distributing the workload in a lazy theorem-prover
- Title not available (Why is that?)
- Decision procedures. An algorithmic point of view
- Hammering towards QED
- versat: A Verified Modern SAT Solver
This page was built for software: CVC Lite
