Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)
Robbert Krebbers. Interactive and Automated Proofs in Modal Separation Logic (Invited Talk). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{krebbers:LIPIcs.ITP.2023.2, author = {Krebbers, Robbert}, title = {{Interactive and Automated Proofs in Modal Separation Logic}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {2:1--2:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-284-6}, ISSN = {1868-8969}, year = {2023}, volume = {268}, editor = {Naumowicz, Adam and Thiemann, Ren\'{e}}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.2}, URN = {urn:nbn:de:0030-drops-183770}, doi = {10.4230/LIPIcs.ITP.2023.2}, annote = {Keywords: Program Verification, Separation Logic, Step-Indexing, Modal Logic, Interactive Theorem Proving, Proof Automation, Iris, Coq} }
Published in: DARTS, Volume 3, Issue 2, Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017)
Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 15:1-15:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@Article{kaiser_et_al:DARTS.3.2.15, author = {Kaiser, Jan-Oliver and Dang, Hoang-Hai and Dreyer, Derek and Lahav, Ori and Vafeiadis, Viktor}, title = {{Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact)}}, pages = {15:1--15:2}, journal = {Dagstuhl Artifacts Series}, ISSN = {2509-8195}, year = {2017}, volume = {3}, number = {2}, editor = {Kaiser, Jan-Oliver and Dang, Hoang-Hai and Dreyer, Derek and Lahav, Ori and Vafeiadis, Viktor}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.15}, URN = {urn:nbn:de:0030-drops-72966}, doi = {10.4230/DARTS.3.2.15}, annote = {Keywords: weak memory models, release-acquire, concurrency, separation logic} }
Published in: LIPIcs, Volume 74, 31st European Conference on Object-Oriented Programming (ECOOP 2017)
Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 17:1-17:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{kaiser_et_al:LIPIcs.ECOOP.2017.17, author = {Kaiser, Jan-Oliver and Dang, Hoang-Hai and Dreyer, Derek and Lahav, Ori and Vafeiadis, Viktor}, title = {{Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris}}, booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)}, pages = {17:1--17:29}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-035-4}, ISSN = {1868-8969}, year = {2017}, volume = {74}, editor = {M\"{u}ller, Peter}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.17}, URN = {urn:nbn:de:0030-drops-72753}, doi = {10.4230/LIPIcs.ECOOP.2017.17}, annote = {Keywords: Weak memory models, release-acquire, concurrency, separation logic} }
Feedback for Dagstuhl Publishing