2 Search Results for "Schommer, Bernhard"


Document
homotopy.io: A Proof Assistant for Finitely-Presented Globular n-Categories

Authors: Nathan Corbyn, Lukas Heidemann, Nick Hu, Chiara Sarti, Calin Tataru, and Jamie Vicary

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)


Abstract
We present the proof assistant homotopy.io for working with finitely-presented semistrict higher categories. The tool runs in the browser with a point-and-click interface, allowing direct manipulation of proof objects via a graphical representation. We describe the user interface and explain how the tool can be used in practice. We also describe the essential subsystems of the tool, including collapse, contraction, expansion, typechecking, and layout, as well as key implementation details including data structure encoding, memoisation, and rendering. These technical innovations have been essential for achieving good performance in a resource-constrained setting.

Cite as

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)


Copy BibTex To Clipboard

@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}
}
Document
Embedded Program Annotations for WCET Analysis

Authors: Bernhard Schommer, Christoph Cullmann, Gernot Gebhard, Xavier Leroy, Michael Schmidt, and Simon Wegener

Published in: OASIcs, Volume 63, 18th International Workshop on Worst-Case Execution Time Analysis (WCET 2018)


Abstract
We present __builtin_ais_annot(), a user-friendly, versatile way to transfer annotations (also known as flow facts) written on the source code level to the machine code level. To do so, we couple two tools often used during the development of safety-critical hard real-time systems, the formally verified C compiler CompCert and the static WCET analyzer aiT. CompCert stores the AIS annotations given via __builtin_ais_annot() in a special section of the ELF binary, which can later be extracted automatically by aiT.

Cite as

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)


Copy BibTex To Clipboard

@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}
}
  • Refine by Author
  • 1 Corbyn, Nathan
  • 1 Cullmann, Christoph
  • 1 Gebhard, Gernot
  • 1 Heidemann, Lukas
  • 1 Hu, Nick
  • Show More...

  • Refine by Classification
  • 1 Computer systems organization → Real-time systems
  • 1 Hardware → Static timing analysis
  • 1 Software and its engineering → Automated static analysis
  • 1 Software and its engineering → Compilers
  • 1 Software and its engineering → Embedded software
  • Show More...

  • Refine by Keyword
  • 1 Annotation Support
  • 1 CompCert
  • 1 Higher category theory
  • 1 Tool Coupling
  • 1 Worst-Case Execution Time (WCET) Analysis
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2018
  • 1 2024