The translator allows behavioural control-flow properties of programs to be transformed into equivalent sets of structural ones.
The specification language is the fragment of the modal mu-calculus with boxes and greatest fixed points only.
The theory behind the translator is presented in the following technical report. More background and related work can be found at the CVPP project web page.
| Atomic proposition | ap ::= | r | ff | tt | meth |
| Box label | l ::= | tau | meth call meth | meth ret meth |
| Property | phi ::= | ap | not ap | (phi) | phi /\ phi | phi \/ phi | [l]phi | prop_var | nu prop_var . phi |
where meth is a string starting with a lower case, while prop_var is a string starting with an upper case.
Interfaces are given as a list of method names, separated by spaces only.
Fill out the form below, i.e. select a predefined property, or enter your own (and select it!), and select a predefined interface, or enter your own (and select it!), and press "show result".
Most of the predefined properties have been taken from the technical report.