Why3 swMATH ID: 4438 Software Authors: François Bobot; Jean-Christophe Filliâtre; Claude Marché; Guillaume Melquiond; Andrei Paskevich Description: Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs. Why3 is a complete reimplementation of the former Why platform. Among the new features are: numerous extensions to the input language, a new architecture for calling external provers, and a well-designed API, allowing to use Why3 as a software library. An important emphasis is put on modularity and genericity, giving the end user a possibility to easily reuse Why3 formalizations or to add support for a new external prover if wanted. Homepage: http://why3.lri.fr/ Keywords: program verification Related Software: Coq; KRAKATOA; z3; Caduceus; WhyML; Boogie; Isabelle/HOL; Dafny; Spec#; JML; Frama-C; VCC; VeriFast; Isabelle; CVC4; SIMPLIFY; cvc3; ESC/Java; TPTP; Alt-Ergo Cited in: 144 Documents Further Publications: http://why3.lri.fr/#publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Why3 – where programs meet provers. Zbl 1435.68366Filliâtre, Jean-Christophe; Paskevich, Andrei 2013 all top 5 Cited by 267 Authors 10 Marché, Claude 9 Filliâtre, Jean-Christophe 7 Melquiond, Guillaume 6 Blanchette, Jasmin Christian 6 Leino, K. Rustan M. 5 Böhme, Sascha 5 Pinto, Jorge Sousa 5 Rieu-Helft, Raphaël 4 Bentkamp, Alexander 4 Boldo, Sylvie 4 Kaliszyk, Cezary 4 Moy, Yannick 4 Paskevich, Andrei 4 Vukmirović, Petar 3 Chen, Ran 3 Cruanes, Simon 3 De Angelis, Emanuele 3 Fioravanti, Fabio 3 Frade, Maria João 3 Müller, Peter 3 Nummelin, Visa 3 Pettorossi, Alberto 3 Proietti, Maurizio 3 Smallbone, Nicholas 3 Swamy, Nikhil 3 Théry, Laurent 3 Tourret, Sophie 3 Wies, Thomas 3 Wolff, Burkhart 2 Ahrendt, Wolfgang 2 Arusoaie, Andrei 2 Barbosa, Manuel 2 Benzaken, Véronique 2 Bhargavan, Karthikeyan 2 Bian, Jinting 2 Chaudhari, Dipak L. 2 Chechik, Marsha 2 Clément, François 2 Clochard, Martin 2 Conchon, Sylvain 2 Contejean, Evelyne 2 Cristiá, Maximiliano 2 Damani, Om P. 2 de Boer, Frank S. 2 De Gouw, Stijn 2 Fournet, Cédric 2 Giorgino, Mathieu 2 Gondelman, Léon 2 Halmagrand, Pierre 2 Hiep, Hans-Dieter A. 2 Hriţcu, Cătălin 2 Khan, Muhammad Taimoor 2 Kobayashi, Naoki 2 Lammich, Peter 2 Levy, Jean-Jacques 2 Lourenço, Cláudio Belo 2 Mayero, Micaela 2 Peña, Ricardo 2 Popescu, Andrei 2 Rastogi, Aseem 2 Reynolds, Andrew 2 Rossi, Gianfranco 2 Roşu, Grigore 2 Rusu, Vlad 2 Schreiner, Wolfgang 2 Schulte, Wolfram 2 Siegel, Stephen F. 2 Strecker, Martin 2 Strub, Pierre-Yves 2 Summers, Alexander J. 2 Ulbrich, Mattias 2 Urban, Josef 2 Weis, Pierre 2 Zhan, Bohua 2 Zirkel, Timothy K. 1 Abbasi, Rosa 1 Abed, Sa’ed 1 Affeldt, Reynald 1 Ahman, Danel 1 Aït Mohamed, Otmane 1 Alkassar, Eyad 1 Anureev, Igor’ Sergeevich 1 Armstrong, Alasdair 1 Aspinall, David 1 Ayad, Ali 1 Bacelar Almeida, José 1 Bansal, Kshitij 1 Baro, Sylvain 1 Barrett, Clark W. 1 Bautista, Santiago 1 Baxter, James 1 Berghammer, Rudolf 1 Beringer, Lennart 1 Bertot, Yves 1 Blazy, Sandrine 1 Blot, Arthur 1 Bobot, François 1 Boström, Pontus 1 Boulmé, Sylvain 1 Brady, Edwin C. ...and 167 more Authors all top 5 Cited in 22 Serials 19 Journal of Automated Reasoning 5 Formal Aspects of Computing 5 Formal Methods in System Design 3 Journal of Symbolic Computation 3 Mathematics in Computer Science 3 Journal of Formalized Reasoning 3 Journal of Logical and Algebraic Methods in Programming 2 Theoretical Computer Science 2 Science of Computer Programming 2 Journal of Functional Programming 2 Theory and Practice of Logic Programming 2 Logical Methods in Computer Science 1 Computers & Mathematics with Applications 1 Journal of Computational and Applied Mathematics 1 Information and Computation 1 Advances in Applied Clifford Algebras 1 Annals of Mathematics and Artificial Intelligence 1 Constraints 1 Joint Bulletin of the Novosibirsk Computing Center (NCC) and A. P. Ershov Institute of Informatics Systems (IIS). Series: Computer Science 1 ACM Transactions on Computational Logic 1 Lecture Notes in Computer Science 1 Computer Science Review all top 5 Cited in 11 Fields 141 Computer science (68-XX) 29 Mathematical logic and foundations (03-XX) 12 Numerical analysis (65-XX) 4 Combinatorics (05-XX) 4 Information and communication theory, circuits (94-XX) 3 Operations research, mathematical programming (90-XX) 2 Number theory (11-XX) 2 Partial differential equations (35-XX) 1 General and overarching topics; collections (00-XX) 1 Linear and multilinear algebra; matrix theory (15-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) Citations by Year