cvc3
From MaRDI portal
Cvc3
Cited in
(only showing first 100 items - show all)- Don't care words with an application to the automata-based approach for real addition
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
- Solving quantified verification conditions using satisfiability modulo theories
- Beaver
- Cocktail
- GNT
- HOL-Boogie
- Shellcheck
- CoLiS
- Whiley
- BarcelogicTools
- TVOC
- SCHUR
- KRAKATOA
- SMT-LIB
- A formally verified interpreter for a shell-like programming language
- LiQuor
- ACSL
- Yices
- Why3
- Caduceus
- UCLID
- Gappa
- z3
- Alt-Ergo
- TASS_
- ISP
- SIMPLIFY
- Experience of improving the BLAST static verification tool
- COMICS
- GiNaCRA
- Zap
- FADAlib
- ESC4
- TaPAS
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
- TASS: the toolkit for accurate scientific software
- CVC Lite
- Formal analysis of the compact position reporting algorithm
- CLSAT
- Verifying Whiley programs with Boogie
- Interproc
- MathSAT
- CVC
- Automatic search for bit-based division property
- DiPro
- VeriCool
- HighSpec
- CVT
- Monotonox
- CSIsat
- Estimating the volume of solution space for satisfiability modulo linear real arithmetic
- Extending Sledgehammer with SMT solvers
- SMELS: satisfiability modulo equality with lazy superposition
- A unified framework for DPLL(T) + certificates
- MUP
- Trusting computations: a mechanized proof from partial differential equations to actual program
- Jahob
- Efficiently solving quantified bit-vector formulas
- Being careful about theory combination
- SMT proof checking using a logical framework
- RSat
- Assumption propagation through annotated programs
- I-RiSC
- Cooperating theorem provers: a case study combining HOL-Light and CVC Lite
- E-matching for fun and profit
- Model-based theory combination
- An experiment with satisfiability modulo SAT
- Behavioral interface specification languages
- 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
- Rewriting Induction + Linear Arithmetic = Decision Procedure
- Computing small unsatisfiable cores in satisfiability modulo theories
- I-RiSC: an SMT-compliant solver for the existential fragment of real algebra
- Dafny: an automatic program verifier for functional correctness
- Satisfiability solving and model generation for quantified first-order logic formulas
- Collective assertions
- 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
- 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
- Satisfiability modulo theories
- scientific article; zbMATH DE number 5613976 (Why is no real title available?)
- Conflict Resolution
- LASH
- LIRA
- SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
- Lazy satisfiability modulo theories
- H-PILoT
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- SMELS: Satisfiability Modulo Equality with Lazy Superposition
- Formal proof of SCHUR conjugate function
- Testing and debugging techniques for answer set solver development
- Towards Automatic Stability Analysis for Rely-Guarantee 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
