Cited in
(31)- TrABin
- HolBA
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Leveraging compiler intermediate representation for multi- and cross-language verification
- Hoare-style logic for unstructured programs
- HOL-Boogie
- Predator
- GENA
- TVLA
- net.datastructures
- Joogie
- LCTD
- DKAL and Z3: a logic embedding experiment
- ARMor
- DKAL
- SMACK
- Cibai
- UppSAT
- LCT
- Cloc
- Calysto
- Cascade
- GraVy
- A dynamic logic for unstructured programs with embedded assertions
- QF_FP
- An SMT theory of fixed-point arithmetic
- A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs
- LCTD: test-guided proofs for C programs on LLVM
- Programming Languages and Systems
- Cost analysis of object-oriented bytecode programs
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
This page was built for software: BoogiePL
