Recherche - Archive ouverte HAL Accéder directement au contenu

Filtrer vos résultats

25 résultats
Image document

Vérification de la génération modulaire du code impératif pour Lustre

Timothy Bourke , Pierre-Evariste Dagand , Marc Pouzet , Lionel Rieg
JFLA 2017 - Vingt-huitième Journées Francophones des Langages Applicatifs, Jan 2017, Gourette, France
Communication dans un congrès hal-01403830v1
Image document

Extracting Herbrand trees in classical realizability using forcing

Lionel Rieg
Computer Science Logic 2013, Simona Ronchi Della Rocca, Sep 2013, Turin, Italy. pp.15, ⟨10.4230/LIPIcs.CSL.2013.i⟩
Communication dans un congrès ensl-00814278v2

[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
Image document

A Formally Verified Compiler for Lustre

Timothy Bourke , Lélio Brun , Pierre-Evariste Dagand , Xavier Leroy , Marc Pouzet , et al.
PLDI 2017 - 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, ACM, Jun 2017, Barcelone, Spain
Communication dans un congrès hal-01512286v1

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

A Foundational Framework for Certified Impossibility Results with Mobile Robots on Graphs

Thibaut Balabonski , Robin Pelle , Lionel Rieg , Sébastien Tixeuil
ICDCN 2018 - 19th International Conference on Distributed Computing and Networking, Jan 2018, Varanasi, India. pp.1-10, ⟨10.1145/3154273.3154321⟩
Communication dans un congrès hal-01753439v1

Integrating Formal Schedulability Analysis into a Verified OS Kernel

Xiaojie Guo , Maxime Lesourd , Mengqi Liu , Lionel Rieg , Zhong Shao
Computer Aided Verification, Jul 2019, New York, United States. pp.496-514, ⟨10.1007/978-3-030-25543-5_28⟩
Communication dans un congrès hal-02289494v1
Image document

Impossibility of Gathering, a Certification

Pierre Courtieu , Lionel Rieg , Xavier Urbain , Sébastien Tixeuil
[Technical Report] CEDRIC-14-3016, CEDRIC laboratory, CNAM-Paris, France. 2014, pp.10
Rapport hal-00995126v1
Image document

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

Thibaut Balabonski , Pierre Courtieu , Robin Pelle , Lionel Rieg , Sébastien Tixeuil , et al.
[Research Report] Sorbonne Université, CNRS, Laboratoire d’Informatique de Paris 6, LIP6, F-75005 Paris, France. 2018, pp.1-12
Rapport hal-01762962v1
Image document

A Certified Universal Gathering Algorithm for Oblivious Mobile Robots

Pierre Courtieu , Lionel Rieg , Sébastien Tixeuil , Xavier Urbain
[Research Report] UPMC, Sorbonne Universites CNRS; CNAM, Paris; College de France; Université Paris Sud. 2015
Rapport hal-01159890v1

Brief announcement: Certified Universal Gathering in R2 for Oblivious Mobile Robots

Pierre Courtieu , Lionel Rieg , Sébastien Tixeuil , Xavier Urbain
ACM Conference on Principles of Distributed Computing (PODC), ACM, Jul 2016, Chicago, United States
Communication dans un congrès hal-01349084v1

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
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
Image document

Extracting Herbrand trees from Coq

Lionel Rieg
2011
Rapport ensl-00814115v1
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

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
Image document

Good friends are hard to find!

Thomas Brihaye , Mohamed Ghannem , Nicolas Markey , Lionel Rieg
Proceedings of the 15th International Symposium on Temporal Representation and Reasoning (TIME'08), 2008, Montréal, Canada. pp.32-40, ⟨10.1109/TIME.2008.10⟩
Communication dans un congrès hal-01194596v1
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

Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation

Mengqi Liu , Lionel Rieg , Zhong Shao , Ronghui Gu , David Costanzo , et al.
Proceedings of the ACM on Programming Languages, 2020, 4 (POPL), pp.1-31. ⟨10.1145/3371088⟩
Article dans une revue hal-02875542v1
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
Image document

On Forcing and Classical Realizability

Lionel Rieg
Other [cs.OH]. Ecole normale supérieure de lyon - ENS LYON, 2014. English. ⟨NNT : 2014ENSL0915⟩
Thèse tel-01061442v1