body
News
- 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