5 Search Results for "Foster, Nate"

Document
DOI: 10.4230/LIPIcs.ECOOP.2023.21
Automata Learning with an Incomplete Teacher

Authors: Mark Moeller, Thomas Wiener, Alaia Solko-Breslin, Caleb Koch, Nate Foster, and Alexandra Silva

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
The preceding decade has seen significant interest in use of active learning to build models of programs and protocols. But existing algorithms assume the existence of an idealized oracle - a so-called Minimally Adequate Teacher (MAT) - that cannot be fully realized in practice and so is usually approximated with testing. This work proposes a new framework for active learning based on an incomplete teacher. This new formulation, called iMAT, neatly handles scenarios in which the teacher has access to only a finite number of tests or otherwise has gaps in its knowledge. We adapt Angluin’s L^⋆ algorithm for learning finite automata to incomplete teachers and we build a prototype implementation in OCaml that uses an SMT solver to help fill in information not supplied by the teacher. We demonstrate the behavior of our iMAT prototype on a variety of learning problems from a standard benchmark suite.
Cite as

Mark Moeller, Thomas Wiener, Alaia Solko-Breslin, Caleb Koch, Nate Foster, and Alexandra Silva. Automata Learning with an Incomplete Teacher. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 21:1-21:30, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{moeller_et_al:LIPIcs.ECOOP.2023.21,
  author =	{Moeller, Mark and Wiener, Thomas and Solko-Breslin, Alaia and Koch, Caleb and Foster, Nate and Silva, Alexandra},
  title =	{{Automata Learning with an Incomplete Teacher}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{21:1--21:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim 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.2023.21},
  URN =		{urn:nbn:de:0030-drops-182145},
  doi =		{10.4230/LIPIcs.ECOOP.2023.21},
  annote =	{Keywords: Finite Automata, Active Learning, SMT Solvers}
}
Document
DOI: 10.4230/DagRep.9.3.178
Programmable Network Data Planes (Dagstuhl Seminar 19141)

Authors: Gianni Antichi, Theophilus Benson, Nate Foster, Fernando M. V. Ramos, and Justine Sherry

Published in: Dagstuhl Reports, Volume 9, Issue 3 (2019)

Abstract
Software-Defined Networking (SDN) started the "softwarization" of networking. By relocating the control plane onto a logically centralized machine, SDN gave programmers the ability to specify the behavior of the network directly in software, unleashing a major transformation both in the networking research community and in industry. However, a key limitation of the original SDN vision was the limited functionality exposed in protocols such as OpenFlow. Recent efforts to develop reconfigurable data planes and high-level network programming languages has made it possible to truly program the data plane -- i.e., to change the way packets are processed on network devices. The ability to fully program the network-both control and data plane-is expected have a profound impact on the field of networking in the coming years. In this seminar we discussed the key questions and problems to be addressed in the next 10 years on the area of programmable dataplanes, and how they will potentially shape the future of networking. As an outcome we are now working on a research agenda to serve as the start of a discussion with networking researchers, practitioners, and the industry as a whole. This report is a first step towards that goal.
Cite as

Gianni Antichi, Theophilus Benson, Nate Foster, Fernando M. V. Ramos, and Justine Sherry. Programmable Network Data Planes (Dagstuhl Seminar 19141). In Dagstuhl Reports, Volume 9, Issue 3, pp. 178-201, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{antichi_et_al:DagRep.9.3.178,
  author =	{Antichi, Gianni and Benson, Theophilus and Foster, Nate and Ramos, Fernando M. V. and Sherry, Justine},
  title =	{{Programmable Network Data Planes (Dagstuhl Seminar 19141)}},
  pages =	{178--201},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2019},
  volume =	{9},
  number =	{3},
  editor =	{Antichi, Gianni and Benson, Theophilus and Foster, Nate and Ramos, Fernando M. V. and Sherry, Justine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.9.3.178},
  URN =		{urn:nbn:de:0030-drops-112958},
  doi =		{10.4230/DagRep.9.3.178},
  annote =	{Keywords: programmable data planes, software-defined networks, programmable networks}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.MFCS.2019.2
Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time (Invited Talk)

Authors: Alexandra Silva

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)

Abstract
Guarded Kleene Algebra with Tests (GKAT) is a variation on Kleene Algebra with Tests (KAT) that arises by restricting the union (+) and iteration (*) operations from KAT to predicate-guarded versions. We develop the (co)algebraic theory of GKAT and show how it can be efficiently used to reason about imperative programs. In contrast to KAT, whose equational theory is PSPACE-complete, we show that the equational theory of GKAT is (almost) linear time. We also provide a full Kleene theorem and prove completeness for an analogue of Salomaa’s axiomatization of Kleene Algebra. We will also discuss how this result has practical implications in the verification of programs, with examples from network and probabilistic programming. This is joint work with Nate Foster, Justin Hsu, Tobias Kappe, Dexter Kozen, and Steffen Smolka.
Cite as

