Leon swMATH ID: 9159 Software Authors: Régis Blanc; Viktor Kuncak; Etienne Kneuss; Philippe Suter Description: An overview of the Leon verification system: verification by translation to recursive functions. We present the Leon verification system for a subset of the Scala programming language. Along with several functional features of Scala, Leon supports imperative constructs such as mutations and loops, using a translation into recursive functional form. Both properties and programs in Leon are expressed in terms of user-defined functions. We discuss several techniques that led to an efficient semi-decision procedure for first-order constraints with recursive functions, which is the core solving engine of Leon. We describe a generational unrolling strategy for recursive templates that yields smaller satisfiable formulas and ensures completeness for counterexamples. We illustrate the current capabilities of Leon on a set of examples, such as data structure implementations; we show that Leon successfully finds bugs or proves completeness of pattern matching as well as validity of function postconditions. Homepage: http://dl.acm.org/citation.cfm?id=2489838 Related Software: CVC4; Dafny; z3; Isabelle/HOL; SMT-LIB; Why3; Spec#; SIMPLIFY; Sledgehammer; Scala; CIRC; CPAchecker; HolBA; SeaHorn; GNATprove; RGITL; EiffelBase2; Boogie; CodeContracts; VeriFast Cited in: 12 Publications all top 5 Cited by 25 Authors 4 Reynolds, Andrew 4 Tinelli, Cesare 3 Barrett, Clark W. 2 Bansal, Kshitij 2 Kuncak, Viktor 1 Amin, Nada 1 Barbosa, Haniel 1 Blanchette, Jasmin Christian 1 Cruanes, Simon 1 Ernst, Gidon 1 Gacek, Andrew 1 Hupel, Lars 1 Inala, Jeevana Priya 1 Itzhaky, Shachar 1 Lerner, Benjamin S. 1 Melquiond, Guillaume 1 Pham, Tuan-Hung 1 Polikarpova, Nadia 1 Qiu, Xiaokang 1 Rieu-Helft, Raphaël 1 Rompf, Tiark 1 Singher, Eytan 1 Solar-Lezama, Armando 1 Viswanathan, Arjun 1 Whalen, Michael W. Cited in 2 Serials 1 Journal of Automated Reasoning 1 Logical Methods in Computer Science Cited in 2 Fields 12 Computer science (68-XX) 2 Mathematical logic and foundations (03-XX) Citations by Year