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.

This software is also peer reviewed by journal TOMS.

References in zbMATH (referenced in 11 articles )

Showing results 1 to 11 of 11.
Sorted by year (citations)

  1. Bansal, Kshitij; Barrett, Clark; Reynolds, Andrew; Tinelli, Cesare: Reasoning with finite sets and cardinality constraints in SMT (2018)
  2. Melquiond, Guillaume; Rieu-Helft, Raphaël: A Why3 framework for reflection proofs and its application to GMP’s algorithms (2018)
  3. Reynolds, Andrew; Viswanathan, Arjun; Barbosa, Haniel; Tinelli, Cesare; Barrett, Clark: Datatypes with shared selectors (2018)
  4. Amin, Nada; Rompf, Tiark: LMS-verify: abstraction without regret for verified systems programming (2017)
  5. Inala, Jeevana Priya; Polikarpova, Nadia; Qiu, Xiaokang; Lerner, Benjamin S.; Solar-Lezama, Armando: Synthesis of recursive ADT transformations from reusable templates (2017)
  6. Bansal, Kshitij; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare: A new decision procedure for finite sets and cardinality constraints in SMT (2016)
  7. Hupel, Lars; Kuncak, Viktor: Translating scala programs to isabelle/HOL. System description (2016)
  8. Pham, Tuan-Hung; Gacek, Andrew; Whalen, Michael W.: Reasoning about algebraic data types with abstractions (2016)
  9. Reynolds, Andrew; Blanchette, Jasmin Christian; Cruanes, Simon; Tinelli, Cesare: Model finding for recursive functions in SMT (2016)
  10. Tschannen, J.; Furia, CA; Nordio, M.; Polikarpova, N.: AutoProof: Auto-active Functional Verification of Object-oriented Programs (2015) arXiv
  11. Kuncak, Viktor: Verifying and synthesizing software with recursive functions (invited contribution) (2014)