SIMPLIFY
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Invariant based programming: Basic approach and teaching experiences
- 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
- Theory decision by decomposition
- Combination of convex theories: modularity, deduction completeness, and explanation
- Boolector
- Dafny
- JMLUnit
- lazyCoP
- QOCA
- Whiley
- Valigator
- Zing
- Cogent
- COMBINE
- SciNapse
- BarcelogicTools
- ACSAR
- SCHUR
- SPARK
- KRAKATOA
- PVS
- SMT-LIB
- Daikon
- GeoSteiner
- Automating regression verification of pointer programs by predicate abstraction
- Yices
- Why3
- JML
- Spec#
- Omnibus
- Caduceus
- Frama-C
- UCLID
- Solving quantified linear arithmetic by counterexample-guided instantiation
- Counterexample-guided quantifier instantiation for synthesis in SMT
- Automated verification of functional correctness of race-free GPU programs
- cvc3
- z3
- Alt-Ergo
- Experience of improving the BLAST static verification tool
- Generating error traces from verification-condition counterexamples
- MONA
- DCAS-based concurrent deques
- Automatic software model checking via constraint logic
- Zap
- Princess
- bv2epr
- ESC/Java
- VCC
- Korat
- JUnit
- veriT
- CVC Lite
- Chalice
- Boogie
- PeRIPLO
- OpenSMT
- Bebop
- Solving bitvectors with MCSAT: explanations from bits and pieces
- A posthumous contribution by Larry Wos: excerpts from an unpublished column
- Verifying Whiley programs with Boogie
- Leon
- iProver-Eq
- CVC
- CVC4
- eVolCheck
- VeriCool
- Sparkle
- TVLA
- Omega+
- CVT
- Amphion
- SCOOT
- KeY
- CCured
- A learning-based approach to synthesizing invariants for incomplete verification engines
- MOPS
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- UMM
- LOOP
- Refutation-based synthesis in SMT
- Extending SMT solvers to higher-order logic
- VerCors
- Unification with abstraction and theory instantiation in saturation-based reasoning
- CSIsat
- SMELS: satisfiability modulo equality with lazy superposition
- On interpolation in automated theorem proving
- Verification of SpecC using predicate abstraction
- Mcmt
- Jahob
- The Daikon system for dynamic detection of likely invariants
- SatAbs
- FOCI
- SymDiff
- Embedded software verification using symbolic execution and uninterpreted functions
- Mercator
- VERL
- Beagle
This page was built for software: SIMPLIFY
