From behavioural to structural properties: A tool web interface

[Note: this page provides a slightly refined interface to the translator running at]

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.

The Translator

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.

nu X. ([a call b] X) /\ [b ret a](not r /\ X)
nu X. ([a call b] ff) /\ ([a call a] X) /\ ([a ret a] X)
nu X. ([a call b] ff) /\ ([tau] X) /\ ([a call a] X) /\ ([a ret a] X)
[a call b](nu X. r /\ [b ret a](not r /\ [a call b] X))
nu Y.[a ret a](not r /\ Y) /\ ([tau] X) /\ [a call a] X

a b
b a

Powered by puptol. Visit your puptol session overview.