cvc3

swMATH4886MaRDI QIDQ17038FDOQ17038

Author name not available (Why is that?)

Cited In (79)

• I-RiSC: an SMT-compliant solver for the existential fragment of real algebra
• Formal verification for high-assurance behavioral synthesis
• Translation validation of loop optimizations and software pipelining in the TVOC framework. In memory of Amir Pnueli
• Automatic verification of TLA\(^{ + }\) proof obligations with SMT solvers
• Testing and debugging techniques for answer set solver development
• A slice-based decision procedure for type-based partial orders
• Title not available (Why is that?)
• Heaps and Data Structures: A Challenge for Automated Provers
• Extending Sledgehammer with SMT solvers
• 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
• SMELS: Satisfiability Modulo Equality with Lazy Superposition
• Volume Computation for Boolean Combination of Linear Arithmetic Constraints
• An experiment with satisfiability modulo SAT
• Rewriting Induction + Linear Arithmetic = Decision Procedure
• Formal proof of SCHUR conjugate function
• New results on rewrite-based satisfiability procedures
• The strategy challenge in SMT solving
• Building a calculus of data structures
• 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
• The complexity of reversal-bounded model-checking
• SMELS: satisfiability modulo equality with lazy superposition
• Experience of improving the BLAST static verification tool
• iProver-Eq: An Instantiation-Based Theorem Prover with Equality
• Expressing polymorphic types in a many-sorted language
• Lazy satisfiability modulo theories
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS
• Hardware-Dependent Proofs of Numerical Programs
• Computing small unsatisfiable cores in satisfiability modulo theories
• Cuts from proofs: a complete and practical technique for solving linear inequalities over integers
• The TPTP typed first-order form with arithmetic
• 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
• Modular SMT proofs for fast reflexive checking inside Coq
• Trusting computations: a mechanized proof from partial differential equations to actual program
• Efficiently solving quantified bit-vector formulas
• Abstract domains for automated reasoning about list-manipulating programs with infinite data
• Title not available (Why is that?)
• An abstract decision procedure for a theory of inductive data types.
• Collective assertions
• Verification conditions for source-level imperative programs
• Combining theories with shared set operations
• 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
• Challenges in Satisfiability Modulo Theories
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• Estimating the volume of solution space for satisfiability modulo linear real arithmetic
• Sharing is caring: combination of theories
• Extending Sledgehammer with SMT solvers
• SMT proof checking using a logical framework
• Multi-prover verification of floating-point programs
• Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis
• Cooperating theorem provers: a case study combining HOL-Light and CVC Lite
• A formally verified interpreter for a shell-like programming language
• Model-based theory combination
• E-matching for fun and profit
• 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
• 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
• Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers

This page was built for software: cvc3