Recherche - Archive ouverte HAL Accéder directement au contenu

Filtrer vos résultats

40 résultats

[Invited Paper] Formal Methods for Mobile Robots: Current Results and Open Problems

Béatrice Bérard , Pierre Courtieu , Laure Millet , Maria Potop-Butucaru , Lionel Rieg , et al.
International Journal of Informatics Society, 2015, 7 (3), pp.101-114
Article dans une revue hal-01238784v1

The KRAKATOA tool for certificationof JAVA/JAVACARD programs annotated in JML

Claude Marché , Christine Paulin-Mohring , Xavier Urbain
Journal of Logic and Algebraic Programming, 2004, 58 (1-2), pp.89-106. ⟨10.1016/j.jlap.2003.07.006⟩
Article dans une revue hal-01984932v1

Certified Impossibility Results for Byzantine-Tolerant Mobile Robots

Cédric Auger , Zohir Bouzid , Pierre Courtieu , Sébastien Tixeuil , Xavier Urbain
International Symposium on Stabilization, Safety, and Security of Distributed Systems, Nov 2013, Osaka, Japan. pp.178-190, ⟨10.1007/978-3-319-03089-0_13⟩
Communication dans un congrès hal-00930267v1

Swarms of Mobile Robots: Towards Versatility with Safety

Pierre Courtieu , Lionel Rieg , Sébastien Tixeuil , Xavier Urbain
Leibniz Transactions on Embedded Systems, 2022, Special Issue on Distributed Hybrid Systems, 8 (2), pp.02:1-02:36. ⟨10.4230/LITES.8.2.2⟩
Article dans une revue hal-03901898v1

Automated Certified Proofs with CiME3

Evelyne Contejean , Pierre Courtieu , Julien Forest , Olivier Pons , Xavier Urbain
RTA - 22nd International Conference on Rewriting Techniques and Applications, 2011, Novi Sad, Serbia
Communication dans un congrès hal-00777669v1

Mechanically Proving Termination Using Polynomial Interpretations

Evelyne Contejean , Claude Marché , Ana Paula Tomás , Xavier Urbain
Journal of Automated Reasoning, 2005, 34 (4), pp.325-363. ⟨10.1007/s10817-005-9022-x⟩
Article dans une revue istex hal-01984434v1
Image document

A3PAT, an Approach for Certified Automated Termination Proofs

Evelyne Contejean , Pierre Courtieu , Julien Forest , Andrei Paskevich , Olivier Pons , et al.
2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, ACM, Jan 2010, Madrid, Spain. pp.63-72, ⟨10.1145/1706356.1706370⟩
Communication dans un congrès inria-00535655v1
Image document

Manuel de savoir-prouver à l’usage des roboteux et des distributeux

Thibaut Balabonski , Pierre Courtieu , Robin Pelle , Lionel Rieg , Sébastien Tixeuil , et al.
ALGOTEL 2019 - 21èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications, Jun 2019, Saint Laurent de la Cabrerisse, France. pp.1-4
Communication dans un congrès hal-02115611v1

Brief Announcement Continuous vs. Discrete Asynchronous Moves: A Certified Approach for Mobile Robots

Thibaut Balabonski , Pierre Courtieu , Robin Pelle , Lionel Rieg , Sébastien Tixeuil , et al.
Stabilization, Safety, and Security of Distributed Systems. SSS 2018., Xavier Defago, Toshimitsu Masuzawa, Koichi Wada, Nov 2018, Tokyo, Japan. pp.404-408, ⟨10.1007/978-3-030-03232-6_29⟩
Communication dans un congrès hal-01937420v1

Brief Announcement: Certified impossibility results for Byzantine-tolerant mobile robots

Cédric Auger , Zohir Bouzid , Pierre Courtieu , Sébastien Tixeuil , Xavier Urbain
International Symposium on Distributed Computing (DISC2013), Oct 2013, Jerusalem, Israel. pp.2
Communication dans un congrès hal-01126335v1

Mechanically proving termination using polynomial interpretations

Evelyne Contejean , Claude Marché , Ana-Paula Tomas , Xavier Urbain
[Intern report] 1382, 2006
Rapport inria-00001167v1
Image document

Du discrètement continu au continûment discret

Thibaut Balabonski , Pierre Courtieu , Robin Pelle , Lionel Rieg , Sébastien Tixeuil , et al.
ALGOTEL 2020 – 22èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications, Sep 2020, Lyon, France
Communication dans un congrès hal-02871295v1

Computer Aided Formal Design of Swarm Robotics Algorithms

Thibaut Balabonski , Pierre Courtieu , Robin Pelle , Lionel Rieg , Sébastien Tixeuil , et al.
Stabilization, Safety, and Security of Distributed Systems. SSS 2021, Nov 2021, Online, Sweden. pp.469-473, ⟨10.1007/978-3-030-91081-5_31⟩
Communication dans un congrès hal-03425768v1
Image document

Absolute cross sections and asymmetry parameters for photodetachment of excited C$^-$($^2$D)

Raphaël Marion , Mariko Dunseath-Terao , Kevin Dunseath , Xavier Urbain
14th European Conference on Atoms Molecules and Photons (ECAMP 14), Jun 2022, Vilnius, Lithuania.
Poster de conférence hal-03709572v1

