Published in: LIPIcs, Volume 319, 38th International Symposium on Distributed Computing (DISC 2024)
Yoav Ben Shimon, Ori Lahav, and Sharon Shoham. Hyperproperty-Preserving Register Specifications. In 38th International Symposium on Distributed Computing (DISC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 319, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{benshimon_et_al:LIPIcs.DISC.2024.8, author = {Ben Shimon, Yoav and Lahav, Ori and Shoham, Sharon}, title = {{Hyperproperty-Preserving Register Specifications}}, booktitle = {38th International Symposium on Distributed Computing (DISC 2024)}, pages = {8:1--8:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-352-2}, ISSN = {1868-8969}, year = {2024}, volume = {319}, editor = {Alistarh, Dan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2024.8}, URN = {urn:nbn:de:0030-drops-212630}, doi = {10.4230/LIPIcs.DISC.2024.8}, annote = {Keywords: Hyperproperties, Concurrent objects, Distributed objects, Linearizability, Strong linearizability, Simulation} }
Published in: LIPIcs, Volume 319, 38th International Symposium on Distributed Computing (DISC 2024)
Armando Castañeda, Gregory Chockler, Brijesh Dongol, and Ori Lahav. What Cannot Be Implemented on Weak Memory?. In 38th International Symposium on Distributed Computing (DISC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 319, pp. 11:1-11:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{castaneda_et_al:LIPIcs.DISC.2024.11, author = {Casta\~{n}eda, Armando and Chockler, Gregory and Dongol, Brijesh and Lahav, Ori}, title = {{What Cannot Be Implemented on Weak Memory?}}, booktitle = {38th International Symposium on Distributed Computing (DISC 2024)}, pages = {11:1--11:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-352-2}, ISSN = {1868-8969}, year = {2024}, volume = {319}, editor = {Alistarh, Dan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2024.11}, URN = {urn:nbn:de:0030-drops-212371}, doi = {10.4230/LIPIcs.DISC.2024.11}, annote = {Keywords: Impossibility, Weak Memory Models, Total-Store Order, Release-Acquire} }
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)
Dan Plyukhin, Marco Peressotti, and Fabrizio Montesi. Ozone: Fully Out-of-Order Choreographies. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 31:1-31:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{plyukhin_et_al:LIPIcs.ECOOP.2024.31, author = {Plyukhin, Dan and Peressotti, Marco and Montesi, Fabrizio}, title = {{Ozone: Fully Out-of-Order Choreographies}}, booktitle = {38th European Conference on Object-Oriented Programming (ECOOP 2024)}, pages = {31:1--31: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.31}, URN = {urn:nbn:de:0030-drops-208800}, doi = {10.4230/LIPIcs.ECOOP.2024.31}, annote = {Keywords: Choreographic programming, Asynchrony, Concurrency} }
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)
Benoît Ballenghien and Burkhart Wolff. An Operational Semantics in Isabelle/HOL-CSP. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{ballenghien_et_al:LIPIcs.ITP.2024.7, author = {Ballenghien, Beno\^{i}t and Wolff, Burkhart}, title = {{An Operational Semantics in Isabelle/HOL-CSP}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {7:1--7:18}, 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.7}, URN = {urn:nbn:de:0030-drops-207355}, doi = {10.4230/LIPIcs.ITP.2024.7}, annote = {Keywords: Process-Algebra, Semantics, Concurrency, Computational Models, Theorem Proving, Isabelle/HOL} }
Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)
S. Akshay, Paul Gastin, R. Govind, and B. Srivathsan. MITL Model Checking via Generalized Timed Automata and a New Liveness Algorithm. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{akshay_et_al:LIPIcs.CONCUR.2024.5, author = {Akshay, S. and Gastin, Paul and Govind, R. and Srivathsan, B.}, title = {{MITL Model Checking via Generalized Timed Automata and a New Liveness Algorithm}}, booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)}, pages = {5:1--5:19}, 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.5}, URN = {urn:nbn:de:0030-drops-207774}, doi = {10.4230/LIPIcs.CONCUR.2024.5}, annote = {Keywords: MITL model checking, timed automata, zones, liveness} }
Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)
Philipp Czerner, Javier Esparza, Valentin Krasotin, and Christoph Welzel-Mohr. Computing Inductive Invariants of Regular Abstraction Frameworks. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{czerner_et_al:LIPIcs.CONCUR.2024.19, author = {Czerner, Philipp and Esparza, Javier and Krasotin, Valentin and Welzel-Mohr, Christoph}, title = {{Computing Inductive Invariants of Regular Abstraction Frameworks}}, booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)}, pages = {19:1--19:18}, 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.19}, URN = {urn:nbn:de:0030-drops-207919}, doi = {10.4230/LIPIcs.CONCUR.2024.19}, annote = {Keywords: Regular model checking, abstraction, inductive invariants} }
Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)
Romain Delpy, Anca Muscholl, and Grégoire Sutre. An Automata-Based Approach for Synchronizable Mailbox Communication. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 22:1-22:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{delpy_et_al:LIPIcs.CONCUR.2024.22, author = {Delpy, Romain and Muscholl, Anca and Sutre, Gr\'{e}goire}, title = {{An Automata-Based Approach for Synchronizable Mailbox Communication}}, booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)}, pages = {22:1--22:19}, 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.22}, URN = {urn:nbn:de:0030-drops-207947}, doi = {10.4230/LIPIcs.CONCUR.2024.22}, annote = {Keywords: Concurrent programming, Mailbox communication, Verification} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Lukáš Holík and Pavol Vargovčík. Antichain with SAT and Tries. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 15:1-15:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{holik_et_al:LIPIcs.SAT.2024.15, author = {Hol{\'\i}k, Luk\'{a}\v{s} and Vargov\v{c}{\'\i}k, Pavol}, title = {{Antichain with SAT and Tries}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {15:1--15:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.15}, URN = {urn:nbn:de:0030-drops-205372}, doi = {10.4230/LIPIcs.SAT.2024.15}, annote = {Keywords: SAT, Trie, Antichain, Alternating automata, Subset query} }
Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)
Ahmed Bouajjani. On Verifying Concurrent Programs Under Weakly Consistent Models (Invited Talk). In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{bouajjani:LIPIcs.CONCUR.2023.2, author = {Bouajjani, Ahmed}, title = {{On Verifying Concurrent Programs Under Weakly Consistent Models}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {2:1--2:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.2}, URN = {urn:nbn:de:0030-drops-189961}, doi = {10.4230/LIPIcs.CONCUR.2023.2}, annote = {Keywords: Concurrent programs, weakly consistent models} }
Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)
Javier Esparza and Fabian Reiter. A Classification of Weak Asynchronous Models of Distributed Computing. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{esparza_et_al:LIPIcs.CONCUR.2020.10, author = {Esparza, Javier and Reiter, Fabian}, title = {{A Classification of Weak Asynchronous Models of Distributed Computing}}, booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)}, pages = {10:1--10:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-160-3}, ISSN = {1868-8969}, year = {2020}, volume = {171}, editor = {Konnov, Igor and Kov\'{a}cs, Laura}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.10}, URN = {urn:nbn:de:0030-drops-128229}, doi = {10.4230/LIPIcs.CONCUR.2020.10}, annote = {Keywords: Asynchrony, Concurrency theory, Weak models of distributed computing} }
Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)
Sidi Mohamed Beillahi, Ahmed Bouajjani, and Constantin Enea. Robustness Against Transactional Causal Consistency. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{beillahi_et_al:LIPIcs.CONCUR.2019.30, author = {Beillahi, Sidi Mohamed and Bouajjani, Ahmed and Enea, Constantin}, title = {{Robustness Against Transactional Causal Consistency}}, booktitle = {30th International Conference on Concurrency Theory (CONCUR 2019)}, pages = {30:1--30:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-121-4}, ISSN = {1868-8969}, year = {2019}, volume = {140}, editor = {Fokkink, Wan and van Glabbeek, Rob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.30}, URN = {urn:nbn:de:0030-drops-109321}, doi = {10.4230/LIPIcs.CONCUR.2019.30}, annote = {Keywords: Distributed Databases, Causal Consistency, Model Checking} }
Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)
Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. Verifying Quantitative Temporal Properties of Procedural Programs. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@InProceedings{atig_et_al:LIPIcs.CONCUR.2018.15, author = {Atig, Mohamed Faouzi and Bouajjani, Ahmed and Narayan Kumar, K. and Saivasan, Prakash}, title = {{Verifying Quantitative Temporal Properties of Procedural Programs}}, booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)}, pages = {15:1--15:17}, 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.15}, URN = {urn:nbn:de:0030-drops-95531}, doi = {10.4230/LIPIcs.CONCUR.2018.15}, annote = {Keywords: Verification, Formal Methods, Pushdown systems, Visibly pushdown, Quantitative Temporal Properties} }
Feedback for Dagstuhl Publishing