Publications

2025

Articles de revue

1. Model checking of distributed algorithms using synchronous programs. Erwan Jahier, Karine Altisen, Stéphane Devismes, Gabriel Baiocchi Sant'anna - Theoretical Computer Science - [bibtex]

Articles de conférence

2. Revisited Convergence of a Self-stabilizing BFS Spanning Tree Algorithm. Karine Altisen, Marius Bozga - Formal Techniques for Distributed Objects, Components, and Systems - 45th IFIP WG 6.1 International Conference, FORTE 2025, Lille, France, June 16-20, 2025, Proceedings - [bibtex]

2024

Articles de revue

3. Self-stabilizing synchronous unison in directed networks. Karine Altisen, Alain Cournier, Geoffrey Defalque, Stéphane Devismes - Theoretical Computer Science - [bibtex]

Articles de conférence

4. Chamois: agile development of CompCert extensions for optimization and security. David Monniaux, Sylvain Boulmé - JFLA 2024 -- 35es Journées Francophones des Langages Applicatifs - [bibtex]
5. A Transistor Level Relational Semantics for Electrical Rule Checking by SMT Solving. Oussama Oulkaid, Bruno Ferres, Matthieu Moy, Pascal Raymond, Mehdi Khosravian, Ludovic Henrio, Gabriel Radanne - Design, Automation and Test in Europe Conference - [bibtex]
6. On Self-stabilizing Leader Election in Directed Networks. Karine Altisen, Alain Cournier, Geoffrey Defalque, Stéphane Devismes - Proceedings of the 43rd ACM Symposium on Principles of Distributed Computing (PODC 2024) - [bibtex]

2023

Articles de revue

7. Self-stabilizing Systems in Spite of High Dynamics. Karine Altisen, Stéphane Devismes, Anaïs Durand, Colette Johnen, Franck Petit - Theoretical Computer Science - [bibtex]
8. Formally Verifying Optimizations with Block Simulations. Léo Gourdin, Benjamin Bonneau, Sylvain Boulmé, David Monniaux, Alexandre Bérard - Proceedings of the ACM on Programming Languages, Issue OOPSLA2 - [bibtex]

Articles de conférence

9. Complexité certifiée d'algorithmes autostabilisants en rondes. Karine Altisen, Pierre Corbineau, Stéphane Devismes - ALGOTEL 2023 - 25èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications - [bibtex]
10. Model Checking of Distributed Algorithms using Synchronous Programs. Erwan Jahier, Karine Altisen, Stéphane Devismes, Gabriel B. Sant'Anna - 25th International Symposium on Stabilization, Safety, and Security of Distributed Systems - [bibtex]
11. Lazy Code Transformations in a Formally Verified Compiler. Léo Gourdin - ICOOOLPS '23: 18th ACM International Workshop on Implementation, Compilation, Optimization of OO Languages, Programs and Systems - [bibtex]
12. Pour battre à l'unisson, il faut que tous les chemins viennent de Rome. Karine Altisen, Alain Cournier, Geoffrey Defalque, Stéphane Devismes - ALGOTEL 2023 - 25èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications - Best Student Paper Award - [bibtex]
13. Self-stabilizing Synchronous Unison in Directed Networks. Karine Altisen, Alain Cournier, Geoffrey Defalque, Stéphane Devismes - Proceedings of the 24th International Conference on Distributed Computing and Networking (ICDCN 2023) - Best Student Paper Award - [bibtex]
14. Exploring Worst Cases of Self-stabilizing Algorithms using Simulations. Erwan Jahier, Karine Altisen, Stéphane Devismes - 25th International Symposium on Stabilization, Safety, and Security of Distributed Systems - [bibtex]
15. Electrical Rule Checking of Integrated Circuits using Satisfiability Modulo Theory. Bruno Ferres, Oussama Oulkaid, Ludovic Henrio, Mehdi Khosravian, Matthieu Moy, Gabriel Radanne, Pascal Raymond - DATE 2023 - Design, Automation and Test in Europe Conference - [bibtex]

2022

Articles de conférence

