Leon: an automated system for verifying Scala code, now with support for Isabelle

classic Classic list List threaded Threaded
1 message Options
Reply | Threaded
Open this post in threaded view
|

Leon: an automated system for verifying Scala code, now with support for Isabelle

Lars Hupel-2
I'm happy to announce that the Leon system, developed by Viktor Kuncak and his lab at EPFL, has gained support for Isabelle.

What is this about? In a nutshell:

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 [4] and CVC4 [5].

Isabelle is an interactive theorem prover. It is used for formal specification & proofs. An overview can be found on its website [6]. Some of the readers of this list might be familiar with Coq; both systems serve similar purposes. The main mode of interaction with Isabelle is via its IDE; users type in specifications and proofs which are being checked continuously. It offers automated proof and disproof methods, various decision procedures, executable code generation, a rich library of classical mathematics and much more.

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. It is also possible to convert Scala code into Isabelle code, whereas previously, only the opposite direction was supported. (As a side note: Isabelle was one of the first notable software systems making use of Scala.)

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.

I encourage everyone to play with the system(s); both the Isabelle and the Leon teams are always happy about feedback. All of this is freely available under open source licenses.

PS: Some technical details are outlined in a presentation [7].

[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://github.com/Z3Prover/z3
[5] http://cvc4.cs.nyu.edu/web/
[6] https://isabelle.in.tum.de/overview.html
[7] https://speakerdeck.com/larsrh/translating-scala-programs-to-isabelle-with-leon

--
You received this message because you are subscribed to the Google Groups "scala-announce" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
For more options, visit https://groups.google.com/d/optout.