BoogiePL

MaRDI QIDQ33328swMATHFDO

Official website https://www.microsoft.com/en-us/research/publication/boogiepl-a-typed-procedural-language-for-checking-object-oriented-programs/

Cited in

(31)

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

This page was built for software: BoogiePL