Home > Topics > Formal Proofs > Publications > Publications

Publications

2021

Conference Articles

  1. Exact Worst Case Self-Stabilization Time. Karine Altisen, Pierre Corbineau, Stéphane Devismes - the 22th International Conference on Distributed Computing and Networking (ICDCN 2021) - [bibtex]

2020

Journal Articles

  1. Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation. Mengqi Liu, Lionel Rieg, Zhong Shao, Ronghui Gu, David Costanzo, Jung-Eun Kim, Man-Ki Yoon - Proc. ACM Program. Lang. -- POPL 2020 Proceedings - [bibtex]
  2. Certified and Efficient Instruction Scheduling: Application to Interlocked VLIW Processors. Cyril Six, Sylvain Boulmé, David Monniaux - Proc. ACM Program. Lang. - [bibtex]

Conference Articles

  1. 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

Journal Articles

  1. Refinement to Certify Abstract Interpretations: Illustrated on Linearization for Polyhedra. Sylvain Boulmé, Alexandre Maréchal - Journal of Automated Reasoning - [bibtex]

Conference Articles

  1. 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]
  2. 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]
  3. 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

Conference Articles

  1. The Verified Polyhedron Library: an overview. Sylvain Boulmé, Alexandre Maréchal, David Monniaux, Michaël Périn, Hang Yu - 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC) - [bibtex]
  2. A Coq Tactic for Equality Learning in Linear Arithmetic. Sylvain Boulmé, Alexandre Maréchal - Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings - [bibtex]

2015

Conference Articles

  1. Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra. Sylvain Boulmé, Alexandre Maréchal - Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings - [bibtex]

2014

Conference Articles

  1. Modular and lightweight certification of polyhedral abstract domains. Alexis Fouilhé, Sylvain Boulmé, Michaël Périn - Types for Proofs and Programs (TYPES 2014) -- Book of Abstracts - [bibtex]
  2. A Certifying Frontend for (Sub)polyhedral Abstract Domains. Alexis Fouilhé, Sylvain Boulmé - Verified Software: Theories, Tools and Experiments (VSTTE 2014) - [bibtex]

Contact | Site Map | Site powered by SPIP 3.1.13 + AHUNTSIC [CC License]

info visites 1684342