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: 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)
Nathan Corbyn, Lukas Heidemann, Nick Hu, Chiara Sarti, Calin Tataru, and Jamie Vicary. homotopy.io: A Proof Assistant for Finitely-Presented Globular n-Categories. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 30:1-30:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{corbyn_et_al:LIPIcs.FSCD.2024.30, author = {Corbyn, Nathan and Heidemann, Lukas and Hu, Nick and Sarti, Chiara and Tataru, Calin and Vicary, Jamie}, title = {{homotopy.io: A Proof Assistant for Finitely-Presented Globular n-Categories}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {30:1--30:26}, 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.30}, URN = {urn:nbn:de:0030-drops-203594}, doi = {10.4230/LIPIcs.FSCD.2024.30}, annote = {Keywords: Higher category theory, proof assistant, string diagrams} }
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} }
Feedback for Dagstuhl Publishing