Boogie
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Integration of verification methods for program systems
- An extensible encoding of object-oriented data models in HOL. With an application to IMP++
- Boolector
- Dafny
- HOL-Boogie
- KeY-C
- Ghidra
- Whiley
- ARQMath
- Modula
- ALGOL 68
- IMP++
- CalFuzzer
- SCOOP
- HOL-Z
- ANTLR
- SPARK
- KRAKATOA
- Eiffel
- SMT-LIB
- ACSL
- Instrumenting a weakest precondition calculus for counterexample generation
- Daikon
- Automating regression verification of pointer programs by predicate abstraction
- Why3
- JML
- Spec#
- Omnibus
- distcc
- Caduceus
- Frama-C
- Relational program reasoning using compiler IR
- cvc3
- z3
- LLVM
- Dagger
- SIMPLIFY
- Unifying separation logic and region logic to allow interoperability
- A FOOLish encoding of the next state relations of imperative programs
- ProMoVer
- Rodin
- Atelier B
- Scala
- ESC/Java
- ESC4
- VCC
- PathCrawler
- Pex
- Assertion-based slicing and slice graphs
- Stepwise refinement of heap-manipulating code in Chalice
- A system for compositional verification of asynchronous objects
- Chalice
- VeriFast
- ACL2s
- KRATOS
- JACK
- Alloy*: a general-purpose higher-order relational constraint solver
- CompCertTSO
- Automatic proofs of memory deallocation for a Whiley-to-C compiler
- Verifying Whiley programs with Boogie
- Generalized arrays for Stainless frames
- WhyML
- cminor
- VeriCool
- HighSpec
- InvGen
- HIP
- Smallfoot
- HMC
- SLAB
- NaCl
- Checkfence
- KeY
- CCured
- KIV
- FixBag
- A learning-based approach to synthesizing invariants for incomplete verification engines
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Safe functional systems through integrity types and verified assembly
- Deductive verification of floating-point Java programs in KeY
- BWare
- Fifty years of Hoare's logic
- Regression verification for unbalanced recursive functions
- Exploiting pointer analysis in memory models for deductive verification
- Verifying a concurrent garbage collector with a rely-guarantee methodology
- VerCors
- GPUVerify
- jStar
- Wombit: a portfolio bit-vector solver using word-level propagation
- Program verification by coinduction
- Automating deductive verification for weak-memory programs
- NModel
- SpecExplorer
- AURA
- A framework for the verification of certifying computations
- On automation in the verification of software barriers: experience report
- Jahob
- SMT proof checking using a logical framework
- Traffic 4
- Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006)
This page was built for software: Boogie
