X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/a3f9d0ed51ec4d4f74dc6f9b34a19d745b8ff6d6..d3547e5fc5186be997e4f09bb4a21d50fb0dcf7f:/research/publications.html
diff --git a/research/publications.html b/research/publications.html
index 7d85125..902fb52 100644
--- a/research/publications.html
+++ b/research/publications.html
@@ -5,8 +5,31 @@ slug: Publications
Conference and journal papers
+2023
+
+-
+ Grove: a Separation-Logic Library for Verifying Distributed Systems
+ Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
+ In SOSP 2023
+ [paper] [extended version]
+
+
+-
+ Verifying vMVCC, a high-performance transaction library using multi-version concurrency control
+ Yun-Sheng Chang, Ralf Jung, Upamanyu Sharma, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
+ In OSDI 2023
+ [paper] [paper website (incl. Coq formalization)]
+
+
2022
+-
+ Later Credits: Resourceful Reasoning for the Later Modality
+ Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
+ In ICFP 2022
+ [paper] [paper website (incl. Coq formalization)]
+
+
-
Simuliris: A separation logic framework for verifying concurrent program optimizations
Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer