Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)
Nisarg Patel, Dennis Shasha, and Thomas Wies. Verifying Lock-Free Search Structure Templates. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 30:1-30:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{patel_et_al:LIPIcs.ECOOP.2024.30, author = {Patel, Nisarg and Shasha, Dennis and Wies, Thomas}, title = {{Verifying Lock-Free Search Structure Templates}}, booktitle = {38th European Conference on Object-Oriented Programming (ECOOP 2024)}, pages = {30:1--30:28}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-341-6}, ISSN = {1868-8969}, year = {2024}, volume = {313}, editor = {Aldrich, Jonathan and Salvaneschi, Guido}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.30}, URN = {urn:nbn:de:0030-drops-208797}, doi = {10.4230/LIPIcs.ECOOP.2024.30}, annote = {Keywords: skiplists, lock-free, separation logic, linearizability, future-dependent linearization points, hindsight reasoning} }
Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)
Aleksey Veresov, Jonas Spenger, Paris Carbone, and Philipp Haller. Failure Transparency in Stateful Dataflow Systems. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 42:1-42:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{veresov_et_al:LIPIcs.ECOOP.2024.42, author = {Veresov, Aleksey and Spenger, Jonas and Carbone, Paris and Haller, Philipp}, title = {{Failure Transparency in Stateful Dataflow Systems}}, booktitle = {38th European Conference on Object-Oriented Programming (ECOOP 2024)}, pages = {42:1--42:31}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-341-6}, ISSN = {1868-8969}, year = {2024}, volume = {313}, editor = {Aldrich, Jonathan and Salvaneschi, Guido}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.42}, URN = {urn:nbn:de:0030-drops-208911}, doi = {10.4230/LIPIcs.ECOOP.2024.42}, annote = {Keywords: Failure transparency, stateful dataflow, operational semantics, checkpoint recovery} }
Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)
Scott Wesley, Maria Christakis, Jorge A. Navas, Richard Trefler, Valentin Wüstholz, and Arie Gurfinkel. Inductive Predicate Synthesis Modulo Programs. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 43:1-43:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{wesley_et_al:LIPIcs.ECOOP.2024.43, author = {Wesley, Scott and Christakis, Maria and Navas, Jorge A. and Trefler, Richard and W\"{u}stholz, Valentin and Gurfinkel, Arie}, title = {{Inductive Predicate Synthesis Modulo Programs}}, booktitle = {38th European Conference on Object-Oriented Programming (ECOOP 2024)}, pages = {43:1--43:30}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-341-6}, ISSN = {1868-8969}, year = {2024}, volume = {313}, editor = {Aldrich, Jonathan and Salvaneschi, Guido}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.43}, URN = {urn:nbn:de:0030-drops-208926}, doi = {10.4230/LIPIcs.ECOOP.2024.43}, annote = {Keywords: Software Verification, Invariant Synthesis, Model-Checking} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Vincent Jackson, Toby Murray, and Christine Rizkallah. A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{jackson_et_al:LIPIcs.ITP.2024.23, author = {Jackson, Vincent and Murray, Toby and Rizkallah, Christine}, title = {{A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {23:1--23:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-337-9}, ISSN = {1868-8969}, year = {2024}, volume = {309}, editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.23}, URN = {urn:nbn:de:0030-drops-207510}, doi = {10.4230/LIPIcs.ITP.2024.23}, annote = {Keywords: verification, concurrency, rely-guarantee, separation logic, resource algebras} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Andrew Tolmach, Chris Chhak, and Sean Anderson. Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 36:1-36:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{tolmach_et_al:LIPIcs.ITP.2024.36, author = {Tolmach, Andrew and Chhak, Chris and Anderson, Sean}, title = {{Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {36:1--36:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-337-9}, ISSN = {1868-8969}, year = {2024}, volume = {309}, editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.36}, URN = {urn:nbn:de:0030-drops-207643}, doi = {10.4230/LIPIcs.ITP.2024.36}, annote = {Keywords: Compiler verification, C language semantics, Coq proof assistant} }
Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)
Aristotelis Koutsouridis, Michalis Kokologiannakis, and Viktor Vafeiadis. Automating Memory Model Metatheory with Intersections. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 33:1-33:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{koutsouridis_et_al:LIPIcs.CONCUR.2024.33, author = {Koutsouridis, Aristotelis and Kokologiannakis, Michalis and Vafeiadis, Viktor}, title = {{Automating Memory Model Metatheory with Intersections}}, booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)}, pages = {33:1--33:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-339-3}, ISSN = {1868-8969}, year = {2024}, volume = {311}, editor = {Majumdar, Rupak and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.33}, URN = {urn:nbn:de:0030-drops-208050}, doi = {10.4230/LIPIcs.CONCUR.2024.33}, annote = {Keywords: Kleene Algebra, Weak Memory Models} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Beniamino Accattoli and Adrienne Lancelot. Mirroring Call-By-Need, or Values Acting Silly. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 23:1-23:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{accattoli_et_al:LIPIcs.FSCD.2024.23, author = {Accattoli, Beniamino and Lancelot, Adrienne}, title = {{Mirroring Call-By-Need, or Values Acting Silly}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {23:1--23:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.23}, URN = {urn:nbn:de:0030-drops-203527}, doi = {10.4230/LIPIcs.FSCD.2024.23}, annote = {Keywords: Lambda calculus, intersection types, call-by-value, call-by-need} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Beniamino Accattoli and Claudio Sacerdoti Coen. IMELL Cut Elimination with Linear Overhead. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 24:1-24:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{accattoli_et_al:LIPIcs.FSCD.2024.24, author = {Accattoli, Beniamino and Sacerdoti Coen, Claudio}, title = {{IMELL Cut Elimination with Linear Overhead}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {24:1--24:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.24}, URN = {urn:nbn:de:0030-drops-203539}, doi = {10.4230/LIPIcs.FSCD.2024.24}, annote = {Keywords: Lambda calculus, linear logic, abstract machines} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Delia Kesner, Delia Kesner, Victor Arrial, Victor Arrial, Giulio Guerrieri, and Giulio Guerrieri. Meaningfulness and Genericity in a Subsuming Framework (Invited Talk). In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 1:1-1:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{kesner_et_al:LIPIcs.FSCD.2024.1, author = {Kesner, Delia and Arrial, Victor and Guerrieri, Giulio}, title = {{Meaningfulness and Genericity in a Subsuming Framework}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {1:1--1:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.1}, URN = {urn:nbn:de:0030-drops-203305}, doi = {10.4230/LIPIcs.FSCD.2024.1}, annote = {Keywords: Lambda calculus, Solvability, Meaningfulness, Inhabitation, Genericity} }
Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)
Ashish Mishra and Suresh Jagannathan. Morpheus: Automated Safety Verification of Data-Dependent Parser Combinator Programs. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 20:1-20:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{mishra_et_al:LIPIcs.ECOOP.2023.20, author = {Mishra, Ashish and Jagannathan, Suresh}, title = {{Morpheus: Automated Safety Verification of Data-Dependent Parser Combinator Programs}}, booktitle = {37th European Conference on Object-Oriented Programming (ECOOP 2023)}, pages = {20:1--20:27}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-281-5}, ISSN = {1868-8969}, year = {2023}, volume = {263}, editor = {Ali, Karim and Salvaneschi, Guido}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.20}, URN = {urn:nbn:de:0030-drops-182138}, doi = {10.4230/LIPIcs.ECOOP.2023.20}, annote = {Keywords: Parsers, Verification, Domain-specific languages, Functional programming, Refinement types, Type systems} }
Published in: LIPIcs, Volume 136, 3rd Summit on Advances in Programming Languages (SNAPL 2019)
Gowtham Kaki, KC Sivaramakrishnan, and Suresh Jagannathan. Version Control Is for Your Data Too. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{kaki_et_al:LIPIcs.SNAPL.2019.8, author = {Kaki, Gowtham and Sivaramakrishnan, KC and Jagannathan, Suresh}, title = {{Version Control Is for Your Data Too}}, booktitle = {3rd Summit on Advances in Programming Languages (SNAPL 2019)}, pages = {8:1--8:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-113-9}, ISSN = {1868-8969}, year = {2019}, volume = {136}, editor = {Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.8}, URN = {urn:nbn:de:0030-drops-105516}, doi = {10.4230/LIPIcs.SNAPL.2019.8}, annote = {Keywords: replication, distributed systems, version control} }
Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)
Kartik Nagar and Suresh Jagannathan. Automated Detection of Serializability Violations Under Weak Consistency. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 41:1-41:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@InProceedings{nagar_et_al:LIPIcs.CONCUR.2018.41, author = {Nagar, Kartik and Jagannathan, Suresh}, title = {{Automated Detection of Serializability Violations Under Weak Consistency}}, booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)}, pages = {41:1--41:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-087-3}, ISSN = {1868-8969}, year = {2018}, volume = {118}, editor = {Schewe, Sven and Zhang, Lijun}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.41}, URN = {urn:nbn:de:0030-drops-95799}, doi = {10.4230/LIPIcs.CONCUR.2018.41}, annote = {Keywords: Weak Consistency, Serializability, Database Applications} }
Published in: Dagstuhl Reports, Volume 6, Issue 3 (2016)
Marco Gaboardi, Suresh Jagannathan, Ranjit Jhala, and Stephanie Weirich. Language Based Verification Tools for Functional Programs (Dagstuhl Seminar 16131). In Dagstuhl Reports, Volume 6, Issue 3, pp. 59-77, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@Article{gaboardi_et_al:DagRep.6.3.59, author = {Gaboardi, Marco and Jagannathan, Suresh and Jhala, Ranjit and Weirich, Stephanie}, title = {{Language Based Verification Tools for Functional Programs (Dagstuhl Seminar 16131)}}, pages = {59--77}, journal = {Dagstuhl Reports}, ISSN = {2192-5283}, year = {2016}, volume = {6}, number = {3}, editor = {Gaboardi, Marco and Jagannathan, Suresh and Jhala, Ranjit and Weirich, Stephanie}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.6.3.59}, URN = {urn:nbn:de:0030-drops-61494}, doi = {10.4230/DagRep.6.3.59}, annote = {Keywords: Functional Programming, Type Systems, Contracts, Dependent Types, Model Checking, Program Analysis} }
Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)
Suresh Jagannathan. Relational Refinement Types for Higher-Order Shape Transformers (Invited Talk). In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, p. 9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{jagannathan:LIPIcs.FSTTCS.2015.9, author = {Jagannathan, Suresh}, title = {{Relational Refinement Types for Higher-Order Shape Transformers}}, booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)}, pages = {9--9}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-97-2}, ISSN = {1868-8969}, year = {2015}, volume = {45}, editor = {Harsha, Prahladh and Ramalingam, G.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.9}, URN = {urn:nbn:de:0030-drops-56406}, doi = {10.4230/LIPIcs.FSTTCS.2015.9}, annote = {Keywords: Relational Specifications; Inductive and Parametric Relations; Refinement Types, Shape Analysis, Data Structure Verification\}} }
Published in: LIPIcs, Volume 37, 29th European Conference on Object-Oriented Programming (ECOOP 2015)
Gustavo Petri, Jan Vitek, and Suresh Jagannathan. Cooking the Books: Formalizing JMM Implementation Recipes. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 445-469, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{petri_et_al:LIPIcs.ECOOP.2015.445, author = {Petri, Gustavo and Vitek, Jan and Jagannathan, Suresh}, title = {{Cooking the Books: Formalizing JMM Implementation Recipes}}, booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)}, pages = {445--469}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-86-6}, ISSN = {1868-8969}, year = {2015}, volume = {37}, editor = {Boyland, John Tang}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.445}, URN = {urn:nbn:de:0030-drops-52334}, doi = {10.4230/LIPIcs.ECOOP.2015.445}, annote = {Keywords: Concurrency, Java, Memory Model, Relaxed-Memory} }
Feedback for Dagstuhl Publishing