Pierre Courtieu Bibliography

Workshop PATE (Co-organizer), satellite of conference RDP07, June 2007, Paris. Proceedings

[1] Thibaut Balabonski, Pierre Courtieu, Robin Pelle, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Continuous vs. Discrete Asynchronous Moves: a Certified Approach for Mobile Robots. Research report, Sorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6, LIP6, F-75005 Paris, France, 2018. [ bib | http | .pdf ]
[2] Thibaut Balabonski, Pierre Courtieu, Robin Pelle, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Brief Announcement: Continuous vs. Discrete Asynchronous Moves: a Certified Approach for Mobile Robots. In Taisuke Izumi and Petr Kuznetsov, editors, Stabilization, Safety, and Security of Distributed Systems - 20th International Symposium, (SSS 2018), volume 11201 of Lecture Notes in Computer Science, Tokyo, Japan, November 2018. Springer-Verlag. [ bib ]
[3] Thibaut Balabonski, Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Certified Gathering of Oblivious Mobile Robots: Survey of Recent Results and Open Problems. In Laure Petrucci, Cristina Seceleanu, and Ana Cavalcanti, editors, Critical Systems: Formal Methods and Automated Verification - Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems - and - 17th International Workshop on Automated Verification of Critical Systems, (FMICS-AVoCS 2017), volume 10471 of Lecture Notes in Computer Science, pages 165–181, Turin, Italy, September 2017. Springer-Verlag. [ bib ]
[4] Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Brief Announcement: Certified Universal Gathering in R^2 for Oblivious Mobile Robots. In Proceedings of the 2016 ACM Symposium on Principles of Distributed Computing, PODC 2016, Chicago, IL, USA, July 25-28, 2016, pages 439–441, 2016. [ bib | DOI | .pdf ]
[5] Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Certified Universal Gathering in mathbb R ^2 for Oblivious Mobile Robots. In Distributed Computing - 30th International Symposium, DISC 2016, Paris, France, September 27-29, 2016. Proceedings, pages 187–200, 2016. [ bib | DOI | http | .pdf ]
[6] Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. A Certified Universal Gathering Algorithm for Oblivious Mobile Robots. CoRR, abs/1506.01603, 2015. [ bib ]
[7] Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Impossibility of Gathering, a Certification. Information Processing Letters, 115:447–452, 2015. [ bib | DOI | .pdf ]
[8] Béatrice Bérard, Pierre Courtieu, Laure Millet, Maria Potop-Butucaru, Lionel Rieg, Nathalie Sznajder, Sébastien Tixeuil, and Xavier Urbain. [Invited Paper] Formal Methods for Mobile Robots: Current Results and Open Problems. International Journal of Informatics Society, 7(3):101–114, 2015. [ bib | http ]
[9] Pierre Courtieu, Maria Virginia Aponte, Tristan Crolard, Jason Belt Roby, John Hatcliff, Zhi Zhang, Jerome Guitton, and Trevor Jennings. Towards The Formalization of SPARK 2014 Semantics With Explicit Run-time Checks Using Coq . In High Integrity Language Technology ACM SIGAda's Annual International Conference (HILT 2013). ACM, November 2013. [ bib ]
[10] Cédric Auger, Zohir Bouzid, Pierre Courtieu, Sébastien Tixeuil, and Xavier Urbain. Certified Impossibility Results for Byzantine-Tolerant Mobile Robots. In Teruo Higashino et al., editor, 15th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2013), volume 8255 of Lecture Notes in Computer Science, November 2013. To appear. 15 pages. [ bib ]
[11] P. Courtieu, M. Aponte, Y. Moy, and M. Sango. Maximal and Compositional Pattern-Based Loop Invariants. In Formal method 2012 (FME), volume 7436 of lncs, pages 37–51, Paris, France, August 2012. [ bib | .pdf ]
[12] David Baelde, Pierre Courtieu, David Gross-Amblard, and Christine Paulin. Towards Provably Robust Watermarking. In ITP, 2012. [ bib | .pdf ]
[13] Anne-Gwenn Bosser, Pierre Courtieu, Julien Forest, and Marc Cavazza. Structural Analysis of Narratives with the Coq Proof Assistant. In ITP 2011, volume 6898 of LNCS, pages 55–70, 2011. [ bib | .pdf ]
[14] Evelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Automated Certified Proofs with CiME3. In RTA, pages 21–30, 2011. [ bib | .pdf ]
[15] Évelyne Contejean, Pierre Courtieu, and Olivier Pons et Xavier Urbain Julien Forest, Andrei Paskevich. A3PAT, an Approach for Certified Automated Termination Proofs. In In PEPM'10 Proceedings of the 2010 ACM SIGPLAN Symp. on Partial Evaluation and Program Manipulation, 2010. [ bib | .pdf ]
[16] Pierre Courtieu, Gladys Gbedo, and Olivier Pons. Improved Matrix Interpretation. In Jan van Leeuwen et al., editor, In proc. SOFSEM2010, SOFSEM'10, International Conference on Current Trends in Theory and Practice of Computer Science, volume of LNCS, pages 283–295. Springer, 2010. [ bib | .pdf ]
[17] Pierre Courtieu, Julien Forest, and Xavier Urbain. Certifying a Termination Criterion Based on Graphs, Without Graphs. In César Muñoz and Otmane Ait Mohamed, editors, 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs'08), volume 5170 of Lecture Notes in Computer Science, pages 183–198, Montréal, Canada, August 2008. Springer-Verlag. [ bib | .pdf ]
[18] Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Certification of automated termination proofs. In Boris Konev and Frank Wolter, editors, 6th International Symposium on Frontiers of Combining Systems (FroCos 07), volume 4720 of Lecture Notes in Artificial Intelligence, pages 148–162, Liverpool,UK, September 2007. Springer-Verlag. [ bib | .pdf ]
[19] M. Blanc, P. Clemente, P. Courtieu, S. Franche, L. Oudot, C. Toinard, and L. Vessiller. Amélioration de la sécurité des grands réseaux par une infrastructure de méta-politique. In CFIP 05, 2005. [ bib ]
[20] Mathieu Blanc, Patrice Clemente, Pierre Courtieu, Stephane Franche, Laurent Oudot, Christian Toinard, and Lionel Vessiller. Hardening large-scale networks security through a meta-policy framework. In Third Workshop on the Internet, Telecommunications and Signal Processing (WITSP.04), Adelaide, Australia, dec 2004. [ bib | .pdf ]
[21] Mathieu Blanc, Pierre Courtieu, Gaetan Hains, Laurent Oudot, and Christian Toinard. A novel approach for distributed updates of MAC policies using a meta-protection framework. In Supplementary Proceedings of the 15th IEEE International Symposium on Software Reliability Engineering (ISSRE 2004), Saint Malo, France, nov 2004. [ bib | .pdf ]
[22] G. Barthe, P. Courtieu, G. Dufay, and S. Melo de Sousa. Jakarta: tool-assisted specification and verification of the JavaCard Platform. Journal of Automated Reasoning, Volume 35, Numbers 1-3:295–354, October 2005. [ bib | .pdf ]
[23] G. Barthe and P. Courtieu. Efficient Reasoning about Executable Specifications in Coq. In C. Muñoz V. A Carreno and S. Tahar, editors, Proceedings of TPHOLs'02, volume 2410 of Lecture Notes in Computer Science, pages 31–46. springer, 2002. [ bib | .pdf ]
[24] G. Barthe, G. Dufay, Simao de Sousa, and P. Courtieu. Tool-Assisted Specification and Verification of the JavaCard Platform. In Proceedings of AMAST'02, volume 2422 of Lecture Notes in Computer Science, pages 41–59. Springer-Verlag, 2002. [ bib | .ps.gz ]
[25] Pierre Courtieu. Normalized types. In Proceedings of CSL2001, volume 2142 of Lecture Notes in Computer Science, 2001. [ bib | .ps.gz ]
[26] Pierre Courtieu. Proving self-stabilization with a proof assistant. In Proceedings of IPDPS'2002, IEEE CS Press, 2002. contained in IPDPS collected proceedings CD-ROM, Abstract appears in IPDPS'02 Proc. : Abstracts, p.0209. [ bib | .ps.gz ]
[27] Pierre Courtieu. Représentation de structures non libres en théorie des types. Thèse de doctorat, Université Paris-sud, Laboratoire de Recherche en informatique, décembre 2001. In french. [ bib | .ps.gz | .pdf ]