You will find in this page instructions on how to install Alt-Ergo and Frama-C. The instructions provided here should work on an Ubuntu/Debian system. Do not hesitate to contact C. Garion if you have problems to install the required softwares or want to install them on a different distribution.

Panda installation

If you want to use the Panda software to prove formulas using natural deduction, you can download it here. The JAR of Panda is also locally available here.

OPAM installation

OPAM is a package manager for OCaml softwares like pip for Python or gem for Ruby. By installing it, you will be able to install all the needed softwares for the course automatically.

Please go the Quick Install page and follow the instructions to install OPAM on your computer (for Ubuntu, use the "Installing OPAM with your distribution instructions"). If you are using the last version of Ubuntu, you may have to change the /etc/apt/sources.list.d/avsm-ppa-saucy.list by replacing saucy in the file by raring.

Do not forget to initialize and update OPAM by executing the following command in a terminal:

  opam init
  opam update

Follow the instructions to include the applications installed in ~/.opam in your path.

Softwares installation

To install softwares, you just have to execute the following command in a terminal (and take a coffee, the compilation process is rather long...):

  opam install alt-ergo frama-c

Beware, on a fresh Ubuntu/Debian install, you will have to install before the following Ubuntu/Debian packages:

Configure why3 using the following command:

  why3config --detect

Do not bother with the warnings during configuration of why3.

Verifying installation

To verify installation, use this simple annotated C program. The following invocation of the Frama-C WP plugin should produce a similar result on your machine:

[tof@suntof] ~ % frama-c -wp swap.c

[kernel] preprocessing with "gcc -C -E -I.  swap.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 5 goals scheduled
[wp] [Qed] Goal typed_swap_post_2 : Valid
[wp] [Qed] Goal typed_swap_assign_part1 : Valid
[wp] [Alt-Ergo] Goal typed_swap_assign_part3 : Valid (8ms) (19)
[wp] [Alt-Ergo] Goal typed_swap_assign_part2 : Valid (20ms) (19)
[wp] [Alt-Ergo] Goal typed_swap_post : Valid (20ms) (11)