Published in: LIPIcs, Volume 308, 32nd Annual European Symposium on Algorithms (ESA 2024)
Pu Wu, Huanyu Gu, Huiqin Jiang, Zehui Shao, and Jin Xu. A Faster Algorithm for the 4-Coloring Problem. In 32nd Annual European Symposium on Algorithms (ESA 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 308, pp. 103:1-103:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{wu_et_al:LIPIcs.ESA.2024.103, author = {Wu, Pu and Gu, Huanyu and Jiang, Huiqin and Shao, Zehui and Xu, Jin}, title = {{A Faster Algorithm for the 4-Coloring Problem}}, booktitle = {32nd Annual European Symposium on Algorithms (ESA 2024)}, pages = {103:1--103:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-338-6}, ISSN = {1868-8969}, year = {2024}, volume = {308}, editor = {Chan, Timothy and Fischer, Johannes and Iacono, John and Herman, Grzegorz}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2024.103}, URN = {urn:nbn:de:0030-drops-211749}, doi = {10.4230/LIPIcs.ESA.2024.103}, annote = {Keywords: Graph coloring, Graph algorithms, Exact algorithms} }
Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)
Vidush Singhal, Chaitanya Koparkar, Joseph Zullo, Artem Pelenitsyn, Michael Vollmer, Mike Rainey, Ryan Newton, and Milind Kulkarni. Optimizing Layout of Recursive Datatypes with Marmoset: Or, Algorithms + Data Layouts = Efficient Programs. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 38:1-38:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{singhal_et_al:LIPIcs.ECOOP.2024.38, author = {Singhal, Vidush and Koparkar, Chaitanya and Zullo, Joseph and Pelenitsyn, Artem and Vollmer, Michael and Rainey, Mike and Newton, Ryan and Kulkarni, Milind}, title = {{Optimizing Layout of Recursive Datatypes with Marmoset: Or, Algorithms + Data Layouts = Efficient Programs}}, booktitle = {38th European Conference on Object-Oriented Programming (ECOOP 2024)}, pages = {38:1--38: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.38}, URN = {urn:nbn:de:0030-drops-208875}, doi = {10.4230/LIPIcs.ECOOP.2024.38}, annote = {Keywords: Tree traversals, Compilers, Data layout optimization, Dense data layout} }
Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)
Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Petar Maksimović, and Philippa Gardner. Matching Plans for Frame Inference in Compositional Reasoning. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{loow_et_al:LIPIcs.ECOOP.2024.26, author = {L\"{o}\"{o}w, Andreas and Nantes-Sobrinho, Daniele and Ayoun, Sacha-\'{E}lie and Maksimovi\'{c}, Petar and Gardner, Philippa}, title = {{Matching Plans for Frame Inference in Compositional Reasoning}}, booktitle = {38th European Conference on Object-Oriented Programming (ECOOP 2024)}, pages = {26:1--26:20}, 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.26}, URN = {urn:nbn:de:0030-drops-208751}, doi = {10.4230/LIPIcs.ECOOP.2024.26}, annote = {Keywords: Compositional reasoning, separation logic, frame inference} }
Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)
Ke Sun, Di Wang, Sheng Chen, Meng Wang, and Dan Hao. Formalizing, Mechanizing, and Verifying Class-Based Refinement Types. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 39:1-39:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{sun_et_al:LIPIcs.ECOOP.2024.39, author = {Sun, Ke and Wang, Di and Chen, Sheng and Wang, Meng and Hao, Dan}, title = {{Formalizing, Mechanizing, and Verifying Class-Based Refinement Types}}, booktitle = {38th European Conference on Object-Oriented Programming (ECOOP 2024)}, pages = {39:1--39: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.39}, URN = {urn:nbn:de:0030-drops-208881}, doi = {10.4230/LIPIcs.ECOOP.2024.39}, annote = {Keywords: Refinement Types, Program Verification, Object-oriented Programming} }
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 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Samuel Gruetter, Thomas Bourgeat, and Adam Chlipala. Verifying Software Emulation of an Unsupported Hardware Instruction. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 17:1-17:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{gruetter_et_al:LIPIcs.ITP.2024.17, author = {Gruetter, Samuel and Bourgeat, Thomas and Chlipala, Adam}, title = {{Verifying Software Emulation of an Unsupported Hardware Instruction}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {17:1--17: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.17}, URN = {urn:nbn:de:0030-drops-207452}, doi = {10.4230/LIPIcs.ITP.2024.17}, annote = {Keywords: Software verification, Software-hardware boundary, Coq} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Simon Guilloud, Sankalp Gambhir, Andrea Gilot, and Viktor Kunčak. Mechanized HOL Reasoning in Set Theory. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{guilloud_et_al:LIPIcs.ITP.2024.18, author = {Guilloud, Simon and Gambhir, Sankalp and Gilot, Andrea and Kun\v{c}ak, Viktor}, title = {{Mechanized HOL Reasoning in Set Theory}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {18:1--18: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.18}, URN = {urn:nbn:de:0030-drops-207464}, doi = {10.4230/LIPIcs.ITP.2024.18}, annote = {Keywords: Proof assistant, First Order Logic, Set Theory, Higher Order Logic} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Marc Hermes and Robbert Krebbers. Modular Verification of Intrusive List and Tree Data Structures in Separation Logic. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{hermes_et_al:LIPIcs.ITP.2024.19, author = {Hermes, Marc and Krebbers, Robbert}, title = {{Modular Verification of Intrusive List and Tree Data Structures in Separation Logic}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {19:1--19: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.19}, URN = {urn:nbn:de:0030-drops-207478}, doi = {10.4230/LIPIcs.ITP.2024.19}, annote = {Keywords: Separation Logic, Program Verification, Data Structures, Iris, Coq} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Hannes Saffrich. Abstractions for Multi-Sorted Substitutions. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 32:1-32:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{saffrich:LIPIcs.ITP.2024.32, author = {Saffrich, Hannes}, title = {{Abstractions for Multi-Sorted Substitutions}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {32:1--32:19}, 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.32}, URN = {urn:nbn:de:0030-drops-207609}, doi = {10.4230/LIPIcs.ITP.2024.32}, annote = {Keywords: Agda, Metatheory, Framework} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Audrey Seo, Christopher Lam, Dan Grossman, and Talia Ringer. Correctly Compiling Proofs About Programs Without Proving Compilers Correct. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 33:1-33:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{seo_et_al:LIPIcs.ITP.2024.33, author = {Seo, Audrey and Lam, Christopher and Grossman, Dan and Ringer, Talia}, title = {{Correctly Compiling Proofs About Programs Without Proving Compilers Correct}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {33:1--33: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.33}, URN = {urn:nbn:de:0030-drops-207612}, doi = {10.4230/LIPIcs.ITP.2024.33}, annote = {Keywords: proof transformations, compiler validation, program logics, proof engineering} }
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 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Daniel Faber, Adalat Jabrayilov, and Petra Mutzel. SAT Encoding of Partial Ordering Models for Graph Coloring Problems. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{faber_et_al:LIPIcs.SAT.2024.12, author = {Faber, Daniel and Jabrayilov, Adalat and Mutzel, Petra}, title = {{SAT Encoding of Partial Ordering Models for Graph Coloring Problems}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {12:1--12:20}, 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.12}, URN = {urn:nbn:de:0030-drops-205340}, doi = {10.4230/LIPIcs.SAT.2024.12}, annote = {Keywords: Graph coloring, bandwidth coloring, SAT encodings, ILP formulations} }
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} }
Feedback for Dagstuhl Publishing