Boogie: An Intermediate Verification Language. Boogie is an intermediate verification language, intended as a layer on which to build program verifiers for other languages. Several program verifiers have been built in this way, including the VCC and HAVOC verifiers for C and the verifiers for Dafny, Chalice, and Spec#. A previous version of the language was called BoogiePL. The current language (version 2) is currently known as just Boogie, which is also the name of the verification tool that takes Boogie programs as input. Boogie is also the name of a tool. The tool accepts the Boogie language as input, optionally infers some invariants in the given Boogie program, and then generates verification conditions that are passed to an SMT solver. The default SMT solver is Z3.

References in zbMATH (referenced in 74 articles )

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

1 2 3 4 next

  1. Wiik, Jonatan; Boström, Pontus: Contract-based verification of MATLAB-style matrix programs (2016)
  2. Ahrendt, Wolfgang; Kovács, Laura; Robillard, Simon: Reasoning about loops using Vampire in KeY (2015)
  3. Christakis, Maria; Müller, Peter; Wüstholz, Valentin: An experimental evaluation of deliberate unsoundness in a static program analyzer (2015)
  4. Elenbogen, Dima; Katz, Shmuel; Strichman, Ofer: Proving mutual termination (2015)
  5. Kirchner, Florent; Kosmatov, Nikolai; Prevosto, Virgile; Signoles, Julien; Yakobowski, Boris: Frama-C: a software analysis perspective (2015)
  6. Schäf, Martin; Tiwari, Ashish: Severity levels of inconsistent code (2015)
  7. Alkassar, Eyad; Böhme, Sascha; Mehlhorn, Kurt; Rizkallah, Christine: A framework for the verification of certifying computations (2014)
  8. Amighi, Afshin; Blom, Stefan; Darabi, Saeed; Huisman, Marieke; Mostowski, Wojciech; Zaharieva-Stojanovski, Marina: Verification of concurrent systems with VerCors (2014)
  9. Malkis, Alexander; Banerjee, Anindya: On automation in the verification of software barriers: experience report (2014)
  10. Banerjee, Anindya; Naumann, David A.: Local reasoning for global invariants. II: Dynamic boundaries (2013)
  11. Collingbourne, Peter; Donaldson, Alastair F.; Ketema, Jeroen; Qadeer, Shaz: Interleaving and lock-step semantics for analysis and verification of GPU kernels (2013)
  12. Stump, Aaron; Oe, Duckki; Reynolds, Andrew; Hadarean, Liana; Tinelli, Cesare: SMT proof checking using a logical framework (2013)
  13. Ahrendt, Wolfgang; Dylla, Maximilian: A system for compositional verification of asynchronous objects (2012)
  14. Apt, Krzysztof R.; De Boer, Frank S.; Olderog, Ernst-Rüdiger; De Gouw, Stijn: Verification of object-oriented programs: a transformational approach (2012)
  15. Barros, José Bernardo; da Cruz, Daniela; Henriques, Pedro Rangel; Pinto, Jorge Sousa: Assertion-based slicing and slice graphs (2012)
  16. Hatcliff, John; Leavens, Gary T.; Leino, K.Rustan M.; Müller, Peter; Parkinson, Matthew: Behavioral interface specification languages (2012)
  17. Leino, K.Rustan M.; Yessenov, Kuat: Stepwise refinement of heap-manipulating code in Chalice (2012)
  18. Parkinson, Matthew J.; Summers, Alexander J.: The relationship between separation logic and implicit dynamic frames (2012)
  19. Rosenberg, Stan; Banerjee, Anindya; Naumann, David A.: Decision procedures for region logic (2012)
  20. Sonnex, William; Drossopoulou, Sophia; Eisenbach, Susan: Zeno: an automated prover for properties of recursive data structures (2012)

1 2 3 4 next