Leon: an automated system for verifying Scala code, now with support for Isabelle
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 , try it out online , read the sources  and the documentation . 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 .
Isabelle is an interactive theorem prover. It is used for formal specification & proofs. An overview can be found on its website . 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.)
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.