*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Leon: an automated system for verifying Scala code, now with support for Isabelle*From*: "Lars Hupel" <hupel at in.tum.de>*Date*: Wed, 16 Sep 2015 11:12:51 +0200*Importance*: Normal*Reply-to*: hupel at in.tum.de*User-agent*: Host Europe Webmailer/1.0

I'm happy to announce that the Leon system, developed by Viktor Kuncak and his lab at EPFL, has gained support for Isabelle. Leon is an automated system for verifying Scala code. You can find more details on its website [0], try it out online [1], read the sources [2] and the documentation [3]. In a nutshell, it reads a proper (functional) subset of Scala and is able to verify assertions in the program. Via desugaring, it also supports some imperative features. Aside from verification, it can also find counterexamples (should the assertions not hold), and attempt to synthesize & repair programs. The underlying proof obligations are solved with the automated theorem provers Z3 and CVC4. In the past couple of weeks, Isabelle has been connected to Leon; that is, proof obligations can be passed to Isabelle, giving users access to the vast library of mathematical/programming formalisms which are already available in Isabelle and increasing trustworthiness of the proofs. It is also possible to convert Scala code into Isabelle code, whereas previously, only the opposite direction was supported. For this connection, Makarius' PIDE technology is used (sometimes somewhat creatively, I have to admit). The work is now fully integrated into Leon. Here's an example of what can be proven: @isabelle.proof(method = """(induct "<var xs>", auto)""") def lemma[A, B, C](xs: List[A], f: A => List[B], g: B => List[C]) = (xs.flatMap(f).flatMap(g) == xs.flatMap(x => f(x).flatMap(g))).holds ... being the associativity law of the List monad. While this is an example requiring explicit proof, many other properties can be proven without an annotation. Note that in the above snippet, the "method" is an actual Isar proof method. It is also possible to include larger snippets of theory sources into Scala sources. Some technical details are outlined in a presentation [4]. [0] http://lara.epfl.ch/w/leon [1] http://leon.epfl.ch/ [2] https://github.com/epfl-lara/leon [3] http://leon.epfl.ch/doc/ [4] https://speakerdeck.com/larsrh/translating-scala-programs-to-isabelle-with-leon

- Previous by Date: [isabelle] Notation for series coefficients
- Next by Date: Re: [isabelle] Notation for series coefficients
- Previous by Thread: Re: [isabelle] Notation for series coefficients
- Next by Thread: [isabelle] Isabelle Foundation & Certification
- Cl-isabelle-users September 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list