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

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

1 2 3 4 5 next

  1. Chakraborty, Supratik; Gupta, Ashutosh; Jain, Rahul: Matching multiplications in bit-vector formulas (2017)
  2. Ozeri, Or; Padon, Oded; Rinetzky, Noam; Sagiv, Mooly: Conjunctive abstract interpretation using paramodulation (2017)
  3. Wood, Tim; Drossopolou, Sophia; Lahiri, Shuvendu K.; Eisenbach, Susan: Modular verification of procedure equivalence in the presence of memory allocation (2017)
  4. Belo Lourenço, Cláudio; João Frade, Maria; Sousa Pinto, Jorge: Formalizing single-assignment program verification: an adaptation-complete approach (2016)
  5. Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas: Encoding monomorphic and polymorphic types (2016)
  6. Komuravelli, Anvesh; Gurfinkel, Arie; Chaki, Sagar: SMT-based model checking for recursive programs (2016)
  7. Kremer, Gereon; Corzilius, Florian; Ábrahám, Erika: A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic (2016)
  8. Müller, Peter; Schwerhoff, Malte; Summers, Alexander J.: Viper: a verification infrastructure for permission-based reasoning (2016)
  9. Wiik, Jonatan; Boström, Pontus: Contract-based verification of MATLAB-style matrix programs (2016)
  10. Ahrendt, Wolfgang; Kovács, Laura; Robillard, Simon: Reasoning about loops using Vampire in KeY (2015)
  11. Bjørner, Nikolaj; Gurfinkel, Arie; McMillan, Ken; Rybalchenko, Andrey: Horn clause solvers for program verification (2015)
  12. Christakis, Maria; Müller, Peter; Wüstholz, Valentin: An experimental evaluation of deliberate unsoundness in a static program analyzer (2015)
  13. Elenbogen, Dima; Katz, Shmuel; Strichman, Ofer: Proving mutual termination (2015)
  14. Kirchner, Florent; Kosmatov, Nikolai; Prevosto, Virgile; Signoles, Julien; Yakobowski, Boris: Frama-C: a software analysis perspective (2015) ioport
  15. Leino, K.Rustan M.; Lucio, Paqui: An assertional proof of the stability and correctness of Natural Mergesort (2015)
  16. Schäf, Martin; Tiwari, Ashish: Severity levels of inconsistent code (2015)
  17. Alkassar, Eyad; Böhme, Sascha; Mehlhorn, Kurt; Rizkallah, Christine: A framework for the verification of certifying computations (2014)
  18. Amighi, Afshin; Blom, Stefan; Darabi, Saeed; Huisman, Marieke; Mostowski, Wojciech; Zaharieva-Stojanovski, Marina: Verification of concurrent systems with VerCors (2014)
  19. Furia, Carlo A.; Meyer, Bertrand; Velder, Sergey: Loop invariants: analysis, classification, and examples (2014)
  20. Malkis, Alexander; Banerjee, Anindya: On automation in the verification of software barriers: experience report (2014)

1 2 3 4 5 next