3 Search Results for "Brun, Matthias"

Document
DOI: 10.4230/LIPIcs.ITP.2021.10
Verified Progress Tracking for Timely Dataflow

Authors: Matthias Brun, Sára Decova, Andrea Lattuada, and Dmitriy Traytel

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract
Large-scale stream processing systems often follow the dataflow paradigm, which enforces a program structure that exposes a high degree of parallelism. The Timely Dataflow distributed system supports expressive cyclic dataflows for which it offers low-latency data- and pipeline-parallel stream processing. To achieve high expressiveness and performance, Timely Dataflow uses an intricate distributed protocol for tracking the computation’s progress. We modeled the progress tracking protocol as a combination of two independent transition systems in the Isabelle/HOL proof assistant. We specified and verified the safety of the two components and of the combined protocol. To this end, we identified abstract assumptions on dataflow programs that are sufficient for safety and were not previously formalized.
Cite as

Matthias Brun, Sára Decova, Andrea Lattuada, and Dmitriy Traytel. Verified Progress Tracking for Timely Dataflow. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 10:1-10:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{brun_et_al:LIPIcs.ITP.2021.10,
  author =	{Brun, Matthias and Decova, S\'{a}ra and Lattuada, Andrea and Traytel, Dmitriy},
  title =	{{Verified Progress Tracking for Timely Dataflow}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{10:1--10:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.10},
  URN =		{urn:nbn:de:0030-drops-139057},
  doi =		{10.4230/LIPIcs.ITP.2021.10},
  annote =	{Keywords: safety, distributed systems, timely dataflow, Isabelle/HOL}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.10
Generic Authenticated Data Structures, Formally

Authors: Matthias Brun and Dmitriy Traytel

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
Authenticated data structures are a technique for outsourcing data storage and maintenance to an untrusted server. The server is required to produce an efficiently checkable and cryptographically secure proof that it carried out precisely the requested computation. Recently, Miller et al. [https://doi.org/10.1145/2535838.2535851] demonstrated how to support a wide range of such data structures by integrating an authentication construct as a first class citizen in a functional programming language. In this paper, we put this work to the test of formalization in the Isabelle proof assistant. With Isabelle’s help, we uncover and repair several mistakes and modify the small-step semantics to perform call-by-value evaluation rather than requiring terms to be in administrative normal form.
Cite as

Matthias Brun and Dmitriy Traytel. Generic Authenticated Data Structures, Formally. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{brun_et_al:LIPIcs.ITP.2019.10,
  author =	{Brun, Matthias and Traytel, Dmitriy},
  title =	{{Generic Authenticated Data Structures, Formally}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{10:1--10:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.10},
  URN =		{urn:nbn:de:0030-drops-110657},
  doi =		{10.4230/LIPIcs.ITP.2019.10},
  annote =	{Keywords: Authenticated Data Structures, Verifiable Computation, Isabelle/HOL, Nominal Isabelle}
}
Document
DOI: 10.4230/DagSemProc.08031.2
08031 – Software Engineering for Self-Adaptive Systems: A Research Road Map

Authors: Betty H.C. Cheng, Holger Giese, Paola Inverardi, Jeff Magee, Rogerio de Lemos, Jesper Andersson, Basil Becker, Nelly Bencomo, Yuriy Brun, Bojan Cukic, Giovanna Di Marzo Serugendo, Schahram Dustdar, Anthony Finkelstein, Cristina Gacek, Kurt Geihs, Vincenzo Grassi, Gabor Karsai, Holger Kienle, Jeff Kramer, Marin Litoiu, Sam Malek, Raffaela Mirandola, Hausi Müller, Sooyong Park, Mary Shaw, Matthias Tichy, Massimo Tivoli, Danny Weyns, and Jon Whittle

Published in: Dagstuhl Seminar Proceedings, Volume 8031, Software Engineering for Self-Adaptive Systems (2008)

Abstract
Software's ability to adapt at run-time to changing user needs, system intrusions or faults, changing operational environment, and resource variability has been proposed as a means to cope with the complexity of today's software-intensive systems. Such self-adaptive systems can configure and reconfigure themselves, augment their functionality, continually optimize themselves, protect themselves, and recover themselves, while keeping most of their complexity hidden from the user and administrator. In this paper, we present research road map for software engineering of self-adaptive systems focusing on four views, which we identify as essential: requirements, modelling, engineering, and assurances.
Cite as

Betty H.C. Cheng, Holger Giese, Paola Inverardi, Jeff Magee, Rogerio de Lemos, Jesper Andersson, Basil Becker, Nelly Bencomo, Yuriy Brun, Bojan Cukic, Giovanna Di Marzo Serugendo, Schahram Dustdar, Anthony Finkelstein, Cristina Gacek, Kurt Geihs, Vincenzo Grassi, Gabor Karsai, Holger Kienle, Jeff Kramer, Marin Litoiu, Sam Malek, Raffaela Mirandola, Hausi Müller, Sooyong Park, Mary Shaw, Matthias Tichy, Massimo Tivoli, Danny Weyns, and Jon Whittle. 08031 – Software Engineering for Self-Adaptive Systems: A Research Road Map. In Software Engineering for Self-Adaptive Systems. Dagstuhl Seminar Proceedings, Volume 8031, pp. 1-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{cheng_et_al:DagSemProc.08031.2,
  author =	{Cheng, Betty H.C. and Giese, Holger and Inverardi, Paola and Magee, Jeff and de Lemos, Rogerio and Andersson, Jesper and Becker, Basil and Bencomo, Nelly and Brun, Yuriy and Cukic, Bojan and Di Marzo Serugendo, Giovanna and Dustdar, Schahram and Finkelstein, Anthony and Gacek, Cristina and Geihs, Kurt and Grassi, Vincenzo and Karsai, Gabor and Kienle, Holger and Kramer, Jeff and Litoiu, Marin and Malek, Sam and Mirandola, Raffaela and M\"{u}ller, Hausi and Park, Sooyong and Shaw, Mary and Tichy, Matthias and Tivoli, Massimo and Weyns, Danny and Whittle, Jon},
  title =	{{08031 – Software Engineering for Self-Adaptive Systems: A Research Road Map}},
  booktitle =	{Software Engineering for Self-Adaptive Systems},
  pages =	{1--13},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8031},
  editor =	{Betty H. C. Cheng and Rogerio de Lemos and Holger Giese and Paola Inverardi and Jeff Magee},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.08031.2},
  URN =		{urn:nbn:de:0030-drops-15008},
  doi =		{10.4230/DagSemProc.08031.2},
  annote =	{Keywords: Software engineering, requirements engineering, modelling, evolution, assurances, self-adaptability, self-organization, self-management}
}
  • Refine by Author
  • 2 Brun, Matthias
  • 2 Traytel, Dmitriy
  • 1 Andersson, Jesper
  • 1 Becker, Basil
  • 1 Bencomo, Nelly
  • Show More...

  • Refine by Classification
  • 2 Security and privacy → Logic and verification
  • 1 Computing methodologies → Distributed algorithms
  • 1 Software and its engineering → Data flow languages

  • Refine by Keyword
  • 2 Isabelle/HOL
  • 1 Authenticated Data Structures
  • 1 Nominal Isabelle
  • 1 Software engineering
  • 1 Verifiable Computation
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2008
  • 1 2019
  • 1 2021

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