The following pages link to CVC Lite (Q19608):
Displaying 34 items.
- Strategies for scalable symbolic execution-driven test generation for programs (Q350939) (← links)
- Proceedings of the 3rd workshop on pragmatics of decision procedures in automated reasoning (PDPAR 2005), Edinburgh, UK, July12, 2005 (Q368046) (← links)
- Decision procedures. An algorithmic point of view (Q518892) (← links)
- Equality detection for linear arithmetic constraints (Q621462) (← links)
- Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005) (Q861691) (← links)
- Deciding Boolean algebra with Presburger arithmetic (Q861705) (← links)
- The SAT-based approach to separation logic (Q862390) (← links)
- Applying SAT solving in classification of finite algebras (Q862393) (← links)
- M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures (Q862395) (← links)
- Automatic construction and verification of isotopy invariants (Q928664) (← links)
- Efficiently checking propositional refutations in HOL theorem provers (Q1006729) (← links)
- The RISC ProofNavigator: a proving assistant for program verification in the classroom (Q1019024) (← links)
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis (Q1037399) (← links)
- Extending Sledgehammer with SMT solvers (Q2351158) (← links)
- Efficient theory combination via Boolean search (Q2432765) (← links)
- Processes and continuous change in a SAT-based planner (Q2457662) (← links)
- A randomized satisfiability procedure for arithmetic and uninterpreted function symbols (Q2486581) (← links)
- Embedded software verification using symbolic execution and uninterpreted functions (Q2506297) (← links)
- Verification of clock synchronization algorithms: experiments on a combination of deductive tools (Q2642981) (← links)
- Predicate diagrams for the verification of real-time systems (Q2642985) (← links)
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler (Q2655335) (← links)
- (Q2848688) (← links)
- (Q2848691) (← links)
- Rewrite-Based Decision Procedures (Q2864358) (← links)
- Bounded Model Checking with Parametric Data Structures (Q2864380) (← links)
- Mothers of Pipelines (Q2864521) (← links)
- An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types (Q2864522) (← links)
- Distributing the Workload in a Lazy Theorem-Prover (Q2870323) (← links)
- versat: A Verified Modern SAT Solver (Q2891429) (← links)
- Theorem proving for classical logic with partial functions by reduction to Kleene logic (Q2987064) (← links)
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses (Q3100209) (← links)
- Modular SMT Proofs for Fast Reflexive Checking Inside Coq (Q3100210) (← links)
- Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL (Q3100212) (← links)
- Hammering towards QED (Q5195271) (← links)
