SIMPLIFY
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Combination of convex theories: modularity, deduction completeness, and explanation
- Adapting real quantifier elimination methods for conflict set computation
- SMELS: satisfiability modulo equality with lazy superposition
- A polymorphic intermediate verification language: design and logical encoding
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
- scientific article; zbMATH DE number 2090312 (Why is no real title available?)
- Quantifier simplification by unification in SMT
- Product programs in the wild: retrofitting program verifiers to check information flow security
- A learning-based approach to synthesizing invariants for incomplete verification engines
- Modular verification of procedure equivalence in the presence of memory allocation
- Verification of SpecC using predicate abstraction
- Solving quantified linear arithmetic by counterexample-guided instantiation
- Incremental Instance Generation in Local Reasoning
- Search-space partitioning for parallelizing SMT solvers
- Congruence closure with free variables
- Extended static checking
- Automating regression verification of pointer programs by predicate abstraction
- Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
- Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic
- Formal proof of SCHUR conjugate function
- Using History Invariants to Verify Observers
- Program verification with interacting analysis plugins
- SMELS: Satisfiability Modulo Equality with Lazy Superposition
- Counterexample-Guided Model Synthesis
- Automating theorem proving with SMT
- Verifying and synthesizing software with recursive functions (invited contribution)
- DCAS-based concurrent deques
- Automatic software model checking via constraint logic
- Solving quantified bit-vector formulas using binary decision diagrams
- Generating error traces from verification-condition counterexamples
- Programmed strategies for program verification
- Experience of improving the BLAST static verification tool
- SAT-Based Model Checking
- Congruence closure in intensional type theory
- Unification with abstraction and theory instantiation in saturation-based reasoning
- Decision procedures for region logic
- Computer Aided Verification
- Model Checking Software
- Embedded software verification using symbolic execution and uninterpreted functions
- A posthumous contribution by Larry Wos: excerpts from an unpublished column
- A verifying compiler for a multi-threaded object-oriented language
- Verifying Whiley programs with Boogie
- lazyCoP
- Whiley
- JMLAutoTest
- Whiteoak
- Formal verification of a C-like memory model and its uses for verifying program transformations
- Zap: Automated Theorem Proving for Software Analysis
- Satisfiability solving and model generation for quantified first-order logic formulas
- Generating Unit Tests from Formal Proofs
- Synthesis of positive logic programs for checking a class of definitions with infinite quantification
- Formal Methods for Hardware Verification
- Practical realisation and elimination of an ECC-related software bug attack
- Theories, solvers and static analysis by abstract interpretation
- Modular SMT proofs for fast reflexive checking inside Coq
- OpenSMT2: an SMT solver for multi-core and cloud computing
- The Daikon system for dynamic detection of likely invariants
- Dafny: an automatic program verifier for functional correctness
- 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
- bv2epr
- Zap
- ESC/Java
- Korat
- JUnit
- VCC
- veriT
- CVC Lite
- Boogie
- Chalice
- PeRIPLO
This page was built for software: SIMPLIFY
