• Sept. 2019 - The project funding has terminated. Thanks to all the contributors. A closing meeting (hosted at IRISA, Rennes; 20 participants) has been organized to summarize the most significant results of the project, and to draw some future research directions.

Past events

  • Oct. 2018 - Paper published in Journal of Automated Reasoning.
    "Verifying a Concurrent Garbage Collector using a Rely-Guarantee Methodology".
    Extended version of our ITP'17 paper.
  • July 2018 - Thomas Rubiano will be joining the project as a postdoc in September. Welcome Thomas!
  • July 2018 - Yon Fernandez de Retana PhD defense. [thesis]
    Title : "Vers la compilation vérifiée de Sea of Nodes : propriétés et raisonnement sémantiques".
    Jury :
    • David Monniaux, Verimag
    • Alain Darte, Laboratoire de l’Informatique du Parallélisme
    • Thibaut Balabonski, Université Paris-Sud, LRI
    • Thomas Jensen, Inria
    • David Pichardie, ENS Rennes, IRISA
    • Delphine Demange, Université Rennes 1, IRISA
  • May 2018 - Discover workshop in Saint-Malo
    Invited speakers : Assia Mahboubi (Inria), Jacques Noyer (Mines Nantes).
    A 2-days workshop with technical talks about programming languages, verification and security.
  • Jan. 2018 - Paper accepted at CC 2018.
    "Semantic Reasoning about the Sea of Nodes".
  • Nov. 2017 - Paper accepted at SAC SVT 2018.
    "Verified Compilation of Linearizable Data Structures".
  • June 2017 - Paper accepted at ITP'17.
    "Verifying a Concurrent Garbage Collector using a Rely-Guarantee Methodology".
  • June 2017 - Invited talk by Delphine Demange at Inria Scientific Days 2017.
    "On-the-Fly Garbage Collection: An Exercise in Compiler Verification".
  • June 2017 - Presentation by Yon Fernandez de Retana at 12th meeting of French community of Compilation.
    "Sea-of-Nodes: semantics and proof of program optimizations".
  • March 2017 - Andrea Parri (Scuola Superiore Sant'Anna, Pisa) visiting us at IRISA.
    "A Formal Model of the Linux-Kernel Memory Ordering". Joint work with Alglave, Maranget, McKenney, Stern.
  • Nov. 2016 - Dagstuhl seminar 16471 Concurrency with Weak Memory Models
  • July 2016 - Paper accepted at the ECOOP worshop FTfJP'16.
    "An Extended Buffered Memory Model With Full Reorderings".
  • Jun. 2016 - Session on Program Static Analysis and Verification at Journées nationales 2016 GT-Vérif
  • Jan. 2016 - Invited talk by Delphine Demange at Journées nationales 2016 GDR Informatique Mathématique
  • Jan. 2016 - Gustavo Petri visiting us at IRISA
  • April 2015 - Robin Morisset visiting us at IRISA

Last Updated 2019-09-27 Fri 19:01