From behavioural to structural properties:
A tool web interface

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.

Property and interface grammar

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.

Property: nu X. ([a call b] ff) /\ ([tau] X) /\ ([a call a] X) /\ ([a ret a] X)
Interface: a b

Enter a behavioural property and an interface of provided methods: