Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Siddharth Bhat, Alex Keizer, Chris Hughes, Andrés Goens, and Tobias Grosser. Verifying Peephole Rewriting in SSA Compiler IRs. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 9:1-9:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{bhat_et_al:LIPIcs.ITP.2024.9, author = {Bhat, Siddharth and Keizer, Alex and Hughes, Chris and Goens, Andr\'{e}s and Grosser, Tobias}, title = {{Verifying Peephole Rewriting in SSA Compiler IRs}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {9:1--9: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.9}, URN = {urn:nbn:de:0030-drops-207372}, doi = {10.4230/LIPIcs.ITP.2024.9}, annote = {Keywords: compilers, semantics, mechanization, MLIR, SSA, regions, peephole rewrites} }
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)
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)
Martin Rau and Tobias Nipkow. A Verified Earley Parser. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 31:1-31:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{rau_et_al:LIPIcs.ITP.2024.31, author = {Rau, Martin and Nipkow, Tobias}, title = {{A Verified Earley Parser}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {31:1--31: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.31}, URN = {urn:nbn:de:0030-drops-207596}, doi = {10.4230/LIPIcs.ITP.2024.31}, annote = {Keywords: Verification, Parsers, Earley, Isabelle} }
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 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Martina Seidl. Models and Counter-Models of Quantified Boolean Formulas (Invited Talk). In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 1:1-1:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{seidl:LIPIcs.SAT.2024.1, author = {Seidl, Martina}, title = {{Models and Counter-Models of Quantified Boolean Formulas}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {1:1--1:7}, 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.1}, URN = {urn:nbn:de:0030-drops-205238}, doi = {10.4230/LIPIcs.SAT.2024.1}, annote = {Keywords: Quantified Boolean Formula, Solution Extraction, Solution Counting} }
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 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Friedrich Slivovsky. Strategy Extraction by Interpolation. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{slivovsky:LIPIcs.SAT.2024.28, author = {Slivovsky, Friedrich}, title = {{Strategy Extraction by Interpolation}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {28:1--28: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.28}, URN = {urn:nbn:de:0030-drops-205509}, doi = {10.4230/LIPIcs.SAT.2024.28}, annote = {Keywords: QBF, Expansion, Strategy Extraction, Interpolation} }
Published in: OASIcs, Volume 121, 22nd International Workshop on Worst-Case Execution Time Analysis (WCET 2024)
Emad Jacob Maroun, Eva Dengler, Christian Dietrich, Stefan Hepp, Henriette Herzog, Benedikt Huber, Jens Knoop, Daniel Wiltsche-Prokesch, Peter Puschner, Phillip Raffeck, Martin Schoeberl, Simon Schuster, and Peter Wägemann. The Platin Multi-Target Worst-Case Analysis Tool. In 22nd International Workshop on Worst-Case Execution Time Analysis (WCET 2024). Open Access Series in Informatics (OASIcs), Volume 121, pp. 2:1-2:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{maroun_et_al:OASIcs.WCET.2024.2, author = {Maroun, Emad Jacob and Dengler, Eva and Dietrich, Christian and Hepp, Stefan and Herzog, Henriette and Huber, Benedikt and Knoop, Jens and Wiltsche-Prokesch, Daniel and Puschner, Peter and Raffeck, Phillip and Schoeberl, Martin and Schuster, Simon and W\"{a}gemann, Peter}, title = {{The Platin Multi-Target Worst-Case Analysis Tool}}, booktitle = {22nd International Workshop on Worst-Case Execution Time Analysis (WCET 2024)}, pages = {2:1--2:14}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-95977-346-1}, ISSN = {2190-6807}, year = {2024}, volume = {121}, editor = {Carle, Thomas}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2024.2}, URN = {urn:nbn:de:0030-drops-204704}, doi = {10.4230/OASIcs.WCET.2024.2}, annote = {Keywords: worst-case resource consumption, WCET, static analysis tool} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, and Alan Schmitt. Optimizing a Non-Deterministic Abstract Machine with Environments. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 11:1-11:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{biernacka_et_al:LIPIcs.FSCD.2024.11, author = {Biernacka, Ma{\l}gorzata and Biernacki, Dariusz and Lenglet, Sergue\"{i} and Schmitt, Alan}, title = {{Optimizing a Non-Deterministic Abstract Machine with Environments}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {11:1--11:22}, 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.11}, URN = {urn:nbn:de:0030-drops-203409}, doi = {10.4230/LIPIcs.FSCD.2024.11}, annote = {Keywords: Abstract machine, Explicit substitutions, Refocusing} }
Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
Pierre Nigron and Pierre-Évariste Dagand. Reaching for the Star: Tale of a Monad in Coq. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 29:1-29:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{nigron_et_al:LIPIcs.ITP.2021.29, author = {Nigron, Pierre and Dagand, Pierre-\'{E}variste}, title = {{Reaching for the Star: Tale of a Monad in Coq}}, booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, pages = {29:1--29:19}, 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.29}, URN = {urn:nbn:de:0030-drops-139241}, doi = {10.4230/LIPIcs.ITP.2021.29}, annote = {Keywords: monads, hoare logic, separation logic, Coq} }
Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)
Davide Ancona, Francesco Dagnino, Jurriaan Rot, and Elena Zucca. A Big Step from Finite to Infinite Computations (SCICO Journal-first). In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 32:1-32:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{ancona_et_al:LIPIcs.ECOOP.2020.32, author = {Ancona, Davide and Dagnino, Francesco and Rot, Jurriaan and Zucca, Elena}, title = {{A Big Step from Finite to Infinite Computations}}, booktitle = {34th European Conference on Object-Oriented Programming (ECOOP 2020)}, pages = {32:1--32:2}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-154-2}, ISSN = {1868-8969}, year = {2020}, volume = {166}, editor = {Hirschfeld, Robert and Pape, Tobias}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.32}, URN = {urn:nbn:de:0030-drops-131895}, doi = {10.4230/LIPIcs.ECOOP.2020.32}, annote = {Keywords: Operational semantics, coinduction, infinite behaviour} }
Published in: OASIcs, Volume 63, 18th International Workshop on Worst-Case Execution Time Analysis (WCET 2018)
Bernhard Schommer, Christoph Cullmann, Gernot Gebhard, Xavier Leroy, Michael Schmidt, and Simon Wegener. Embedded Program Annotations for WCET Analysis. In 18th International Workshop on Worst-Case Execution Time Analysis (WCET 2018). Open Access Series in Informatics (OASIcs), Volume 63, pp. 8:1-8:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@InProceedings{schommer_et_al:OASIcs.WCET.2018.8, author = {Schommer, Bernhard and Cullmann, Christoph and Gebhard, Gernot and Leroy, Xavier and Schmidt, Michael and Wegener, Simon}, title = {{Embedded Program Annotations for WCET Analysis}}, booktitle = {18th International Workshop on Worst-Case Execution Time Analysis (WCET 2018)}, pages = {8:1--8:13}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-95977-073-6}, ISSN = {2190-6807}, year = {2018}, volume = {63}, editor = {Brandner, Florian}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2018.8}, URN = {urn:nbn:de:0030-drops-97543}, doi = {10.4230/OASIcs.WCET.2018.8}, annote = {Keywords: Worst-Case Execution Time (WCET) Analysis, Annotation Support, CompCert, Tool Coupling, aiT} }
Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)
Xavier Leroy. Formally Verifying a Compiler: What Does It Mean, Exactly? (Invited Talk). In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@InProceedings{leroy:LIPIcs.ICALP.2016.2, author = {Leroy, Xavier}, title = {{Formally Verifying a Compiler: What Does It Mean, Exactly?}}, booktitle = {43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)}, pages = {2:1--2:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-013-2}, ISSN = {1868-8969}, year = {2016}, volume = {55}, editor = {Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.2}, URN = {urn:nbn:de:0030-drops-63384}, doi = {10.4230/LIPIcs.ICALP.2016.2}, annote = {Keywords: Compilers, Compiler Optimization, Compiler Verification} }
Feedback for Dagstuhl Publishing