DARTS.10.2.19.pdf
- Filesize: 464 kB
- 2 pages
Document
Pipit on the Post: Proving Pre- and Post-Conditions of Reactive Systems (Artifact)
Authors
Amos Robinson 
,
Alex Potanin
-
Part of:
Issue:
Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024)
Volume: DARTS, Volume 10 (ECOOP 2024)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2024-09-12
Artifact Description
Document Identifiers
Author Details
Cite As Get BibTex
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)
https://doi.org/10.4230/DARTS.10.2.19
Artifact
DARTS-10-2-19-artifact-d189cb98071ea28d01ac2f98cb52bf42.tar.gz
(Filesize: 10.24 MB)
MD5 Sum:
d189cb98071ea28d01ac2f98cb52bf42
(Get MD5 Sum)
Artifact Evaluation Policy
The artifact has been evaluated as described in the ECOOP 2024 Call for Artifacts and the ACM Artifact Review and Badging Policy.
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.
Subject Classification
ACM Subject Classification
- Computer systems organization → Real-time languages
- Theory of computation → Program verification
- Software and its engineering → Specialized application languages
Keywords
- Lustre
- streaming
- reactive
- verification
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads