A model checker and assume/guarantee contract generator for Lustre programs.
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
cmake
src merge master with devel Mar 22, 2017
tests
.travis.yml
CMakeLists.txt
LICENSE
README.md

README.md

Build Status

Zustre

Zustre is a modular SMT-based PDR-style verification engine for Lustre programs. It is also an engine to generate mode-aware assume-guarantee style formal contract.

##License## Zustre is distributed under a modified BSD license. See LICENSE for details.

Demo

asciicast

Dependencies

Compilation

  • Build separately LustreC
  • cd zustre ; mkdir build ; cd build
  • cmake -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=run -DLUSTREC_ROOT=LUSTREC_DIR ../ where LUSTREC_DIR is the directory containing LustreC. Note that you need to compile LustreC separately beforehand.
  • cmake --build . to build zustre
  • cmake --build . --target install to install everything in run directory
  • cmake --build . --target package to package everything.
  • (Optional) To use Eldarica just copy the eldarica binary under build/run/bin

Zustre and dependencies are installed under build/run

Usage

  • To simply verify Lustre code:
>  ./build/run/bin/zustre [LUSTRE_FILE] --node [OBSERVER NODE (default: top)]
  • To generate CoCoSpec contract of Lustre code:
> ./build/run/bin/zustre [LUSTRE_FILE] --cg --node [OBSERVER NODE (default: top)]
  • To use Eldarica as the backend solver:
> ./build/run/bin/zustre --eldarica [LUSTRE_FILE] --node [OBSERVER NODE (default: top)]

Options

  • -h, --help show this help message and exit
  • --pp Enable default pre-processing
  • --trace TRACE Trace levels to enable
  • --stat Print statistics
  • --verbose Verbose
  • --no-simp Z3 simplification
  • --node NODE Specify top node (default:top)
  • --cg Generate modular contrats
  • --smt2 Directly encoded file in SMT2 Format
  • --no-solving Generate only Horn clauses, i.e. do not solve
  • --xml Output result in XML format
  • --save Save intermediate files
  • --no-dl Disable Difference Logic (UTVPI) in SPACER
  • --timeout TIMEOUT Set timeout for solving
  • --eldarica Use Eldarica as the backend solver

Contact