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)