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