CVC Lite
From MaRDI portal
Software:19608
No author found.
Related Items (51)
New results on rewrite-based satisfiability procedures ⋮ versat: A Verified Modern SAT Solver ⋮ Unnamed Item ⋮ Tools and Algorithms for the Construction and Analysis of Systems ⋮ Verification of clock synchronization algorithms: experiments on a combination of deductive tools ⋮ Predicate diagrams for the verification of real-time systems ⋮ Unnamed Item ⋮ Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005) ⋮ Deciding Boolean algebra with Presburger arithmetic ⋮ The SAT-based approach to separation logic ⋮ Applying SAT solving in classification of finite algebras ⋮ M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures ⋮ Strategies for scalable symbolic execution-driven test generation for programs ⋮ HOL-Boogie -- an interactive prover-backend for the verifying C compiler ⋮ Proceedings of the 3rd workshop on pragmatics of decision procedures in automated reasoning (PDPAR 2005), Edinburgh, UK, July12, 2005 ⋮ Equality detection for linear arithmetic constraints ⋮ Efficient theory combination via Boolean search ⋮ Automatic Refinement of Split Binary Semaphore ⋮ Theorem proving for classical logic with partial functions by reduction to Kleene logic ⋮ Model Checking Recursive Programs with Exact Predicate Abstraction ⋮ Automatic construction and verification of isotopy invariants ⋮ Processes and continuous change in a SAT-based planner ⋮ Automated Deduction – CADE-20 ⋮ Term Rewriting and Applications ⋮ Decision procedures. An algorithmic point of view ⋮ Programming Languages and Systems ⋮ Highly Automated Formal Proofs over Memory Usage of Assembly Code ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A randomized satisfiability procedure for arithmetic and uninterpreted function symbols ⋮ Fast LCF-Style Proof Reconstruction for Z3 ⋮ Embedded software verification using symbolic execution and uninterpreted functions ⋮ Extending Sledgehammer with SMT Solvers ⋮ Automatic Construction and Verification of Isotopy Invariants ⋮ Rocket-Fast Proof Checking for SMT Solvers ⋮ Efficiently checking propositional refutations in HOL theorem provers ⋮ Scalable fine-grained proofs for formula processing ⋮ The RISC ProofNavigator: a proving assistant for program verification in the classroom ⋮ A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses ⋮ Modular SMT Proofs for Fast Reflexive Checking Inside Coq ⋮ Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL ⋮ Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis ⋮ Combining Theories with Shared Set Operations ⋮ Computer Aided Verification ⋮ Rewrite-Based Decision Procedures ⋮ Bounded Model Checking with Parametric Data Structures ⋮ Mothers of Pipelines ⋮ An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types ⋮ Hammering towards QED ⋮ Distributing the Workload in a Lazy Theorem-Prover ⋮ Extending Sledgehammer with SMT solvers
This page was built for software: CVC Lite
