Output details

A Practical Approach to Verification of Mobile Systems Using Net Unfoldings

<04> This paper identifies a pi-Calculus fragment, called Safe Finite Control Processes (SFCP), admitting efficient translation to safe Petri nets, for which efficient verification techniques exist. Moreover, it develops a translation from Finite Control Processes (FCP) -commonly used pi-Calculus fragment- to SFCPs. These translations have been implemented, and the experiments show that the proposed approach has significant advantages over other existing tools in terms of memory consumption and runtime. This paper was selected for journal publication as one of the best papers of Petri Nets'08. A PhD studentship was provided by the School to further develop this line of research.