RESY: Requirement Synthesis for Compositional Model Checking

Current version: 1.6
Copyright © 2007 Saarland University


The requirement synthesis tool RESY automatically computes environment assumptions for compositional model checking. Given a process M in a multi-process PROMELA program, an abstraction refinement loop computes a coarse equivalence relation on the states of the environment, collapsing two states if the environment of M can either force the occurrence of an error from both states or from neither state. RESY supports three different operation modes: assumption generation, compositional model checking, and front-end to the model checker SPIN. In assumption generation mode, RESY minimizes the size of the assumption; small assumptions are useful for program documentation and as certificates for re-verification. In compositional model checking mode, RESY terminates as soon as the property is proven or disproven, independently of the size of the assumption. In front-end mode, RESY terminates when the size of the assumption falls below a specified threshold, and calls SPIN with the simplified verification problem.

Industrial Partner

RESY was developed in cooperation with our industrial partner META-LEVEL Software AG.

Operation Modes


You can download and use RESY under the terms of the following LICENSE.


For bug reports please contact Hans-Jörg Peter.