Skip to content

A model checker and assume/guarantee contract generator for Lustre programs.

License

Notifications You must be signed in to change notification settings

coco-team/zustre

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

90 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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

About

A model checker and assume/guarantee contract generator for Lustre programs.

Topics

Resources

License

Stars

Watchers

Forks

Packages

No packages published