Lab for Automated Reasoning and Analysis LARA

LAB 01 : Introduction to leon

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

The Web interface is accessible at:

http://lara.epfl.ch/leon/tutorials

Leon Package

A tentative self-contained release is available here:

leon.tar.bz2.

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

Note

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

 
sav13/labs_01.txt · Last modified: 2013/04/24 16:30 by ekneuss
 
© EPFL 2018 - Legal notice