Courtieu

Pierre Courtieu

Maître de conférences
Équipe : Systèmes sûrs
Site web : http://cedric.cnam.fr/~courtiep
Bureau : 33.1.15A

2025

Articles de conférence

  1. Bonnet, F. c.; Bramas, Q.; Courtieu, P.; Défago, X.; Rieg, L.; Tixeuil, S. and Urbain, X. Comment se rassembler (avec certitude) quand on est confus et désorienté. In ALGOTEL 2025 -- 27èmes Rencontres Francophones sur les AspectsAlgorithmiques des Télécommunications, Saint Valery-sur-Somme, France, 2025. www 
  1. Bonnet, F. c.; Bramas, Q.; Courtieu, P.; Défago, X.; Rieg, L.; Tixeuil, S. and Urbain, X. Deterministic Color-optimal Self-stabilizing Semi-synchronous Gathering: a Certified Algorithm. In LNCS, Springer Nature, Delphi, Greece, LNCS , 2025. www 
  1. Aponte, M-V.; Bouverot-Dupuis, M.; Bramas, Q.; Courtieu, P.; Rieg, L. and Urbain, X. Rendez-vous au Point-Dont-On-Ne-Doit-Pas-Calculer-Les-Coordonnées. In ALGOTEL 2025 -- 27èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications, Saint Valery-sur-Somme, France, 2025. www 

Logiciel

  1. Courtieu, P.; Rieg, L. and Urbain, X. Pactole. www 

2022

Articles de revue

  1. Courtieu, P.; Rieg, L.; Tixeuil, S. and Urbain, X. Swarms of Mobile Robots: Towards Versatility with Safety. In Leibniz Transactions on Embedded Systems, 8 (2): 02:1-02:36, 2022. doi  www 

2021

Articles de conférence

  1. Balabonski, T.; Courtieu, P.; Pelle, R.; Rieg, L.; Tixeuil, S. and Urbain, X. Comment s'assurer de garder le contact (et nos distances). In ALGOTEL 2021 - 23èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications, La Rochelle, France, 2021. www 

Non publié

  1. Balabonski, T.; Courtieu, P.; Pelle, R.; Rieg, L.; Tixeuil, S. and Urbain, X. Computer Aided Formal Design of Swarm Robotics Algorithms. , working paper or preprint. www 

2020

Articles de conférence

  1. Balabonski, T.; Courtieu, P.; Pelle, R.; Rieg, L.; Tixeuil, S. and Urbain, X. Du discrètement continu au contin^ument discret. In ALGOTEL 2020 -- 22èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications, Lyon, France, 2020. www 

2019

