Boogie

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 114 articles )

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

1 2 3 4 5 6 next

  1. Apt, Krzysztof R.; Olderog, Ernst-Rüdiger: Fifty years of Hoare’s logic (2019)
  2. Bouillaguet, Quentin; Bobot, François; Sighireanu, Mihaela; Yakobowski, Boris: Exploiting pointer analysis in memory models for deductive verification (2019)
  3. Milicevic, Aleksandar; Near, Joseph P.; Kang, Eunsuk; Jackson, Daniel: Alloy*: a general-purpose higher-order relational constraint solver (2019)
  4. Wang, Wenxi; Søndergaard, Harald; Stuckey, Peter J.: Wombit: a portfolio bit-vector solver using word-level propagation (2019)
  5. Zakowski, Yannick; Cachera, David; Demange, Delphine; Petri, Gustavo; Pichardie, David; Jagannathan, Suresh; Vitek, Jan: Verifying a concurrent garbage collector with a Rely-Guarantee methodology (2019)
  6. Bao, Yuyan; Leavens, Gary T.; Ernst, Gidon: Unifying separation logic and region logic to allow interoperability (2018)
  7. Dailler, Sylvain; Hauzar, David; Marché, Claude; Moy, Yannick: Instrumenting a weakest precondition calculus for counterexample generation (2018)
  8. Godefroid, Patrice; Sen, Koushik: Combining model checking and testing (2018)
  9. He, Shaobo; Lahiri, Shuvendu K.; Rakamarić, Zvonimir: Verifying relative safety, accuracy, and termination for program approximations (2018)
  10. Kiefer, Moritz; Klebanov, Vladimir; Ulbrich, Mattias: Relational program reasoning using compiler IR (2018)
  11. Klebanov, Vladimir; Rümmer, Philipp; Ulbrich, Mattias: Automating regression verification of pointer programs by predicate abstraction (2018)
  12. Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei: A foolish encoding of the next state relations of imperative programs (2018)
  13. Moore, Brandon; Peña, Lucas; Rosu, Grigore: Program verification by coinduction (2018)
  14. Müller, Peter (ed.); Schaefer, Ina (ed.): Principled software development. Essays dedicated to Arnd Poetzsch-Heffter on the occasion of his 60th birthday. Selected papers based on the presentations at the symposium, Kaiserslautern, Germany, November 2018 (2018)
  15. Summers, Alexander J.; Müller, Peter: Automating deductive verification for weak-memory programs (2018)
  16. Chakraborty, Supratik; Gupta, Ashutosh; Jain, Rahul: Matching multiplications in bit-vector formulas (2017)
  17. Ozeri, Or; Padon, Oded; Rinetzky, Noam; Sagiv, Mooly: Conjunctive abstract interpretation using paramodulation (2017)
  18. Wood, Tim; Drossopolou, Sophia; Lahiri, Shuvendu K.; Eisenbach, Susan: Modular verification of procedure equivalence in the presence of memory allocation (2017)
  19. Belo Lourenço, Cláudio; João Frade, Maria; Sousa Pinto, Jorge: Formalizing single-assignment program verification: an adaptation-complete approach (2016)
  20. Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas: Encoding monomorphic and polymorphic types (2016)

1 2 3 4 5 6 next