Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Mohammad Abdulaziz and Thomas Ammer. A Formal Analysis of Capacity Scaling Algorithms for Minimum Cost Flows. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 3:1-3:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{abdulaziz_et_al:LIPIcs.ITP.2024.3, author = {Abdulaziz, Mohammad and Ammer, Thomas}, title = {{A Formal Analysis of Capacity Scaling Algorithms for Minimum Cost Flows}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {3:1--3: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.3}, URN = {urn:nbn:de:0030-drops-207316}, doi = {10.4230/LIPIcs.ITP.2024.3}, annote = {Keywords: Network Flows, Formal Verification, Combinatorial Optimisation} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Martin Desharnais, Balazs Toth, Uwe Waldmann, Jasmin Blanchette, and Sophie Tourret. A Modular Formalization of Superposition in Isabelle/HOL. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{desharnais_et_al:LIPIcs.ITP.2024.12, author = {Desharnais, Martin and Toth, Balazs and Waldmann, Uwe and Blanchette, Jasmin and Tourret, Sophie}, title = {{A Modular Formalization of Superposition in Isabelle/HOL}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {12:1--12: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.12}, URN = {urn:nbn:de:0030-drops-207401}, doi = {10.4230/LIPIcs.ITP.2024.12}, annote = {Keywords: Superposition, verification, first-order logic, higher-order logic} }
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)
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)
Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro, and Marijn J. H. Heule. Formal Verification of the Empty Hexagon Number. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 35:1-35:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{subercaseaux_et_al:LIPIcs.ITP.2024.35, author = {Subercaseaux, Bernardo and Nawrocki, Wojciech and Gallicchio, James and Codel, Cayden and Carneiro, Mario and Heule, Marijn J. H.}, title = {{Formal Verification of the Empty Hexagon Number}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {35:1--35: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.35}, URN = {urn:nbn:de:0030-drops-207633}, doi = {10.4230/LIPIcs.ITP.2024.35}, annote = {Keywords: Empty Hexagon Number, Discrete Computational Geometry, Erd\H{o}s-Szekeres} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Dominik Schreiber. Trusted Scalable SAT Solving with On-The-Fly LRAT Checking. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{schreiber:LIPIcs.SAT.2024.25, author = {Schreiber, Dominik}, title = {{Trusted Scalable SAT Solving with On-The-Fly LRAT Checking}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {25:1--25:19}, 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.25}, URN = {urn:nbn:de:0030-drops-205477}, doi = {10.4230/LIPIcs.SAT.2024.25}, annote = {Keywords: SAT solving, distributed algorithms, proofs} }
Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Peter Lammich. Refinement of Parallel Algorithms down to LLVM. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{lammich:LIPIcs.ITP.2022.24, author = {Lammich, Peter}, title = {{Refinement of Parallel Algorithms down to LLVM}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {24:1--24:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-252-5}, ISSN = {1868-8969}, year = {2022}, volume = {237}, editor = {Andronick, June and de Moura, Leonardo}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.24}, URN = {urn:nbn:de:0030-drops-167333}, doi = {10.4230/LIPIcs.ITP.2022.24}, annote = {Keywords: Isabelle, Concurrent Separation Logic, Parallel Sorting, LLVM} }
Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
Andrei Popescu, Thomas Bauereiss, and Peter Lammich. Bounded-Deducibility Security (Invited Paper). In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 3:1-3:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{popescu_et_al:LIPIcs.ITP.2021.3, author = {Popescu, Andrei and Bauereiss, Thomas and Lammich, Peter}, title = {{Bounded-Deducibility Security}}, booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, pages = {3:1--3:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-188-7}, ISSN = {1868-8969}, year = {2021}, volume = {193}, editor = {Cohen, Liron and Kaliszyk, Cezary}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.3}, URN = {urn:nbn:de:0030-drops-138982}, doi = {10.4230/LIPIcs.ITP.2021.3}, annote = {Keywords: Information-flow security, Unwinding proof method, Compositionality, Verification} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Julian Brunner, Benedikt Seidl, and Salomon Sickert. A Verified and Compositional Translation of LTL to Deterministic Rabin Automata. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{brunner_et_al:LIPIcs.ITP.2019.11, author = {Brunner, Julian and Seidl, Benedikt and Sickert, Salomon}, title = {{A Verified and Compositional Translation of LTL to Deterministic Rabin Automata}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {11:1--11:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-122-1}, ISSN = {1868-8969}, year = {2019}, volume = {141}, editor = {Harrison, John and O'Leary, John and Tolmach, Andrew}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.11}, URN = {urn:nbn:de:0030-drops-110664}, doi = {10.4230/LIPIcs.ITP.2019.11}, annote = {Keywords: Automata Theory, Automata over Infinite Words, Deterministic Automata, Linear Temporal Logic, Model Checking, Verified Algorithms} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Maximilian P. L. Haslbeck and Peter Lammich. Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{haslbeck_et_al:LIPIcs.ITP.2019.20, author = {Haslbeck, Maximilian P. L. and Lammich, Peter}, title = {{Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {20:1--20:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-122-1}, ISSN = {1868-8969}, year = {2019}, volume = {141}, editor = {Harrison, John and O'Leary, John and Tolmach, Andrew}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.20}, URN = {urn:nbn:de:0030-drops-110754}, doi = {10.4230/LIPIcs.ITP.2019.20}, annote = {Keywords: Isabelle, Time Complexity Analysis, Separation Logic, Program Verification, Refinement, Run Time, Algorithms} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Peter Lammich. Generating Verified LLVM from Isabelle/HOL. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 22:1-22:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{lammich:LIPIcs.ITP.2019.22, author = {Lammich, Peter}, title = {{Generating Verified LLVM from Isabelle/HOL}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {22:1--22:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-122-1}, ISSN = {1868-8969}, year = {2019}, volume = {141}, editor = {Harrison, John and O'Leary, John and Tolmach, Andrew}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.22}, URN = {urn:nbn:de:0030-drops-110777}, doi = {10.4230/LIPIcs.ITP.2019.22}, annote = {Keywords: Isabelle/HOL, LLVM, Separation Logic, Verification Condition Generator, Code Generation} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Peter Lammich and Tobias Nipkow. Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{lammich_et_al:LIPIcs.ITP.2019.23, author = {Lammich, Peter and Nipkow, Tobias}, title = {{Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {23:1--23:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-122-1}, ISSN = {1868-8969}, year = {2019}, volume = {141}, editor = {Harrison, John and O'Leary, John and Tolmach, Andrew}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.23}, URN = {urn:nbn:de:0030-drops-110788}, doi = {10.4230/LIPIcs.ITP.2019.23}, annote = {Keywords: Priority queue, Dijkstra’s algorithm, Prim’s algorithm, verification, Isabelle} }
Feedback for Dagstuhl Publishing