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

Dependencies

LustreC (Lustre compiler)
SPACER (PDR engine)
(Optional) Eldarica (Horn Clause solver)
Python v. 2.7. (or up)

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

Temesghen Kahsai (NASA Ames / CMU)
Arie Gurfinkel (SEI / CMU)