2 Search Results for "Panda, Aurojit"


Document
Invited Talk
Simple Invariants for Proving the Safety of Distributed Protocols (Invited Talk)

Authors: Mooly Sagiv

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)


Abstract
Safety of a distributed protocol means that the protocol never reaches a bad state, e.g., a state where two nodes become leaders in a leader-election protocol. Proving safety is obviously undecidable since such protocols are run by an unbounded number of nodes, and their safety needs to be established for any number of nodes. I will describe a deductive approach for proving safety, based on the concept of universally quantified inductive invariants—an adaptation of the mathematical concept of induction to the domain of programs. In the deductive approach, the programmer specifies a candidate inductive invariant and the system automatically checks if it is inductive. By restricting the invariants to be universally quantified, this approach can be effectively implemented with a SAT solver. This is a joint work with Ken McMillan (Microsoft Research), Oded Padon (Tel Aviv University), Aurojit Panda (UC Berkeley), and Sharon Shoham (Tel Aviv University) and was integrated into the IVY system. The work is inspired by Shachar Itzhaky's thesis.

Cite as

Mooly Sagiv. Simple Invariants for Proving the Safety of Distributed Protocols (Invited Talk). In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{sagiv:LIPIcs.FSTTCS.2016.2,
  author =	{Sagiv, Mooly},
  title =	{{Simple Invariants for Proving the Safety of Distributed Protocols}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{2:1--2:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.2},
  URN =		{urn:nbn:de:0030-drops-68877},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.2},
  annote =	{Keywords: Program verification, Distributed protocols, Deductive reasoning}
}
Document
New Directions for Network Verification

Authors: Aurojit Panda, Katerina Argyraki, Mooly Sagiv, Michael Schapira, and Scott Shenker

Published in: LIPIcs, Volume 32, 1st Summit on Advances in Programming Languages (SNAPL 2015)


Abstract
Network verification has recently gained popularity in the programming languages and verification community. Much of the recent work in this area has focused on verifying the behavior of simple networks, whose actions are dictated by static, immutable rules configured ahead of time. However, in reality, modern networks contain a variety of middleboxes, whose behavior is affected both by their configuration and by mutable state updated in response to packets received by them. In this position paper we critically review recent progress on network verification, propose some next steps towards a more complete form of network verification, dispel some myths about networks, provide a more formal description of our approach, and end with a discussion of the formal questions posed to this community by the network verification agenda.

Cite as

Aurojit Panda, Katerina Argyraki, Mooly Sagiv, Michael Schapira, and Scott Shenker. New Directions for Network Verification. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 209-220, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{panda_et_al:LIPIcs.SNAPL.2015.209,
  author =	{Panda, Aurojit and Argyraki, Katerina and Sagiv, Mooly and Schapira, Michael and Shenker, Scott},
  title =	{{New Directions for Network Verification}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{209--220},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-80-4},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{32},
  editor =	{Ball, Thomas and Bodík, Rastislav and Krishnamurthi, Shriram and Lerner, Benjamin S. and Morriset, Greg},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2015.209},
  URN =		{urn:nbn:de:0030-drops-50278},
  doi =		{10.4230/LIPIcs.SNAPL.2015.209},
  annote =	{Keywords: Middleboxes, Network Verification, Mutable Dataplane}
}
  • Refine by Author
  • 2 Sagiv, Mooly
  • 1 Argyraki, Katerina
  • 1 Panda, Aurojit
  • 1 Schapira, Michael
  • 1 Shenker, Scott

  • Refine by Classification

  • Refine by Keyword
  • 1 Deductive reasoning
  • 1 Distributed protocols
  • 1 Middleboxes
  • 1 Mutable Dataplane
  • 1 Network Verification
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2015
  • 1 2016

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