Boogie: A Modular Reusable Verifier for Object-Oriented Programs
By Mike Barnett, B. E. Chang, R. Deline, Bart P. F. Jacobs, K. R. M. Leino. Formal Methods for Components and Objects, 2005
1,068 citations recorded by the source corpus.
Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software
View Paper: https://www.semanticscholar.org/paper/31120ae4647ed520efa75ddcaaa3316966f4eff9
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Artificial Intelligence
- Sanjit A. Seshia
- Rohit Sinha
- Clark W. Barrett
- Sriram K. Rajamani
- Cesare Tinelli
- François Bobot
- A. Paskevich
- Jean-Christophe Filliâtre
In Computational Theory and Mathematics
- Sanjit A. Seshia
- Clark W. Barrett
- Cesare Tinelli
- François Bobot
- A. Paskevich
- Jean-Christophe Filliâtre
- Claude Marché
- Andrew Reynolds
In Software
- Abhik Roychoudhury
- Sergey Mechtaev
- Jooyong Yi
- Sanjit A. Seshia
- Cesare Tinelli
- Rohit Sinha
- Clark W. Barrett
- Sriram K. Rajamani
Citations in the corpus
- A design and verification methodology for secure isolated regions (2016, methodology): “The Boogie verifier [4] generates VCs and automatically discharges them using the Z3 SMT solver [14].”
- Building a push-button RESOLVE verifier: Progress and challenges (2011, neutral): “Whereas RESOLVE compiles mathematical assertions directly to VCs, Spec# compiles first to an intermediate language, Boogie [4], intended to generalize the verification process.”
- Why3 - Where Programs Meet Provers (2013, methodology): “WhyML is used as an intermediate language for the verification of C, Java, or Ada programs [2], in a similar fashion to the Boogie language [3].”
- Rodin: an open toolset for modelling and reasoning in Event-B (2010, methodology): “We quote two points from [11] about Boogie and present our view of them:”
- cvc5: A Versatile and Industrial-Strength SMT Solver (2022, background): “SMT solvers are widely recognized as crucial back-end reasoning engines for a variety of applications, including software and hardware verification [19, 52, 60, 68, 82, 86], model checking [41, 42, 98], type checking, static analysis, security [10,62], automated test-case generation [40,135],…”
- Why3: Shepherd Your Herd of Provers (2011, methodology): “We also plan to use WhyML as an intermediate language for program verification, in the spirit of the former Why platform [14] or Boogie [1].”
- Moat: Verifying Confidentiality of Enclave Programs (2015, methodology): “While attempting to prove this property in the Boogie verifier [6], we quite expectedly discovered counter-examples that illustrate the different ways in which G affects p enc ’s execution: 1. p enc invokes load ( mem , a ), where a is an address in mem ¬ epc .”
- DirectFix: Looking for Simple Program Repairs (2015, methodology): “VCC translates a C program into a Boogie program.”
- VCC: A Practical System for Verifying Concurrent C (2009, neutral): “Boogie [14] is an intermediate language that is used by a number of software verification tools including Spec# and HAVOC.”
- A Formal Foundation for Secure Remote Execution of Enclaves (2017, methodology): “A significant part of the effort in developing the proofs was finding the correct inductive invariants to help Boogie prove the properties.”