2 Search Results for "Zhu, Xiaoyun"

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
DOI: 10.4230/DagRep.5.1.164
Model-driven Algorithms and Architectures for Self-Aware Computing Systems (Dagstuhl Seminar 15041)

Authors: Samuel Kounev, Xiaoyun Zhu, Jeffrey O. Kephart, and Marta Kwiatkowska

Published in: Dagstuhl Reports, Volume 5, Issue 1 (2015)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 15041 "Model-driven Algorithms and Architectures for Self-Aware Computing Systems". The design of self-aware computing systems calls for an integrated interdisciplinary approach building on results from multiple areas of computer science and engineering, including software and systems engineering, systems modeling, simulation and analysis, autonomic and organic computing, machine learning and artificial intelligence, data center resource management, and so on. The Dagstuhl Seminar 15041 served as a platform to raise the awareness about the relevant research efforts in the respective research communities as well as existing synergies that can be exploited to advance the state-of-the-art, formulate a new research agenda that takes a broader view on the problem following an integrated and interdisciplinary approach, and establish collaborations between academia and industry.
Cite as

Samuel Kounev, Xiaoyun Zhu, Jeffrey O. Kephart, and Marta Kwiatkowska. Model-driven Algorithms and Architectures for Self-Aware Computing Systems (Dagstuhl Seminar 15041). In Dagstuhl Reports, Volume 5, Issue 1, pp. 164-196, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{kounev_et_al:DagRep.5.1.164,
  author =	{Kounev, Samuel and Zhu, Xiaoyun and Kephart, Jeffrey O. and Kwiatkowska, Marta},
  title =	{{Model-driven Algorithms and Architectures for Self-Aware Computing Systems (Dagstuhl Seminar 15041)}},
  pages =	{164--196},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{5},
  number =	{1},
  editor =	{Kounev, Samuel and Zhu, Xiaoyun and Kephart, Jeffrey O. and Kwiatkowska, Marta},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.5.1.164},
  URN =		{urn:nbn:de:0030-drops-50385},
  doi =		{10.4230/DagRep.5.1.164},
  annote =	{Keywords: autonomic systems, self-adaptive, self-managing, model-driven, architecture-based, systems management, machine learning, feedback-based design}
}
  • Refine by Author
  • 1 Kephart, Jeffrey O.
  • 1 Kounev, Samuel
  • 1 Kwiatkowska, Marta
  • 1 Potanin, Alex
  • 1 Robinson, Amos
  • Show More...

  • Refine by Classification
  • 1 Computer systems organization → Real-time languages
  • 1 Software and its engineering → Specialized application languages
  • 1 Theory of computation → Program verification

  • Refine by Keyword
  • 1 Lustre
  • 1 architecture-based
  • 1 autonomic systems
  • 1 feedback-based design
  • 1 machine learning
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2015
  • 1 2024

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 Imprint Privacy Contact