Boogie swMATH ID: 7714 Software Authors: K. Rustan M. Leino Description: 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. Homepage: http://research.microsoft.com/en-us/projects/boogie/ Related Software: z3; Why3; Spec#; KRAKATOA; ESC/Java; Dafny; Caduceus; VCC; SIMPLIFY; Coq; JML; VeriFast; SMT-LIB; Eiffel; KeY; Frama-C; Isabelle/HOL; WhyML; CVC4; ACSL Cited in: 117 Publications all top 5 Cited by 249 Authors 12 Leino, K. Rustan M. 5 Böhme, Sascha 5 Müller, Peter 5 Summers, Alexander J. 4 Banerjee, Anindya 4 Lahiri, Shuvendu Kumar 4 Schulte, Wolfram 4 Ulbrich, Mattias 4 Wolff, Burkhart 3 Ahrendt, Wolfgang 3 Kovács, Laura Ildikó 3 Leavens, Gary T. 3 Logozzo, Francesco 3 Naumann, David A. 3 Parkinson, Matthew J. 3 Pinto, Jorge Sousa 2 Anureev, Igor’ Sergeevich 2 Apt, Krzysztof Rafal 2 de Moura, Leonardo 2 Drossopoulou, Sophia Chloe 2 Eisenbach, Susan 2 Frade, Maria João 2 Furia, Carlo Alberto 2 Garg, Pranav 2 Gurfinkel, Arie 2 Hawblitzel, Chris 2 Hobor, Aquinas 2 Hoenicke, Jochen 2 Jacobs, Bart 2 Klebanov, Vladimir 2 Madhusudan, Parthasarathy 2 Marché, Claude 2 Meyer, Bertrand 2 Moskal, Michał 2 Moy, Yannick 2 Olderog, Ernst-Rüdiger 2 Petrank, Erez 2 Piessens, Frank 2 Podelski, Andreas 2 Qadeer, Shaz 2 Rümmer, Philipp 2 Schäf, Martin 2 Strichman, Ofer 2 Stump, Aaron 2 Utting, Mark 2 Vojdani, Vesal 2 Weiss, Benjamin 1 Abbasi, Rosa 1 Ábrahám, Erika 1 Aït Mohamed, Otmane 1 Alkassar, Eyad 1 Amighi, Afshin 1 Bao, Yuyan 1 Barrett, Clark W. 1 Barros, José Bernardo 1 Barthe, Gilles 1 Baxter, James 1 Bhargavan, Karthikeyan 1 Birkedal, Lars 1 Bjørner, Nikolaj S. 1 Blanchette, Jasmin Christian 1 Blom, Stefan 1 Bobot, François 1 Boston, Brett 1 Boström, Pontus 1 Bouillaguet, Quentin 1 Boulmé, Sylvain 1 Breese, Samuel 1 Brucker, Achim D. 1 Burel, Guillaume 1 Bury, Guillaume 1 Cachera, David 1 Cauderlier, Raphaël 1 Chaki, Sagar 1 Chakraborty, Supratik 1 Chalin, Patrice 1 Chen, Juan 1 Chin, Wei-Ngan 1 Christensen, Michael F. 1 Cogumbreiro, Tiago 1 Collingbourne, Peter 1 Condit, Jeremy 1 Corzilius, Florian 1 Cousot, Patrick 1 Cousot, Radhia 1 da Cruz, Daniela 1 Dailler, Sylvain 1 Darabi, Saeed 1 Darulova, Eva 1 Daum, Matthias 1 De Angelis, Emanuele 1 de Boer, Frank S. 1 De Gouw, Stijn 1 Delahaye, David 1 Demange, Delphine 1 Dockins, Robert 1 Dodds, Joey 1 Dodds, Mike 1 Donaldson, Alastair F. 1 Dörrenbächer, Jan ...and 149 more Authors all top 5 Cited in 20 Serials 13 Journal of Automated Reasoning 9 Formal Aspects of Computing 9 Formal Methods in System Design 5 Logical Methods in Computer Science 2 ACM Computing Surveys 2 Science of Computer Programming 2 Joint Bulletin of the Novosibirsk Computing Center (NCC) and A. P. Ershov Institute of Informatics Systems (IIS). Series: Computer Science 2 Lecture Notes in Computer Science 1 Journal of Computer and System Sciences 1 Programming and Computer Software 1 Theoretical Computer Science 1 Journal of Symbolic Computation 1 Journal of Functional Programming 1 Journal of the ACM 1 Higher-Order and Symbolic Computation 1 Theory and Practice of Logic Programming 1 ACM Transactions on Computational Logic 1 Dissertationes Mathematicae Universitatis Tartuensis 1 Computer Science Review 1 Journal of Logical and Algebraic Methods in Programming all top 5 Cited in 6 Fields 117 Computer science (68-XX) 22 Mathematical logic and foundations (03-XX) 3 General and overarching topics; collections (00-XX) 2 Numerical analysis (65-XX) 1 Operations research, mathematical programming (90-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year