E. Clarke, A. Emerson, and J. Sifakis, Model checking, Communications of the ACM, vol.52, issue.11, 2007.
DOI : 10.1145/1592761.1592781

A. Coq and /. Inria, The Coq proof assistant
URL : https://hal.archives-ouvertes.fr/inria-00069919

S. Evangelista, Méthodes et outils de vérification pour les réseaux de Petri de haut niveau, CNAM, 2006.

L. Fronc, Analyse efficace des réseaux de Petri par des techniques de compilation Master's thesis, MPRI, university of Paris 7, 2010.

L. Fronc and F. Pommereau, Proving a Petri net model-checker implementation, 2010.

L. Fronc and F. Pommereau, Optimizing the compilation of Petri nets models, Proc. of SUMo'11, 2011.

G. J. Holzmann, D. Peled, and M. Yannakakis, On nested depth-first search, Proc. of the 2nd Spin Workshop, 1996.

K. Jensen and L. M. Kristensen, Coloured Petri Nets: Modelling and Validation of Concurrent Systems, 2009.

C. Lattner, LLVM language reference manual

C. Lattner, The LLVM compiler infrastructure

C. Lattner, LLVM related publications

C. Pajault and S. Evangelista, Helena: a high level net analyzer

L. Paulson, T. Nipkow, and M. Wenzel, The Isabelle proof assistant

F. Pommereau, Quickly prototyping Petri nets tools with SNAKES. Petri net newsletter, 2008.

C. Reinke, Haskell-Coloured Petri Nets, IFL'99, 1999.
DOI : 10.1007/10722298_10

X. Rival, Traces Abstraction in Static Analysis and Program Transformation Abstraction de Traces en Analyse Statique et Transformations de Programmes, 2005.

K. N. Verma, J. Goubault-larrecq, S. Prasad, and S. Arun-kumar, Reflecting BDDs in Coq, ASIAN'00, 1961.
DOI : 10.1007/3-540-44464-5_13

URL : https://hal.archives-ouvertes.fr/inria-00072797