|
 
|
Xavier Urbain
|
Equipe SYS Parti depuis le 01/09/2016 Mail : [nom]  [ensiie].[fr]
Tel : 0169367338 Fax : (33)15880 http://www.ensiie.fr/~urbain |
Xavier's Tag-Cloud :
algorithme probabiliste,
analysis of algorithms
automatic theorem proving
computational geometry
distributed computing
theory of computation,
automated deduction,
automated proof,
certification,
certified proof,
confluence,
deep embedding,
distributed algorithm,
distributed computing,
formal proof,
gathering,
impossibility result,
mobile autonomous robot,
mobile robot,
preuve de programme,
proof assistant,
proof certification
,
rewriting,
robot swarm,
swarm,
swarm of robot,
term algebra,
termination,
theorem proving
|
Publications
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
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)
Conférence Internationale avec comité de lecture
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)
Revue Internationale avec comité de lecture
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,
- [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
2011
- [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,
-
[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
- [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,
-
[Urb10]
X. Urbain.
"Preuve automatique : techniques, outils et certification",
Soutenue le: 29 November 2010,
pp. 77,
Conférence Internationale avec comité de lecture
Mémoire de HDR
2008
- [DLM08] F. Duran, S. Lucas, J. Meseguer, C. Marché, X. Urbain. "Proving Operational Termination of Membership Equational Programs", Higher Order and Symbolic Computation, vol. 21(1), pp. 59-88, 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,
- [GLU08] R. Gutiérrez, S. Lucas, X. Urbain. "Usable Rules for Context-Sensitive Rewriting", 19th Int. Conf. on Rewriting Techniques and Applications, Linz, Autriche, January 2008, Vol. 5117, pp.126-141, Series LNCS,
-
[CFU08a]
E. Contejean, J. Forest, X. Urbain.
"Deep-Embedded Unification",
Date de dépot: 2008/01/01,
(Tech. Rep.: CEDRIC-08-1547)
Revue Internationale avec comité de lecture
Conférence Internationale avec comité de lecture
Rapport Scientifique
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,
- [GLU07] R. Gutiérrez, S. Lucas, X. Urbain. "Towards a notion of Usable Rule for Context-Sensitive Rewrite Systems", PROLE'07, E. Pimentel ed., Proceedings of 7th Spanish Conference on Programming and Computer Languages, Saragosse, Espagne, January 2007, pp.243--252,
-
[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
Conférence Nationale avec comité de lecture
Rapport Scientifique
2005
- [CMP05] E. Contejean, C. Marché, A. Paula Tomas, X. Urbain. "Mechanically proving termination using polynomial interpretations", JAR, Journal of Automated Reasoning, vol. 34(4), pp. 325-363, 2005
