cvc3
From MaRDI portal
Cvc3
Cited in
(only showing first 100 items - show all)- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- Minimal counterexamples for linear-time probabilistic verification
- Heaps and Data Structures: A Challenge for Automated Provers
- Extending Sledgehammer with SMT solvers
- Verifying Whiley programs with Boogie
- Being careful about theory combination
- 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
- Automating theorem proving with SMT
- 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
- SAT modulo linear arithmetic for solving polynomial constraints
- Assumption propagation through annotated programs
- New results on rewrite-based satisfiability procedures
- Building a calculus of data structures
- The strategy challenge in SMT solving
- The complexity of reversal-bounded model-checking
- Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis
- SMELS: satisfiability modulo equality with lazy superposition
- Experience of improving the BLAST static verification tool
- Expressing polymorphic types in a many-sorted language
- Lazy satisfiability modulo theories
- iProver-Eq: An Instantiation-Based Theorem Prover with Equality
- A FORMAL SYSTEM FOR EUCLID’SELEMENTS
- Combining top-down and bottom-up techniques in program derivation
- 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
- Solving quantified verification conditions using satisfiability modulo theories
- A formal semantics of extended hierarchical state transition matrices using CSP\#
- The TPTP typed first-order form with arithmetic
- 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
- Beaver
- Cocktail
- GNT
- HOL-Boogie
- BarcelogicTools
- TVOC
- SCHUR
- KRAKATOA
- ACSL
- LiQuor
- SMT-LIB
- Caduceus
- Why3
- Yices
- Alt-Ergo
- Gappa
- ISP
- UCLID
- SIMPLIFY
- TASS_
- z3
- COMICS
- GiNaCRA
- FADAlib
- Zap
- ESC4
- TaPAS
- CVC Lite
- CLSAT
- Interproc
- CVC
- MathSAT
- DiPro
- HighSpec
- CVT
- VeriCool
- Monotonox
- CSIsat
- MUP
- Jahob
- RSat
- I-RiSC
- LASH
- LIRA
- H-PILoT
- KLEE-FP
- Nemerle
- Robbins Conjecture
- STP
- 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
- Verification conditions for source-level imperative programs
- scientific article; zbMATH DE number 5613976 (Why is no real title available?)
- Collective assertions
- I-RiSC: an SMT-compliant solver for the existential fragment of real algebra
- An abstract decision procedure for a theory of inductive data types.
- Combining theories with shared set operations
This page was built for software: cvc3
