Courtieu

Pierre Courtieu

Maître de conférences
Team: Systèmes sûrs
Personal website: http://cedric.cnam.fr/~courtiep
Office: 33.1.15A

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 7th International Conference on NETworked sYStems (NETYS 2019), 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 Formal Methods for Industrial Critical Systems and Automated Verification of Critical Systems (FMICS/AVOCS), 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. A Certified Universal Gathering Algorithm for Oblivious Mobile Robots. In Distributed Computing (DISC), Paris, 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 ACM Conference on Principles of Distributed Computing (PODC), Chicago, United States, 2016. 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 International Symposium on Stabilization, Safety, and Security of Distributed Systems, 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 High Integrity Language Technology - ACM SIGAda?s Annual International Conference, 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 International Symposium on Distributed Computing (DISC2013), 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 Interactive theorem proving (TPHOLs), 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 Formal method 2012 (FME), 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 Interactive theorem proving (TPHOLs), 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 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, pages 63-72, ACM, Madrid, Spain, PEPM'10 , 2010. doi  www 
  1. Courtieu, P.; Gbedo, G. and Pons, O. Improved Matrix Interpretation. In SOFSEM'10, Int. Conf. on Current Trends in Theory and Practice of Computer Science,, 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 TPHOLs'08 Theorem Proving in Higher Order Logics, Montr?al, Canada, 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 6th Int. Symp. on Frontiers of Combining Systems, Liverpool, Royaume-Uni, 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.
Top