Articles de conférence

  1. Courtieu, P. Les Protocoles de Déplacement de Robots: l'Algorithmique distribuée comme terrain de jeu pour la preuve formelle. In JFLA 2019. Journées Francophones des Langages Applicatifs, Les Rousses, France, 2019. www 
  1. Balabonski, T.; Courtieu, P.; Pelle, R.; Rieg, L.; Tixeuil, S. and Urbain, X. Manuel de savoir-prouver `a l'usage des roboteux et des distributeux. In ALGOTEL 2019 - 21èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications, pages 1-4, Saint Laurent de la Cabrerisse, France, 2019. www 
  1. Balabonski, T.; Courtieu, P.; Pelle, R.; Rieg, L.; Tixeuil, S. and Urbain, X. Continuous vs. Discrete Asynchronous Moves: A Certified Approach for Mobile Robots. In Lecture Notes in Computer Science, pages 93-09, Marrakech, Morocco, Lecture Notes in Computer Science 11704, 2019. doi  www 

2018

Articles de conférence

  1. Balabonski, T.; Courtieu, P.; Pelle, R.; Rieg, L.; Tixeuil, S. and Urbain, X. Brief Announcement Continuous vs. Discrete Asynchronous Moves: A Certified Approach for Mobile Robots. In Stabilization, Safety, and Security of Distributed Systems. SSS 2018., pages 404-408, Springer-Verlag, Tokyo, Japan, Lecture Notes in Computer Science 11201, 2018. doi  www 

Rapports

  1. Balabonski, T.; Courtieu, P.; Pelle, R.; Rieg, L.; Tixeuil, S. and Urbain, X. Continuous vs. Discrete Asynchronous Moves: a Certified Approach for Mobile Robots. Technical Report, Sorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6, LIP6, F-75005 Paris, France, 2018.

2017

Articles de conférence

  1. Balabonski, T.; Courtieu, P.; Rieg, L.; Tixeuil, S. and Urbain, X. Certified Gathering of Oblivious Mobile Robots: survey of recent results and open problems. In Proceedings of AVOCS 2017, pages 165-181, Springer, Turin, Italy, Lecture Notes in Computer Science 10471, 2017. doi  www 

2016

Articles de conférence

  1. Bosser, A-G.; Aponte, M-V.; Courtieu, P. and Forest, J. Une preuve est une histoire. In Vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016), Saint-Malo, France, 2016. www 
  1. Courtieu, P.; Rieg, L.; Tixeuil, S. and Urbain, X. Brief announcement: Certified Universal Gathering in R2 for Oblivious Mobile Robots. In PODC '16: Proceedings of the 2016 ACM Symposium on Principles of Distributed Computing, pages 439-441, ACM, Chicago, United States, 2016. doi  www 
  1. Courtieu, P.; Rieg, L.; Tixeuil, S. and Urbain, X. Certified Universal Gathering in $R^2$ for Oblivious Mobile Robots. In Lecture Notes in Computer Science, pages 187-200, Springer Berlin Heidelberg, Paris, France, Lecture Notes in Computer Science 9888, 2016. doi  www 

Rapports

  1. Courtieu, P.; Rieg, L.; Tixeuil, S. and Urbain, X. Certified Universal Gathering in $R^2$ for Oblivious Mobile Robots. Technical Report, UPMC ; CNAM, 2016.

2015

Articles de revue

  1. Bérard, B.; Courtieu, P.; Millet, L.; Potop-Butucaru, M.; Rieg, L.; Sznajder, N.; Tixeuil, S. and Urbain, X. [Invited Paper] Formal Methods for Mobile Robots: Current Results and Open Problems. In International Journal of Informatics Society, 7 (3): 101-114, 2015. www 
  1. Courtieu, P.; Rieg, L.; Tixeuil, S. and Urbain, X. Impossibility of gathering, a certification. In Information Processing Letters, 115 (3): 447-452, 2015. doi  www 

Rapports

  1. Courtieu, P.; Rieg, L.; Tixeuil, S. and Urbain, X. A Certified Universal Gathering Algorithm for Oblivious Mobile Robots. Technical Report, UPMC, Sorbonne Universites CNRS ; CNAM, Paris ; College de France ; Université Paris Sud, 2015.

2014

Rapports

  1. Courtieu, P.; Rieg, L.; Urbain, X. and Tixeuil, S. Impossibility of Gathering, a Certification. Technical Report CEDRIC-14-3016, CEDRIC laboratory, CNAM-Paris, France, 2014.

2013

Articles de conférence

  1. Auger, C.; Bouzid, Z.; Courtieu, P.; Tixeuil, S. and Urbain, X. Certified Impossibility Results for Byzantine-Tolerant Mobile Robots. In Lecture Notes in Computer Science, pages 178-190, Springer, Osaka, Japan, Lecture Notes in Computer Science 8255, 2013. doi  www 
  1. Courtieu, P.; Aponte, M-V.; Crolard, T.; Zhang, Z.; Belt, J.; Hatcliff, J.; Guitton, J. and Jennings, T. Extended abstract: Towards the Formalization of SPARK 2014 Semantics with Explicit Run-time Checks Using Coq. In ACM Digital Library, pages 2, X, Australia, ACM Digital Library , 2013. www 
  1. Auger, C.; Bouzid, Z.; Courtieu, P.; Tixeuil, S. and Urbain, X. Brief Announcement: Certified impossibility results for Byzantine-tolerant mobile robots. In LNCS, pages 2, Jerusalem, Israel, LNCS 8205, 2013. www 

Rapports

  1. Auger, C.; Bouzid, Z.; Courtieu, P.; Tixeuil, S. and Urbain, X. Certified Impossibility Results for Byzantine-Tolerant Mobile Robots. Technical Report 1560, LRI - CNRS, University Paris-Sud, 2013.

2012

Articles de conférence

  1. Courtieu, P.; Paulin-Mohring, C.; Gross-Amblard, D. and Baelde, D. Toward provably robust watermarking. In LNCS, pages 0-0, X, France, LNCS , 2012. www 
  1. Courtieu, P.; Aponte, M-V.; Moy, Y. and Sango, M. Maximal and Compositional Pattern-Based Loop Invariants. In LNCS, pages 37-51, Paris, France, LNCS 7436, 2012. www 

Rapports

  1. Courtieu, P.; Aponte, M-V.; Sango, M. and Moy, Y. Maximal and Compositional Pattern-BasedLoop Invariants - Definitions and Proofs. Technical Report CEDRIC-12-2555, CEDRIC Lab/CNAM, 2012.

Non publié

  1. Baelde, D.; Courtieu, P.; Gross-Amblard, D. and Paulin-Mohring, C. Towards Provably Robust Watermarking. , working paper or preprint. www 

2011

Articles de conférence

  1. Contejean, E.; Courtieu, P.; Forest, J.; Pons, O. and Urbain, X. Automated Certified Proofs with CiME3. In RTA - 22nd International Conference on Rewriting Techniques and Applications, Novi Sad, Serbia, 2011. www 
  1. Bosser, A-G.; Courtieu, P.; Forest, J. and Cavazza, M. Structural Analysis of Narratives with the Coq Proof Assistant. In Lecture Notes in Computer Science, pages 55-70, Berg en Dal, Netherlands, Lecture Notes in Computer Science 6898, 2011. www 
  1. Courtieu, P.; Baelde, D.; Paulin-Mohring, C.; Urbain, X. and Gross-Amblard, D. Formal Proofs of Robustness for Watermarking Algorithms. In TYPES WOKSHOP 2011, X, France, 2011. www 

Rapports

  1. Bosser, A-G.; Cavazza, M.; Courtieu, P. and Forest, J. Structural Analysis of Narratives with the Coq Proof Assistant. Technical Report CEDRIC-11-2061, CEDRIC Lab/CNAM, 2011.

2010

Articles de conférence

  1. Contejean, E.; Courtieu, P.; Forest, J.; Paskevich, A.; Pons, O. and Urbain, X. A3PAT, an Approach for Certified Automated Termination Proofs. In PEPM'10, pages 63-72, ACM, Madrid, Spain, PEPM'10 , 2010. doi  www 
  1. Courtieu, P.; Gbedo, G. and Pons, O. Improved Matrix Interpretation. In LNCS, pages 12, Spindleruv Ml'yn, Czech Republic, LNCS 5901, 2010. www 

2009

Articles de conférence

  1. Courtieu, P.; Gbedo, G. and Pons, O. Matrix interpretations revisited. In Extended Abstracts of the 10th International Workshop on Termination, WST'09, Leipzig, Germany, Ju, pages 4, X, France, 2009. www 

2008

Articles de conférence

  1. Courtieu, P.; Forest, J. and Urbain, X. Certifying a Termination Criterion Based on Graphs, without Graphs. In Lecture Notes in Computer Science, pages 183-198, Montreal, Canada, Lecture Notes in Computer Science 5170, 2008. www 

2007

Articles de conférence

  1. Contejean, E.; Courtieu, P.; Forest, J.; Pons, O. and Urbain, X. Certification of automated termination proofs. In LNAI 4720, pages 148-162, X, France, LNAI 4720 , 2007. www 

Rapports

  1. Contejean, E.; Courtieu, P.; Forest, J.; Pons, O. and Urbain, X. Certification of automated termination proofs. Technical Report CEDRIC-07-1185, CEDRIC Lab/CNAM, 2007.

2005

Articles de conférence

  1. Blanc, M.; Courtieu, P. and Hains, G. Mandatory Access Control On Distributed Systems: A Metapolicy Framework. In First Colloquium on Risk and Security of the Internet and Systems (CRiSIS 2005), pages 133-144, Ecole Nationale Supérieure d'Ingénieurs de Bourges, Bourges, France, ISBN : 2-9525367-0-8 , 2005. www 
  1. Abou El Kalam, A.; Briffaut, J.; Clemente, P.; Courtieu, P.; Gadaud, F.; Hains, G.; Lalande, J-F. c. and Toinard, C. Systèmes de confiance et détection d'intrusion répartis. In Les Journées Informatique de la Région Centre, pages -, Blois, France, 2005. www 
  1. Blanc, M.; Clemente, P.; Courtieu, P.; Franche, S.; Oudot, L.; Toinard, C. and Vessiller, L. Amélioration de la sécurité des grands réseaux par une infrastructure de méta-politique. In 11ème Colloque Francophone sur l'Ingénierie des Protocoles (CFIP'2005), pages 517-530, Lavoisier, Bordeaux, France, ISBN: 2-7462-1151-3 , 2005. www 

2004

Articles de conférence

  1. Blanc, M.; Courtieu, P.; Hains, G.; Oudot, L. and Toinard, C. A novel approach for distributed updates of MAC policies using a meta-protection framework. In 15th IEEE International Symposium on Software Reliability Engineering (ISSRE 2004), pages 29-30, INRIA, Rennes, France, Saint Malo, France, ISBN: 2-7261-1278-1 , 2004. www 
  1. Blanc, M.; Clemente, P.; Courtieu, P.; Franche, S.; Oudot, L.; Toinard, C. and Vessiller, L. Hardening large-scale networks security through a meta-policy framework. In 3rd Workshop on the Internet, Telecommunications and Signal Processing (WITSP'04), pages 132-137, DSP for Communication Systems, Adela"ide, Australia, ISBN: 0-9756934-0-9 , 2004. www 

2001

Articles de conférence

  1. Courtieu, P. Normalized Types. In Computer Science Logic, Paris, France, 2001. www 

Thèses et habilitations

  1. Courtieu, P. Représentation d'algèbres non libres en théorie des types. Ph.D. Thesis, Université Paris 11, 2001.