From behavioural to structural properties:
The translator allows behavioural control-flow properties of programs
to be transformed into equivalent sets of structural ones.
A tool web interface
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
More background and related work can be found at the
CVPP project web page.
Property and interface grammar
r | ff | tt | meth
tau | meth call meth | meth ret meth
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: