Boogie swMATH ID: 7714 Software Authors: Leino, K. Rustan M. 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#; Dafny; KRAKATOA; VCC; ESC/Java; Caduceus; Coq; JML; Isabelle/HOL; VeriFast; SIMPLIFY; Eiffel; WhyML; SMT-LIB; CVC4; KeY; Frama-C; Viper Cited in: 130 Documents all top 5 Cited by 282 Authors 12 Leino, K. Rustan M. 8 Müller, Peter 6 Summers, Alexander J. 5 Böhme, Sascha 4 Banerjee, Anindya 4 Lahiri, Shuvendu Kumar 4 Schulte, Wolfram 4 Ulbrich, Mattias 4 Wolff, Burkhart 3 Ahrendt, Wolfgang 3 De Angelis, Emanuele 3 Fioravanti, Fabio 3 Garg, Pranav 3 Kovács, Laura Ildikó 3 Leavens, Gary T. 3 Logozzo, Francesco 3 Madhusudan, Parthasarathy 3 Naumann, David A. 3 Parkinson, Matthew J. 3 Pettorossi, Alberto 3 Pinto, Jorge Sousa 3 Proietti, Maurizio 2 Anureev, Igor’ Sergeevich 2 Apt, Krzysztof Rafal 2 Barrett, Clark W. 2 de Moura, Leonardo 2 Drossopoulou, Sophia Chloe 2 Eisenbach, Susan 2 Ene, Cristian 2 Frade, Maria João 2 Furia, Carlo Alberto 2 Gurfinkel, Arie 2 Hawblitzel, Chris 2 Hoenicke, Jochen 2 Jacobs, Bart 2 Klebanov, Vladimir 2 Marché, Claude 2 Meyer, Bertrand 2 Moskal, Michał 2 Mounier, Laurent 2 Moy, Yannick 2 Neider, Daniel 2 Olderog, Ernst-Rüdiger 2 Petrank, Erez 2 Petri, Gustavo 2 Piessens, Frank 2 Podelski, Andreas 2 Potet, Marie-Laure 2 Qadeer, Shaz 2 Reynolds, Andrew 2 Rümmer, Philipp 2 Saha, Shambwaditya 2 Schaefer, Ina 2 Schäf, Martin 2 Strichman, Ofer 2 Stump, Aaron 2 Tinelli, Cesare 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 Barros, José Bernardo 1 Barthe, Gilles 1 Batista Ribeiro, Leandro 1 Baunach, Marcel 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 Bordis, Tabea 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 ...and 182 more Authors all top 5 Cited in 20 Serials 14 Journal of Automated Reasoning 9 Formal Aspects of Computing 9 Formal Methods in System Design 6 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 Theory and Practice of Logic Programming 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 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 130 Computer science (68-XX) 22 Mathematical logic and foundations (03-XX) 3 General and overarching topics; collections (00-XX) 2 Numerical analysis (65-XX) 2 Operations research, mathematical programming (90-XX) 2 Information and communication theory, circuits (94-XX) Citations by Year