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

Citations by Year