P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles et al., Frama-C a software analysis perspective, p.2012

F. Loulergue, F. Gava, N. Kosmatov, and M. Lemerre, , p.2012

M. Lemerre, V. David, and G. Vidal-naquet, A communication mechanism for resource isolation, Proceedings of the Second Workshop on Isolation and Integration in Embedded Systems, IIES '09, 2009.
DOI : 10.1145/1519130.1519131
URL : https://hal.archives-ouvertes.fr/hal-00471460

M. Lemerre, V. David, and G. Vidal-naquet, A dependable kernel design for resource isolation and protection, p.2010
URL : https://hal.archives-ouvertes.fr/hal-00517703

M. Lemerre, E. Ohayon, D. Chabrol, M. Jan, and M. B. Jacques, Method and Tools for Mixed-Criticality Real-Time Applications within PharOS, 2011 14th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing Workshops, 2011.
DOI : 10.1109/ISORCW.2011.15

Y. Moy, Automatic Modular Static Safety Checking for C Programs, 2009.

N. Williams, B. Marre, P. Mouy, and M. Roger, PathCrawler: Automatic Generation of Path Tests by Combining Static and Dynamic Analysis, 2005.
DOI : 10.1007/11408901_21
URL : https://hal.archives-ouvertes.fr/hal-01810201

B. Botella, M. Delahaye, S. Hong-tuan-ha, N. Kosmatov, P. Mouy et al., Automating structural testing of C programs: Experience with PathCrawler, 2009 ICSE Workshop on Automation of Software Test, 2009.
DOI : 10.1109/IWAST.2009.5069043
URL : https://hal.archives-ouvertes.fr/hal-01810197

M. Lemerre, Intégration de systèmes hétérogènes en termes de niveaux de sécurité, 2009.

N. Williams and N. Kosmatov, Structural Testing with PathCrawler: Tutorial Synopsis, 2012 12th International Conference on Quality Software, p.2012
DOI : 10.1109/QSIC.2012.24
URL : https://hal.archives-ouvertes.fr/hal-01810295

G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock et al., seL4, Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, SOSP '09, 2009.
DOI : 10.1145/1629575.1629596

E. Alkassar, W. Paul, A. Starostin, and A. Tsyban, Pervasive Verification of an OS Microkernel, 2010.
DOI : 10.1007/978-3-642-15057-9_5

E. Alkassar, M. A. Hillebrand, W. J. Paul, and E. Petrova, Automated Verification of a Small Hypervisor, 2010.
DOI : 10.1007/978-3-642-15057-9_3

E. Alkassar, E. Cohen, M. Kovalev, and W. J. Paul, Verification of TLB Virtualization Implemented in C, p.2012
DOI : 10.1145/1629575.1629596
URL : http://www-wjp.cs.uni-saarland.de/publikationen/ACKP12.pdf

G. Klein, From a Verified Kernel towards Verified Systems, p.2010
DOI : 10.1145/1806596.1806610
URL : http://www.cse.unsw.edu.au/%7Ekleing/papers/aplas10.pdf