AstraVer Toolset

AstraVer Toolset is built on top of 'Frama-C + Jessie plugin + Why3' deductive verification toolchain, so it can be used to prove properties of Linux kernel code.

Jessie2 is a fork of the Jessie plug-in for Frama-C that allows deductive verification of C programs annotated with ACSL and is primarily targeted at Linux kernel modules source code. It uses the language and tools of the Why3 verification platform. Unlike original Jessie, Jessie2 is not distributed as a part of the Why2 verification platform and is compiled/installed separately.
Note: For now, this fork requires modified version of the Frama-C source code analysis platform, that is based on the Sodium 20150201 version of the original platform.


Using OPAM

  • Install OPAM as described on the OPAM documentation.
    For example (installing to /usr/local/bin unsing the binary installer):
        chmod +x
        sudo ./ /usr/local/bin
  • Initialize OPAM to use the OCaml 4.03.0 compiler:
        opam init --comp 4.03.0
        eval `opam config env`
  • Install Git.
    For example on Ubuntu:
        sudo apt-get install git
  • Add ISPRAS OPAM repository at with Jessie2 and modified Frama-C Sodium packages to the OPAM installation
    (ispras is just an arbitrary name of the new repository):
        opam repo add ispras
  • Install external dependencies for the Jessie2 and Frama-C build i.e. Autoconf, Gtk2 development files and M4.
    Ubuntu example:
        sudo apt-get install $(opam install -e ubuntu jessie2)
  • Build and install the Jessie2 plugin for Frama-C with OPAM (the Frama-C itself will be built and installed automatically). One
    can use the -j option to speed-up compilation on a multi-core machine:
        opam install -j 4 jessie2
  • Build and install either original or patched (search in task view, empty theory filtering) version of the Why3 verification platform:
        sudo apt-get install $(opam install -e ubuntu why3) # Install GMP (external dependency) on Ubuntu
        opam install -j 4 why3
  • The one using Jessie would also likely need SMT solvers e.g. Alt-Ergo (also Z3, CVC4 and others). Alt-Ergo can be installed via OPAM:
         opam install alt-ergo altgr-ergo satML-plugin
  • The Why3 IDE should be initialized to detect available provers (and plugins):
        why3 config --detect-provers --detect-plugins

Our Repositories

  • Jessie2 (git clone has the following branches:
    -- master -- references the latest released version of the Jessie2 plugin (currently `astraver-v1.1')
  • QA (git clone is a submodule of the Jessie2 repository. It contains several new test sets and the corresponding new testing script (in OCaml) that is based on the Why3 proof replayer.
  • Frama-C (git clone has two branches:
    -- master -- this is a dummy branch with each commit corresponding to an upstream release of Frama-C starting from "Sodium 20150201" (framac|1db5542e)
    -- 20150201 -- references patched version of Frama-C Sodium 20150201 required by the latest Jessie2 (astraver-v1.1) with some significant changes (wrap-around annotations and logic operations on bounded integers, annotation importing -- an order-independent merging of annotations from several C source files)
  • Why3 (git clone has two branches:
    -- master -- a periodically updated mirror of the INRIA official Why3 Git repository's master branch
    -- patched -- the periodically merged patched version of the Why3 platform with several small unmerged changes
  • OPAM-repository (git clone is the above mentioned OPAM repository