BoogiePL

BoogiePL: A typed procedural language for checking object-oriented programs. This note defines BoogiePL, an intermediate language for program analysis and program verification. The language is a simple coarsely typed imperative language with procedures and arrays, plus support for introducing mathematical functions and declaring properties of these functions. BoogiePL can be used to represent programs written in an imperative source language (like an object-oriented .NET language), along with a logical encoding of the semantics of such a source language. From the resulting BoogiePL program, one can then generate verification conditions or perform other program analyses such as the inference of program invariants. In this way, BoogiePL also serves as a programming-notation front end to theorem provers. BoogiePL is accepted as input to Boogie, the Spec# static program verifier.


References in zbMATH (referenced in 12 articles )

Showing results 1 to 12 of 12.
Sorted by year (citations)

  1. Garzella, Jack J.; Baranowski, Marek; He, Shaobo; Rakamarić, Zvonimir: Leveraging compiler intermediate representation for multi- and cross-language verification (2020)
  2. Saarikivi, Olli; Heljanko, Keijo: LCTD: test-guided proofs for C programs on LLVM (2016)
  3. Albert, Elvira; Arenas, Puri; Genaim, Samir; Puebla, German; Zanardini, Damiano: Cost analysis of object-oriented bytecode programs (2012)
  4. Ulbrich, Mattias: A dynamic logic for unstructured programs with embedded assertions (2011)
  5. Ahrendt, Wolfgang; Beckert, Bernhard; Giese, Martin; Rümmer, Philipp: Practical aspects of automated deduction for program verification (2010) ioport
  6. Beckert, Bernhard; Moskal, Michal: Deductive verification of system software in the verisoft XT project (2010) ioport
  7. Böhme, Sascha; Moskal, Michał; Schulte, Wolfram; Wolff, Burkhart: HOL-Boogie -- an interactive prover-backend for the verifying C compiler (2010)
  8. Mera, Sergio; Bjørner, Nikolaj: DKAL and Z3: a logic embedding experiment (2010)
  9. Chatterjee, Shaunak; Lahiri, Shuvendu K.; Qadeer, Shaz; Rakamarić, Zvonimir: A low-level memory model and an accompanying reachability predicate (2009) ioport
  10. Böhme, Sascha; Leino, K. Rustan M.; Wolff, Burkhart: HOL-Boogie -- an interactive prover for the Boogie program-verifier (2008)
  11. Méndez-Lojo, Mario; Navas, Jorge; Hermenegildo, Manuel V.: A flexible, (C)LP-based approach to the analysis of object-oriented programs (2008)
  12. Leino, K. Rustan M.; Logozzo, Francesco: Loop invariants on demand (2005)