Certification of automated termination proofs

Evelyne Contejean , Pierre Courtieu , Julien Forest , Olivier Pons , Xavier Urbain
6th Int. Symp. on Frontiers of Combining Systems, Liverpool, Royaume-Uni, Jan 2007, X, France. pp.148-162
Communication dans un congrès hal-01125312v1

Towards a notion of Usable Rule for Context-Sensitive Rewrite Systems

Ra?l Guti?rrez , Salvador Lucas , Xavier Urbain
PROLE'07, E. Pimentel ed., Proceedings of 7th Spanish Conference on Programming and Computer Languages, Saragosse, Espagne, Jan 2007, X, France. pp.243--252
Communication dans un congrès hal-01125366v1

Certifying a Termination Criterion Based on Graphs, without Graphs

Pierre Courtieu , Julien Forest , Xavier Urbain
TPHOLs'08 Theorem Proving in Higher Order Logics, Montr?al, Canada, Jan 2008, Montreal, Canada. pp.183-198
Communication dans un congrès hal-01125530v1
Image document

Approche incrémentale des preuves automatiques de terminaison

Xavier Urbain
Logique en informatique [cs.LO]. Université Paris 11, 2001. Français. ⟨NNT : 2001PA112227⟩
Thèse tel-02061902v1

Certified Gathering of Oblivious Mobile Robots: survey of recent results and open problems

Thibaut Balabonski , Pierre Courtieu , Lionel Rieg , Sébastien Tixeuil , Xavier Urbain
Formal Methods for Industrial Critical Systems and Automated Verification of Critical Systems (FMICS/AVOCS), Sep 2017, Turin, Italy. pp.165-181, ⟨10.1007/978-3-319-67113-0_11⟩
Communication dans un congrès hal-01549942v1

Formal Proofs of Robustness for Watermarking Algorithms

Pierre Courtieu , David Baelde , Christine Paulin-Mohring , Xavier Urbain , David Gross-Amblard
TYPES WOKSHOP 2011, Sep 2011, X, France
Communication dans un congrès hal-01126043v1
Image document

Certified Universal Gathering in $R^2$ for Oblivious Mobile Robots

Pierre Courtieu , Lionel Rieg , Sébastien Tixeuil , Xavier Urbain
[Research Report] UPMC; CNAM. 2016
Rapport hal-01274295v1

Impossibility of gathering, a certification

Pierre Courtieu , Lionel Rieg , Sébastien Tixeuil , Xavier Urbain
Information Processing Letters, 2015, 115 (3), pp.447-452. ⟨10.1016/j.ipl.2014.11.001⟩
Article dans une revue hal-01122869v1
Image document

Certified Impossibility Results for Byzantine-Tolerant Mobile Robots

Cédric Auger , Zohir Bouzid , Pierre Courtieu , Sébastien Tixeuil , Xavier Urbain
[Research Report] 1560, LRI - CNRS, University Paris-Sud. 2013
Rapport hal-00834633v1

Continuous vs. Discrete Asynchronous Moves: A Certified Approach for Mobile Robots

Thibaut Balabonski , Pierre Courtieu , Robin Pelle , Lionel Rieg , Sébastien Tixeuil , et al.
7th International Conference on NETworked sYStems (NETYS 2019), Jun 2019, Marrakech, Morocco. pp.93-09, ⟨10.1007/978-3-030-31277-0_7⟩
Communication dans un congrès hal-02115599v1

Synchronous Gathering Without Multiplicity Detection: A Certified Algorithm

Thibaut Balabonski , Amélie Delga , Lionel Rieg , Sébastien Tixeuil , Xavier Urbain
International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2016), Nov 2016, Lyon, France. pp.7-19, ⟨10.1007/978-3-319-49259-9_2⟩
Communication dans un congrès hal-01491813v1

Certification of automated termination proofs

Evelyne Contejean , Pierre Courtieu , Julien Forest , Olivier Pons , Xavier Urbain
[Research Report] CEDRIC-07-1185, CEDRIC Lab/CNAM. 2007
Rapport hal-01125298v1
Image document

Comment s'assurer de garder le contact (et nos distances)

Thibaut Balabonski , Pierre Courtieu , Robin Pelle , Lionel Rieg , Sébastien Tixeuil , et al.
ALGOTEL 2021 - 23èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications, 2021, La Rochelle, France
Communication dans un congrès hal-03219933v1
Image document

Computer Aided Formal Design of Swarm Robotics Algorithms

Thibaut Balabonski , Pierre Courtieu , Robin Pelle , Lionel Rieg , Sébastien Tixeuil , et al.
2021
Pré-publication, Document de travail hal-03111541v1

Synchronous Gathering without Multiplicity Detection: a Certified Algorithm

Thibaut Balabonski , Amélie Delga , Lionel Rieg , Sébastien Tixeuil , Xavier Urbain
Theory of Computing Systems, 2019, 63 (2), pp.200-218. ⟨10.1007/s00224-017-9828-z⟩
Article dans une revue hal-01894618v1

A Certified Universal Gathering Algorithm for Oblivious Mobile Robots

Pierre Courtieu , Lionel Rieg , Sébastien Tixeuil , Xavier Urbain
Distributed Computing (DISC), Sep 2016, Paris, France
Communication dans un congrès hal-01349061v1