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
- 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
- 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é
- Computer Aided Formal Design of Swarm Robotics Algorithms. , working paper or preprint. www
2020
Articles de conférence
- 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
- 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
- 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
- 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
- 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
2017
Articles de conférence
- 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
- Une preuve est une histoire. In Vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016), Saint-Malo, France, 2016. www
- Brief announcement: Certified Universal Gathering in R2 for Oblivious Mobile Robots. In ACM Conference on Principles of Distributed Computing (PODC), pages 439-441, ACM, Chicago, United States, 2016. doi www
- 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
- Certified Universal Gathering in $R^2$ for Oblivious Mobile Robots. Technical Report, UPMC ; CNAM, 2016.
2015
Articles de revue
- [Invited Paper] Formal Methods for Mobile Robots: Current Results and Open Problems. In International Journal of Informatics Society, 7 (3): 101-114, 2015. www
- Impossibility of gathering, a certification. In Information Processing Letters, 115 (3): 447-452, 2015. doi www
Rapports
2014
Rapports
- Impossibility of Gathering, a Certification. Technical Report CEDRIC-14-3016, CEDRIC laboratory, CNAM-Paris, France, 2014.
2013
Articles de conférence
- 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
- 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
- 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
- Certified Impossibility Results for Byzantine-Tolerant Mobile Robots. Technical Report 1560, LRI - CNRS, University Paris-Sud, 2013.
2012
Articles de conférence
- Toward provably robust watermarking. In Interactive theorem proving (TPHOLs), pages 0-0, X, France, LNCS , 2012. www
- Maximal and Compositional Pattern-Based Loop Invariants. In Formal method 2012 (FME), pages 37-51, Paris, France, LNCS 7436, 2012. www
Rapports
- Maximal and Compositional Pattern-BasedLoop Invariants - Definitions and Proofs. Technical Report CEDRIC-12-2555, CEDRIC Lab/CNAM, 2012.
Non publié
- Towards Provably Robust Watermarking. , working paper or preprint. www
2011
Articles de conférence
- Automated Certified Proofs with CiME3. In RTA - 22nd International Conference on Rewriting Techniques and Applications, Novi Sad, Serbia, 2011. www
- 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
- Formal Proofs of Robustness for Watermarking Algorithms. In TYPES WOKSHOP 2011, X, France, 2011. www
Rapports
- Structural Analysis of Narratives with the Coq Proof Assistant. Technical Report CEDRIC-11-2061, CEDRIC Lab/CNAM, 2011.
2010
Articles de conférence
- 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
- 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
- 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
- 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
- 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
- Certification of automated termination proofs. Technical Report CEDRIC-07-1185, CEDRIC Lab/CNAM, 2007.
2005
Articles de conférence
- 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
- 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
- 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
- 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
- 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
- Normalized Types. In Computer Science Logic, Paris, France, 2001. www
Thèses et habilitations
- Représentation d'algèbres non libres en théorie des types. Ph.D. Thesis, Université Paris 11, 2001.