CVC Lite

swMATH7581MaRDI QIDQ19608FDOQ19608

Author name not available (Why is that?)

Cited In (51)

• Tools and Algorithms for the Construction and Analysis of Systems
• 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
• 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
• Automatic Refinement of Split Binary Semaphore
• The RISC ProofNavigator: a proving assistant for program verification in the classroom
• A randomized satisfiability procedure for arithmetic and uninterpreted function symbols
• Extending Sledgehammer with SMT Solvers
• Equality detection for linear arithmetic constraints
• Theorem proving for classical logic with partial functions by reduction to Kleene logic
• Highly Automated Formal Proofs over Memory Usage of Assembly Code
• 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
• 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
• Verification of clock synchronization algorithms: experiments on a combination of deductive tools
• Cooperating theorem provers: a case study combining HOL-Light and CVC Lite
• Modular SMT Proofs for Fast Reflexive Checking Inside Coq
• 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
• Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL
• 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
• Combining Theories with Shared Set Operations
• Title not available (Why is that?)

This page was built for software: CVC Lite