cvc3

swMATH4886MaRDI QIDQ17038FDOQ17038

Author name not available (Why is that?)

Cited In (79)

• Formal Verification for High-Assurance Behavioral Synthesis
• Translation Validation of Loop Optimizations and Software Pipelining in the TVOC Framework
• A Slice-Based Decision Procedure for Type-Based Partial Orders
• Automatic Verification of TLA +  Proof Obligations with SMT Solvers
• I-RiSC: An SMT-Compliant Solver for the Existential Fragment of Real Algebra
• Testing and debugging techniques for answer set solver development
• Title not available (Why is that?)
• Sharing Is Caring: Combination of Theories
• Heaps and Data Structures: A Challenge for Automated Provers
• Title not available (Why is that?)
• Minimal counterexamples for linear-time probabilistic verification
• Verifying Whiley programs with Boogie
• Being careful about theory combination
• Combining Top-Down and Bottom-Up Techniques in Program Derivation
• Formal analysis of the compact position reporting algorithm
• Towards Automatic Stability Analysis for Rely-Guarantee Proofs
• SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
• Satisfiability Solving and Model Generation for Quantified First-Order Logic Formulas
• Dafny: An Automatic Program Verifier for Functional Correctness
• Automatic Proof and Disproof in Isabelle/HOL
• SMELS: Satisfiability Modulo Equality with Lazy Superposition
• Title not available (Why is that?)
• Volume Computation for Boolean Combination of Linear Arithmetic Constraints
• An experiment with satisfiability modulo SAT
• Rewriting Induction + Linear Arithmetic = Decision Procedure
• New results on rewrite-based satisfiability procedures
• Assumption propagation through annotated programs
• Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis
• SAT modulo linear arithmetic for solving polynomial constraints
• SMELS: satisfiability modulo equality with lazy superposition
• Experience of improving the BLAST static verification tool
• iProver-Eq: An Instantiation-Based Theorem Prover with Equality
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS
• Hardware-Dependent Proofs of Numerical Programs
• Cuts from proofs: a complete and practical technique for solving linear inequalities over integers
• Solving quantified verification conditions using satisfiability modulo theories
• A formal semantics of extended hierarchical state transition matrices using CSP\#
• Don't care words with an application to the automata-based approach for real addition
• Automatic search for bit-based division property
• Behavioral interface specification languages
• A unified framework for DPLL(T) + certificates
• Trusting computations: a mechanized proof from partial differential equations to actual program
• Efficiently solving quantified bit-vector formulas
• Multi-Prover Verification of Floating-Point Programs
• Title not available (Why is that?)
• Verification conditions for source-level imperative programs
• Extending Sledgehammer with SMT Solvers
• Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
• The Complexity of Reversal-Bounded Model-Checking
• Challenges in Satisfiability Modulo Theories
• Formal Proof of SCHUR Conjugate Function
• Expressing Polymorphic Types in a Many-Sorted Language
• Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories
• The TPTP Typed First-Order Form with Arithmetic
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• Estimating the volume of solution space for satisfiability modulo linear real arithmetic
• Building a Calculus of Data Structures
• Extending Sledgehammer with SMT solvers
• SMT proof checking using a logical framework
• Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis
• Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data
• Cooperating theorem provers: a case study combining HOL-Light and CVC Lite
• A formally verified interpreter for a shell-like programming language
• Modular SMT Proofs for Fast Reflexive Checking Inside Coq
• Model-based theory combination
• E-matching for fun and profit
• Collective Assertions
• The Strategy Challenge in SMT Solving
• Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL
• Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences
• Automating Theorem Proving with SMT
• Satisfiability Modulo Theories
• Conflict Resolution
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• TASS: the toolkit for accurate scientific software
• Formal verification of numerical programs: from C annotated programs to mechanical proofs
• Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
• Combining Theories with Shared Set Operations
• Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers

This page was built for software: cvc3