cvc3

swMATH4886MaRDI QIDQ17038

No author found.

Related Items (79)

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

This page was built for software: cvc3