LAB 01 : Introduction to leon

We will introduce you to the Leon online interface to verify programs.

The Web interface is accessible at:

A tentative self-contained release is available here:

This packaged version has been tested for x86_64 and OSX 64b, we would love to hear from you if it works or fails on your setup.

Once extracted, you can use leon as follows:

  $ cd path/to/extracted/
  $ ./leon --xlang examples/01_Introduction.scala

You can specify one function in particular to analyze using the –functions parameter:

  $ ./leon --functions=contains --xlang examples/01_Introduction.scala

Another impotant option is the –timeout one which limits the time (in seconds) a solver can spend on a verification condition.

  $ ./leon --functions=contains --xlang --timeout=1 examples/01_Introduction.scala

If you experience errors such as: java.util.NoSuchElementException: None.get , make sure you included the –xlang option.