Search Results

Documents authored by Robinson, Amos

Document
DOI: 10.4230/LIPIcs.ECOOP.2024.34
Pipit on the Post: Proving Pre- and Post-Conditions of Reactive Systems

Authors: Amos Robinson and Alex Potanin

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Synchronous languages such as Lustre and Scade are used to implement safety-critical control systems; proving such programs correct and having the proved properties apply to the compiled code is therefore equally critical. We introduce Pipit, a small synchronous language embedded in F*, designed for verifying control systems and executing them in real-time. Pipit includes a verified translation to transition systems; by reusing F*’s existing proof automation, certain safety properties can be automatically proved by k-induction on the transition system. Pipit can also generate executable code in a subset of F* which is suitable for compilation and real-time execution on embedded devices. The executable code is deterministic and total and preserves the semantics of the original program.
Cite as

Amos Robinson and Alex Potanin. Pipit on the Post: Proving Pre- and Post-Conditions of Reactive Systems. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 34:1-34:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{robinson_et_al:LIPIcs.ECOOP.2024.34,
  author =	{Robinson, Amos and Potanin, Alex},
  title =	{{Pipit on the Post: Proving Pre- and Post-Conditions of Reactive Systems}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{34:1--34: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.34},
  URN =		{urn:nbn:de:0030-drops-208836},
  doi =		{10.4230/LIPIcs.ECOOP.2024.34},
  annote =	{Keywords: Lustre, streaming, reactive, verification}
}
Document
Artifact
DOI: 10.4230/DARTS.10.2.19
Pipit on the Post: Proving Pre- and Post-Conditions of Reactive Systems (Artifact)

Authors: Amos Robinson and Alex Potanin

Published in: DARTS, Volume 10, Issue 2, Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Synchronous languages such as Lustre and Scade are used to implement safety-critical control systems; proving such programs correct and having the proved properties apply to the compiled code is therefore equally critical. We introduce Pipit, a small synchronous language embedded in F*, designed for verifying control systems and executing them in real-time. Pipit includes a verified translation to transition systems; by reusing F*’s existing proof automation, certain safety properties can be automatically proved by k-induction on the transition system. Pipit can also generate executable code in a subset of F* which is suitable for compilation and real-time execution on embedded devices. The executable code is deterministic and total and preserves the semantics of the original program.
Cite as

Amos Robinson and Alex Potanin. Pipit on the Post: Proving Pre- and Post-Conditions of Reactive Systems (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 19:1-19:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{robinson_et_al:DARTS.10.2.19,
  author =	{Robinson, Amos and Potanin, Alex},
  title =	{{Pipit on the Post: Proving Pre- and Post-Conditions of Reactive Systems (Artifact)}},
  pages =	{19:1--19:2},
  journal =	{Dagstuhl Artifacts Series},
  ISBN =	{978-3-95977-342-3},
  ISSN =	{2509-8195},
  year =	{2024},
  volume =	{10},
  number =	{2},
  editor =	{Robinson, Amos and Potanin, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.19},
  URN =		{urn:nbn:de:0030-drops-209177},
  doi =		{10.4230/DARTS.10.2.19},
  annote =	{Keywords: Lustre, streaming, reactive, verification}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact