Skip to Main content Skip to Navigation
Conference papers

PIC2LNT: Model Transformation for Model Checking an Applied Pi-Calculus

Radu Mateescu 1, * Gwen Salaün 1 
* Corresponding author
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : In this paper, we present an applied pi-calculus obtained by extending Milner's pi-calculus with data types and expressions. The applied pi-calculus is automatically translated to the LNT value-passing process specification language by means of the PIC2LNT 2.0 tool. This enables the verification of applied pi-calculus specifications by using the data-based temporal logics and the model checkers of the CADP toolbox.
Complete list of metadata

Cited literature [12 references]  Display  Hide  Download
Contributor : Radu Mateescu Connect in order to contact the contributor
Submitted on : Thursday, March 28, 2013 - 10:35:20 AM
Last modification on : Tuesday, August 2, 2022 - 4:24:37 AM
Long-term archiving on: : Saturday, June 29, 2013 - 4:02:57 AM


Files produced by the author(s)



Radu Mateescu, Gwen Salaün. PIC2LNT: Model Transformation for Model Checking an Applied Pi-Calculus. TACAS - 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - 2013, Mar 2013, Rome, Italy. pp.192-198, ⟨10.1007/978-3-642-36742-7_14⟩. ⟨hal-00805533⟩



Record views


Files downloads