Cited in
(only showing first 100 items - show all)- 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
- Satisfiability modulo theories
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- Challenges in Satisfiability Modulo Theories
- Estimating the volume of solution space for satisfiability modulo linear real arithmetic
- Sharing is caring: combination of theories
- Extending Sledgehammer with SMT solvers
- CoLiS
- Shellcheck
- Whiley
- 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
- Formal verification for high-assurance behavioral synthesis
- A formally verified interpreter for a shell-like programming language
- Cooperating theorem provers: a case study combining HOL-Light and CVC Lite
- Automatic verification of TLA\(^{ + }\) proof obligations with SMT solvers
- Translation validation of loop optimizations and software pipelining in the TVOC framework. In memory of Amir Pnueli
- checkbashisms
- Model-based theory combination
- E-matching for fun and profit
- Satisfiability solving and model generation for quantified first-order logic formulas
- Testing and debugging techniques for answer set solver development
- 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
- Conflict Resolution
- TASS: the toolkit for accurate scientific software
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- JMLAutoTest
- Whiteoak
- A slice-based decision procedure for type-based partial orders
- 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
This page was built for software: cvc3
