Blanc, RégisKneuss, EtienneKuncak, ViktorSuter, Philippe2014-04-252014-04-252014-04-25201310.1145/2489837.2489838https://infoscience.epfl.ch/handle/20.500.14299/102949We 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.text::conference output::conference paper not in proceedings