Cited in
(only showing first 100 items - show all)- A learning-based approach to synthesizing invariants for incomplete verification engines
- Verifying Heap-Manipulating Programs in an SMT Framework
- scientific article; zbMATH DE number 2090312 (Why is no real title available?)
- A posthumous contribution by Larry Wos: excerpts from an unpublished column
- Verifying Whiley programs with Boogie
- Quantifier simplification by unification in SMT
- Product programs in the wild: retrofitting program verifiers to check information flow security
- Using History Invariants to Verify Observers
- The Daikon system for dynamic detection of likely invariants
- Efficient weakest preconditions
- Programming Languages and Systems
- Programming Languages and Systems
- Adapting real quantifier elimination methods for conflict set computation
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Modular verification of procedure equivalence in the presence of memory allocation
- Formal verification of a C-like memory model and its uses for verifying program transformations
- Automating Induction with an SMT Solver
- Computer Aided Verification
- Incremental Instance Generation in Local Reasoning
- Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
- Theoretical Aspects of Computing – ICTAC 2005
- Predicate abstraction in a program logic calculus
- Abstract Counterexamples for Non-disjunctive Abstractions
- Algebraic Methodology and Software Technology
- SMELS: Satisfiability Modulo Equality with Lazy Superposition
- Automating theorem proving with SMT
- Two for the price of one: lifting separation logic assertions
- Automated verification of functional correctness of race-free GPU programs
- Counterexample-guided quantifier instantiation for synthesis in SMT
- Programmed strategies for program verification
- Decision procedures for flat array properties
- Interpolation systems for ground proofs in automated deduction: a survey
- Adding decision procedures to SMT solvers using axioms with triggers
- Semantically-guided goal-sensitive reasoning: model representation
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- Extended static checking
- Formal proof of SCHUR conjugate function
- An instantiation scheme for satisfiability modulo theories
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- On deciding satisfiability by theorem proving with speculative inferences
- New results on rewrite-based satisfiability procedures
- Synthesis of positive logic programs for checking a class of definitions with infinite quantification
- Automatic software model checking via constraint logic
- Bounded quantifier instantiation for checking inductive invariants
- Proving properties of functional programs by equality saturation
- Congruence closure with free variables
- Search-space partitioning for parallelizing SMT solvers
- Automated Deduction – CADE-20
- Automated Deduction – CADE-20
- Automatic decidability and combinability
- Certifying optimality of state estimation programs.
- SMELS: satisfiability modulo equality with lazy superposition
- OpenSMT2: an SMT solver for multi-core and cloud computing
- Experience of improving the BLAST static verification tool
- Solving bitvectors with MCSAT: explanations from bits and pieces
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Zap: Automated Theorem Proving for Software Analysis
- Combining nonstably infinite theories
- Refutation-based synthesis in SMT
- Thread Quantification for Concurrent Shape Analysis
- Program verification with interacting analysis plugins
- Formal Methods for Hardware Verification
- Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
- Solving quantified verification conditions using satisfiability modulo theories
- Theory decision by decomposition
- Structured derivations: a unified proof style for teaching mathematics
- Don't care words with an application to the automata-based approach for real addition
- Automating regression verification of pointer programs by predicate abstraction
- Generating error traces from verification-condition counterexamples
- Boolector
- Dafny
- JMLUnit
- QOCA
- Cogent
- Valigator
- Zing
- COMBINE
- SciNapse
- BarcelogicTools
- ACSAR
- SCHUR
- KRAKATOA
- SPARK
- PVS
- SMT-LIB
- Daikon
- GeoSteiner
- Caduceus
- JML
- Frama-C
- Omnibus
- Why3
- Yices
- Alt-Ergo
- cvc3
- Spec#
- UCLID
- z3
- MONA
- Princess
This page was built for software: SIMPLIFY
