|
 
|
Pierre Courtieu
cnam.frPublications
2018
- [CBT18] P. Courtieu, T. Balabonski, S. Tixeuil, X. Urbain, L. Rieg. "Brief Announcement: Continuous vs. Discrete Asynchronous Moves: A Certified Approach for Mobile Robots", Stabilization, Safety, and Security of Distributed Systems (SSS), November 2018, Vol. 11201, pp.404-408, Series LNCS, Tokyo, Japon, (DOI: 10.1007/978-3-030-03232-6_29)
Conférence Internationale avec comité de lecture
2017
- [CT17] P. Courtieu, S. Tixeuil. "Certified Gathering of Oblivious Mobile Robots: Survey of Recent Results and Open Problems", FMICS-AVoCS 2017, September 2017, Vol. 10471, pp.165-181, Series LNCS, Turin, Italy, (DOI: 10.1007/978-3-319-67113-0_11)
- [CZR17] P. Courtieu, Z. Zhang, Robby, J. Hatcliff, Y. Moy. "Focused Certification of an Industrial Compilation and Static Verification Toolchain", Software Engineering and Formal Methods (SEFM), August 2017, Vol. 10469, pp.17-34, Series LNCS, Trento, Italy, (DOI: 10.1007/978-3-319-66197-1_2)
-
[17]
P. Courtieu.
"Typage du langage R",
Date de dépot: 2017/09/30,
Nb pages 32,
(Tech. Rep.: CEDRIC-17-4158)
Conférence Internationale avec comité de lecture
Rapport Scientifique
2016
- [CUT16a] P. Courtieu, X. Urbain, S. Tixeuil, L. Rieg. "Certified Universal Gathering in {\textbackslash}mathbb {R} {\^{}}2 for Oblivious Mobile Robots", DISC 2016, Distributed Computing 30th International Symposium, September 2016, Vol. 9888, pp.187-200, Series LNCS, Paris, France, (DOI: 10.1007/978-3-662-53426-7_14)
- [CUT16] P. Courtieu, X. Urbain, S. Tixeuil, L. Rieg. "Brief Announcement: Certified Universal Gathering in R2 for Oblivious Mobile Robots", PODC '16: Proceedings of the 2016 ACM Symposium on Principles of Distributed Computing, July 2016, pp.439-441, Chicago, US, (DOI: 10.1145/2933057.2933070)
- [BCF16] A. Bosser, P. Courtieu, J. Forest, M. Aponte. "Une preuve est (un programme) une histoire", Actes des Vingt-septièmes Journées Francophones des Langages Applicatifs JFLA 2016, January 2016, pp.171-172, Saint Malo, France,
- [CP16] P. Courtieu, C. Pit-Claudel. "Company-Coq: Taking Proof General one step closer to a real IDE", CoqPL'16: International Workshop on Coq for Programming Languages, St Petersburgh, United-States, Florida,
Conférence Internationale avec comité de lecture
Conférence Nationale avec comité de lecture
Conférences Internationales sans actes
2015
- [CBM15] P. Courtieu, B. Bérard, L. Millet, M. Potop-Butucaru, L. Rieg, N. Sznajder, S. Tixeuil, X. Urbain. "[Invited Paper] Formal Methods for Mobile Robots: Current Results and Open Problems", International Journal of Informatics Society, vol. 7(3), pp. 101-114, 2015
- [CRT15a] P. Courtieu, L. Rieg, S. Tixeuil, X. Urbain. "Impossibility of Gathering, a Certification", Information Processing Letters, vol. 115, pp. 447-452, 2015, (doi:10.1016/j.ipl.2014.11.001)
- [CAC15] T. Crolard, M. Aponte, P. Courtieu, J. Lawall. "Formal Methods for Critical Systems: A verified implementation of nested procedures", International Conference on Applied Research in Computer Science and Engineering (ICAR'15), October 2015, pp.1, Lebanon, (DOI: 10.1109/ARCSE.2015.7338125)
Revue Internationale avec comité de lecture
Conférences invitées
2014
-
[CRT14]
P. Courtieu, L. Rieg, S. Tixeuil, X. Urbain.
"Impossibility of Gathering, a Certification",
Date de dépot: 2014/05/22,
Nb pages 10,
(Tech. Rep.: CEDRIC-14-3016)
Rapport Scientifique
2013
- [ABC13] C. Auger, Z. Bouzid, P. Courtieu, S. Tixeuil, X. Urbain. "Certified Impossibility Results for Byzantine-Tolerant Mobile Robots", International Symposium on Stabilization, Safety, and Security of Distributed Systems, November 2013, Vol. 8255, pp.15, Series LNCS, Osaka, Japon,
- [CAC13] P. Courtieu, M. Aponte, T. Crolard, Z. Zhang, Robby, J. Belt, J. Hatcliff, J. Guitton, T. Jennings. "Extended abstract: Towards the Formalization of SPARK 2014 Semantics with Explicit Run-time Checks Using Coq", High Integrity Language Technology - ACM SIGAda’s Annual International Conference, November 2013, pp.2, Series ACM Digital Library, US,
- [ABC13a] C. Auger, Z. Bouzid, P. Courtieu, S. Tixeuil, X. Urbain. "Brief Announcement: Certified impossibility results for Byzantine-tolerant mobile robots", International Symposium on Distributed Computing (DISC2013), October 2013, Vol. 8205, pp.2, Series LNCS, Jerusalem, Israel,
Conférence Internationale avec comité de lecture
2012
- [CAM12] P. Courtieu, M. Aponte, Y. Moy, M. Sango. "Maximal and Compositional Pattern-Based Loop Invariants", Formal method 2012 (FME), August 2012, Vol. 7436, pp.37-51, Series LNCS, Paris, France,
- [CPG12] P. Courtieu, C. Paulin-Mohring, D. Gross-Amblard, D. Baelde. "Toward provably robust watermarking", Interactive theorem proving (TPHOLs), August 2012, pp.0-0, Series LNCS,
-
[CAS12]
P. Courtieu, M. Aponte, M. Sango, Y. Moy.
"Maximal and Compositional Pattern-Based
Loop Invariants - Definitions and Proofs",
Date de dépot: 2012/05/24,
Nb pages 14,
(Tech. Rep.: CEDRIC-12-2555)
Conférence Internationale avec comité de lecture
Rapport Scientifique
2011
- [BCF11] A. Bosser, P. Courtieu, J. Forest, M. Cavazza. "Structural Analysis of Narratives with the Coq Proof Assistant.", Interactive theorem proving (TPHOLs), August 2011, Vol. 6898, pp.55--70, Series Lecture Notes in Computer Science, Berg en Dal, The Netherlands,
- [CCF11a] E. Contejean, P. Courtieu, J. Forest, O. Pons, X. Urbain. "Automated Certified Proofs with CiME 3", 22nd Int. Conf. on Rewriting Techniques and Applications, May 2011, Vol. 10, pp.21-30, Series LIPIcs, Novi Sad, Serbie,
- [CBP11] P. Courtieu, D. Baelde, C. Paulin-Mohring, X. Urbain, D. Gross-Amblard. "Formal Proofs of Robustness for Watermarking Algorithms", TYPES WOKSHOP 2011,
-
[BCC11]
A. Bosser, M. Cavazza, P. Courtieu, J. Forest.
"Structural Analysis of Narratives with the Coq Proof Assistant",
Date de dépot: 2011/03/01,
Nb pages 16,
(Tech. Rep.: CEDRIC-11-2061)
-
[CCF11]
E. Contejean, P. Courtieu, J. Forest, O. Pons, X. Urbain.
"Automated Certified Proofs with CiME3",
Date de dépot: 2011/02/01,
Nb pages 11,
(Tech. Rep.: CEDRIC-11-2044)
Conférence Internationale avec comité de lecture
Conférences Internationales sans actes
Rapport Scientifique
2010
- [CGP10] P. Courtieu, G. Gbedo, O. Pons. "Improved Matrix Interpretation", SOFSEM'10, Int. Conf. on Current Trends in Theory and Practice of Computer Science, , January 2010, Vol. 5901, pp.12, Series LNCS, Spindleruv Ml{\'y}n, Czech Republic,
- [CCF10] E. Contejean, P. Courtieu, J. Forest, A. Paskevich, O. Pons, X. Urbain. "A3PAT, an Approach for Certified Automated Termination Proofs", PEPM'10 Proceedings of the 2010 ACM SIGPLAN Symposium on Partial Evaluation and Program Manipulation, Madrid, Spain, January 2010, pp.10,
Conférence Internationale avec comité de lecture
2009
-
[CGP09a]
P. Courtieu, G. Gbedo, O. Pons.
"Matrix interpretations revisited",
Extended Abstracts of the 10th International Workshop on Termination, WST'09, Leipzig, Germany, Ju,
January 2009,
pp.4,
Conférence Internationale avec comité de lecture
2008
- [CFU08b] P. Courtieu, J. Forest, X. Urbain. "Certifying a Termination Criterion Based on Graphs, without Graphs", TPHOLs'08 Theorem Proving in Higher Order Logics, Montréal, Canada, January 2008, Vol. 5170, pp.183-198, Series Lecture Notes in Computer Science, Montreal, Canada,
Conférence Internationale avec comité de lecture
2007
- [CCF07a] E. Contejean, P. Courtieu, J. Forest, O. Pons, X. Urbain. "Certification of automated termination proofs", 6th Int. Symp. on Frontiers of Combining Systems, Liverpool, Royaume-Uni, January 2007, pp.148-162, Series LNAI 4720,
-
[CCF07]
E. Contejean, P. Courtieu, J. Forest, O. Pons, X. Urbain.
"Certification of automated termination proofs",
Date de dépot: 2007/01/01,
(Tech. Rep.: CEDRIC-07-1185)
Conférence Internationale avec comité de lecture
Rapport Scientifique
2005
-
[BCD05]
G. Barthe, P. Courtieu, G. Dufay, S. De Sousa.
"Tool-assisted specification and verification of Typed Low-Level Languages",
JAR, J. of Automated Reasoning,
vol. 35(4), pp. 295-354,
2005
