SIMPLIFY
From MaRDI portal
swMATH4976MaRDI QIDQ17123FDOQ17123
Author name not available (Why is that?)
Official website: http://www.kindsoftware.com/products/opensource/Simplify/
Cited In (only showing first 100 items - show all)
- A learning-based approach to synthesizing invariants for incomplete verification engines
- Using History Invariants to Verify Observers
- A posthumous contribution by Larry Wos: excerpts from an unpublished column
- Verifying Whiley programs with Boogie
- Adapting real quantifier elimination methods for conflict set computation
- Incremental Instance Generation in Local Reasoning
- Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
- SMELS: Satisfiability Modulo Equality with Lazy Superposition
- Automating theorem proving with SMT
- Two for the price of one: lifting separation logic assertions
- Extended static checking
- Formal proof of SCHUR conjugate function
- Synthesis of positive logic programs for checking a class of definitions with infinite quantification
- Search-space partitioning for parallelizing SMT solvers
- Automatic software model checking via constraint logic
- OpenSMT2: an SMT solver for multi-core and cloud computing
- SMELS: satisfiability modulo equality with lazy superposition
- Experience of improving the BLAST static verification tool
- Zap: Automated Theorem Proving for Software Analysis
- Formal Methods for Hardware Verification
- Program verification with interacting analysis plugins
- Automating regression verification of pointer programs by predicate abstraction
- Generating error traces from verification-condition counterexamples
- Modular SMT proofs for fast reflexive checking inside Coq
- Model Checking Software
- A verifying compiler for a multi-threaded object-oriented language
- Solving quantified bit-vector formulas using binary decision diagrams
- Congruence closure in intensional type theory
- SAT-Based Model Checking
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
- Verifying and synthesizing software with recursive functions (invited contribution)
- Decision procedures for region logic
- Embedded software verification using symbolic execution and uninterpreted functions
- Combination of convex theories: modularity, deduction completeness, and explanation
- Unification with abstraction and theory instantiation in saturation-based reasoning
- Solving quantified linear arithmetic by counterexample-guided instantiation
- lazyCoP
- Whiley
- The problems of C program verification
- JMLAutoTest
- Whiteoak
- Practical realisation and elimination of an ECC-related software bug attack
- Satisfiability solving and model generation for quantified first-order logic formulas
- Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic
- Counterexample-Guided Model Synthesis
- Verification of SpecC using predicate abstraction
- Theories, solvers and static analysis by abstract interpretation
- Generating Unit Tests from Formal Proofs
- A polymorphic intermediate verification language: design and logical encoding
- DCAS-based concurrent deques
- The Daikon system for dynamic detection of likely invariants
- Automating Induction with an SMT Solver
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- Boolector
- QOCA
- Cogent
- SMT-LIB
- 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
- OpenSMT
- Bebop
- Leon
- CVC
- CVC4
- iProver-Eq
- eVolCheck
- Amphion
- CVT
- CCured
- KeY
- Omega+
- SCOOT
- MOPS
- VeriCool
- Sparkle
- LOOP
- TVLA
- UMM
This page was built for software: SIMPLIFY