16. Formally Verified Superblock Scheduling. Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, Nicolas Nardino - Certified Programs and Proofs (CPP '22) - [bibtex]

2021

Articles de revue

17. Terminating Exploration of a Grid by an Optimal Number of Asynchronous Oblivious Robots. Stéphane Devismes, Anissa Lamani, Franck Petit, Pascal Raymond, Sébastien Tixeuil - The Computer Journal - [bibtex]

Articles de conférence

18. Exact Worst Case Self-Stabilization Time. Karine Altisen, Pierre Corbineau, Stéphane Devismes - ICDCN '21: International Conference on Distributed Computing and Networking, Virtual Event, Nara, Japan, January 5-8, 2021 - [bibtex]
19. Self-stabilizing Systems in Spite of High Dynamics. Karine Altisen, Stéphane Devismes, Anaïs Durand, Colette Johnen, Franck Petit - ICDCN '21: International Conference on Distributed Computing and Networking, Virtual Event, Nara, Japan, January 5-8, 2021 - [bibtex]
20. Optimal Exclusive Perpetual Grid Exploration by Luminous Myopic Opaque Robots with Common Chirality. Quentin Bramas, Stéphane Devismes, Pascal Lafourcade - ICDCN '21: International Conference on Distributed Computing and Networking, Virtual Event, Nara, Japan, January 5-8, 2021 - [bibtex]
21. Finding Water on Poleless using Melomaniac Myopic Chameleon Robots. Quentin Bramas, Stéphane Devismes, Pascal Lafourcade - 10th International Conference on Fun with Algorithms, FUN 2021, May 30 to June 1, 2021, Favignana Island, Sicily, Italy - [bibtex]
22. Un jour sans fin. Stéphane Devismes, Pascal Lafourcade - ALGOTEL 2021 - 23èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications - [bibtex]
23. Optimal Exclusive Perpetual Grid Exploration by Luminous Myopic Robots without Common Chirality. Arthur Rauch, Quentin Bramas, Stéphane Devismes, Pascal Lafourcade, Lamani Anissa - NETYS'2021, the 9th International Conference on NETworked sYStems - [bibtex]
24. Simple, light, yet formally verified, global common subexpression elimination and loop-invariant code motion. David Monniaux, Cyril Six - LCTES '21: 22nd ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems, Virtual Event, Canada, 22 June, 2021 - [bibtex]

Thèse de doctorat et HDR

25. Optimized and formally-verified compilation for a VLIW processor. Cyril Six - [bibtex]

2020

Articles de revue

26. Certified and Efficient Instruction Scheduling: Application to Interlocked VLIW Processors. Cyril Six, Sylvain Boulmé, David Monniaux - Proc. ACM Program. Lang. - [bibtex]

Articles de conférence

27. Scaling Up the Memory Interference Analysis for Hard Real-Time Many-Core Systems. Maximilien Dupont De Dinechin, Matheus Schuh, Matthieu Moy, Claire Maiza - DATE 2020 - Design, Automation and Test in Europe Conference - [bibtex]
28. SASA: A SimulAtor of Self-stabilizing Algorithms. Karine Altisen, Stéphane Devismes, Erwan Jahier - Tests and Proofs - 14th International Conference, TAP@STAF 2020, Bergen, Norway, June 22-23, 2020, Proceedings [postponed] - [bibtex]
29. Du discrètement continu au continûment discret. Thibaut Balabonski, Pierre Courtieu, Robin Pelle, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain - ALGOTEL 2020 - 22èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications - [bibtex]

2019

Articles de revue

30. Improving WCET Evaluation using Linear Relation Analysis. Pascal Raymond, Claire Maiza, Catherine Parent-Vigouroux, Erwan Jahier, Nicolas Halbwachs, Fabienne Carrier, Mihail Asavoae, Rémy Boutonnet - Leibniz Transactions on Embedded Systems - [bibtex]
31. Fast and Exact Analysis for LRU Caches. Valentin Touzeau, Claire Maiza, David Monniaux, Jan Reineke - Proc. ACM Program. Lang. - [bibtex]
32. A Survey of Timing Verification Techniques for Multi-Core Real-Time Systems. Claire Maiza, Hamza Rihani, Juan M. Rivas, Joël Goossens, Sebastian Altmeyer, Robert I. Davis - ACM Comput. Surv. - [bibtex]

Articles de conférence

33. Manuel de savoir-prouver à l'usage des roboteux et des distributeux. Thibaut Balabonski, Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain - ALGOTEL 2019, June 4-7, Proceedings - [bibtex]
34. Integrating Formal Schedulability Analysis into a Verified OS Kernel. Xiaojie Guo, Maxime Lesourd, Mengqi Liu, Lionel Rieg, Zhong Shao - Computer Aided Verification - 31st International Conference, CAV 2019, July 15-18, Proceedings - [bibtex]
35. Continuous vs. Discrete Asynchronous Moves: a Certified Approach for Mobile Robots on Graphs. Thibaut Balabonski, Pierre Courtieu, Robin Pelle, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain - NETYS 2019, June 19-21, Proceedings - [bibtex]

2018

Articles de conférence

36. Parallel Code Generation of Synchronous Programs for a Many-core Architecture. Amaury Graillat, Matthieu Moy, Pascal Raymond, Benoît Dupont De Dinechin - Design, Automation and Test in Europe - [bibtex]

2016

Articles de revue

37. Modeling Power Consumption and Temperature in TLM Models. Matthieu Moy, Claude Helmstetter, Tayeb Bouhadiba, Florence Maraninchi - Leibniz Transactions on Embedded Systems - [bibtex]

Articles de conférence

38. RDBG: a Reactive Programs Extensible Debugger. Erwan Jahier - 19th International Workshop on Software and Compilers for Embedded Systems (SCOPES'16), May 23th to 25th, 2016, Sankt Goar, Germany - [bibtex]

2014

Articles de conférence

39. A General Approach for Expressing Infeasibility in Implicit Path Enumeration Technique. Pascal Raymond - International Conference on Embedded Software (EMSOFT 2014) - [bibtex]

2009

Articles de revue

40. Full Simulation Coverage for SystemC Transaction-Level Models of Systems-on-a-Chip. Claude Helmstetter, Florence Maraninchi, Laurent Maillet-Contoz - Formal Methods in System Design - [bibtex]