Alexandra Silva. Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time (Invited Talk). In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, p. 2:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{silva:LIPIcs.MFCS.2019.2,
  author =	{Silva, Alexandra},
  title =	{{Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{2:1--2:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.2},
  URN =		{urn:nbn:de:0030-drops-109462},
  doi =		{10.4230/LIPIcs.MFCS.2019.2},
  annote =	{Keywords: Kleene algebra, verification, decision procedures}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2019.12
How to Avoid Making a Billion-Dollar Mistake: Type-Safe Data Plane Programming with SafeP4

Authors: Matthias Eichholz, Eric Campbell, Nate Foster, Guido Salvaneschi, and Mira Mezini

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)

Abstract
The P4 programming language offers high-level, declarative abstractions that bring the flexibility of software to the domain of networking. Unfortunately, the main abstraction used to represent packet data in P4, namely header types, lacks basic safety guarantees. Over the last few years, experience with an increasing number of programs has shown the risks of the unsafe approach, which often leads to subtle software bugs. This paper proposes SafeP4, a domain-specific language for programmable data planes in which all packet data is guaranteed to have a well-defined meaning and satisfy essential safety guarantees. We equip SafeP4 with a formal semantics and a static type system that statically guarantees header validity - a common source of safety bugs according to our analysis of real-world P4 programs. Statically ensuring header validity is challenging because the set of valid headers can be modified at runtime, making it a dynamic program property. Our type system achieves static safety by using a form of path-sensitive reasoning that tracks dynamic information from conditional statements, routing tables, and the control plane. Our evaluation shows that SafeP4’s type system can effectively eliminate common failures in many real-world programs.
Cite as

Matthias Eichholz, Eric Campbell, Nate Foster, Guido Salvaneschi, and Mira Mezini. How to Avoid Making a Billion-Dollar Mistake: Type-Safe Data Plane Programming with SafeP4. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 12:1-12:28, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{eichholz_et_al:LIPIcs.ECOOP.2019.12,
  author =	{Eichholz, Matthias and Campbell, Eric and Foster, Nate and Salvaneschi, Guido and Mezini, Mira},
  title =	{{How to Avoid Making a Billion-Dollar Mistake: Type-Safe Data Plane Programming with SafeP4}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{12:1--12:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.12},
  URN =		{urn:nbn:de:0030-drops-108041},
  doi =		{10.4230/LIPIcs.ECOOP.2019.12},
  annote =	{Keywords: P4, data plane programming, type systems}
}
Document
DOI: 10.4230/DagRep.5.2.44
Formal Foundations for Networking (Dagstuhl Seminar 15071)

Authors: Nikolaj Bjorner, Nate Foster, Philip Brighten Godfrey, and Pamela Zave

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

Abstract
This report documents the program and outcomes of Dagstuhl Seminar 15071 "Formal Foundations for Networking." Networking is in the midst of a revolution being driven by rapidly expanding infrastructures and emerging software-defined networking architectures. There is a growing need for tools and methodologies that provide rigorous guarantees about performance, reliability, and security. This seminar brought together leading researchers and practitioners from the fields of formal methods, networking, programming languages, and security, to investigate the task of developing formal foundations for networks.
Cite as

Nikolaj Bjorner, Nate Foster, Philip Brighten Godfrey, and Pamela Zave. Formal Foundations for Networking (Dagstuhl Seminar 15071). In Dagstuhl Reports, Volume 5, Issue 2, pp. 44-63, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{bjorner_et_al:DagRep.5.2.44,
  author =	{Bjorner, Nikolaj and Foster, Nate and Godfrey, Philip Brighten and Zave, Pamela},
  title =	{{Formal Foundations for Networking (Dagstuhl Seminar 15071)}},
  pages =	{44--63},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{5},
  number =	{2},
  editor =	{Bjorner, Nikolaj and Foster, Nate and Godfrey, Philip Brighten and Zave, Pamela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.5.2.44},
  URN =		{urn:nbn:de:0030-drops-50440},
  doi =		{10.4230/DagRep.5.2.44},
  annote =	{Keywords: Formal methods, logic, middleboxes, model checking, networking, program synthesis, security, software-defined networking, verification}
}
  • Refine by Author
  • 4 Foster, Nate
  • 2 Silva, Alexandra
  • 1 Antichi, Gianni
  • 1 Benson, Theophilus
  • 1 Bjorner, Nikolaj
  • Show More...

  • Refine by Classification
  • 1 Networks → Programming interfaces
  • 1 Software and its engineering → Formal language definitions
  • 1 Theory of computation → Active learning
  • 1 Theory of computation → Formal languages and automata theory

  • Refine by Keyword
  • 2 verification
  • 1 Active Learning
  • 1 Finite Automata
  • 1 Formal methods
  • 1 Kleene algebra
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 3 2019
  • 1 2015
  • 1 2023

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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact