ICFP 2021
Sun 22 - Sat 28 August 2021
Tue 24 Aug 2021 16:45 - 17:00 at ICFP Talks - Session 3
Wed 25 Aug 2021 04:45 - 05:00 at ICFP Talks - Session 3

ProbNV is a new framework for probabilistic network control plane verification that strikes a balance between generality and scalability. ProbNV is general enough to encode a wide range of features from the most common protocols (eBGP and OSPF) and yet scalable enough to handle challenging properties, such as probabilistic all-failures analysis of medium-sized networks with 100-200 devices. When there are a small, bounded number of failures, networks with up to 500 devices may be verified in seconds. ProbNV operates by
translating raw CISCO configurations into a probabilistic and functional programming language designed for network verification. This language comes equipped with a novel type system that characterizes the sort of representation to be used for each data structure: \emph{concrete} for the usual representation of values; \emph{symbolic} for a BDD-based representation of sets of values; and \emph{multi-value} for an MTBDD-based representation of values that depend upon symbolics. Careful use of these varying representations speeds execution of symbolic simulation of network models. The MTBDD-based representations are also used to calculate probabilistic properties of network models once symbolic simulation is complete. We implement the language and evaluate its performance on benchmarks constructed from real network topologies and synthesized routing policies.

Tue 24 Aug

Displayed time zone: Seoul change

16:00 - 17:30
16:00
15m
Talk
Modular, Compositional, and Executable Formal Semantics for LLVM IR
Research Papers
Yannick Zakowski Inria, Calvin Beck University of Pennsylvania, Irene Yoon University of Pennsylvania, Ilya Zaichuk Taras Shevchenko National University of Kyiv, Vadim Zaliva University of Cambridge, UK, Steve Zdancewic University of Pennsylvania
DOI Media Attached
16:15
15m
Talk
Higher-Order Probabilistic Adversarial Computations: Categorical Semantics and Program Logics
Research Papers
Alejandro Aguirre Aarhus University, Gilles Barthe MPI-SP; IMDEA Software Institute, Marco Gaboardi Boston University, Deepak Garg MPI-SWS, Shin-ya Katsumata National Institute of Informatics, Tetsuya Sato Tokyo Institute of Technology
DOI Media Attached
16:30
15m
Talk
How to Evaluate Blame for Gradual Types
Research Papers
Lukas Lazarek Northwestern University, Ben Greenman Brown University, Matthias Felleisen Northeastern University, Christos Dimoulas PLT @ Northwestern University
DOI Media Attached
16:45
15m
Talk
ProbNV: Probabilistic Verification of Network Control Planes
Research Papers
Nick Giannarakis University of Wisconsin-Madison, Alexandra Silva University College London, David Walker Princeton University
DOI Media Attached
17:00
15m
Talk
Of JavaScript AOT Compilation Performance
Research Papers
Manuel Serrano Inria, France
DOI Media Attached
17:15
15m
Talk
Symbolic and Automatic Differentiation of Languages
Research Papers
DOI Media Attached

Wed 25 Aug

Displayed time zone: Seoul change

04:00 - 05:30
Session 3Research Papers at ICFP Talks
04:00
15m
Talk
Modular, Compositional, and Executable Formal Semantics for LLVM IR
Research Papers
Yannick Zakowski Inria, Calvin Beck University of Pennsylvania, Irene Yoon University of Pennsylvania, Ilya Zaichuk Taras Shevchenko National University of Kyiv, Vadim Zaliva University of Cambridge, UK, Steve Zdancewic University of Pennsylvania
DOI Media Attached
04:15
15m
Talk
Higher-Order Probabilistic Adversarial Computations: Categorical Semantics and Program Logics
Research Papers
Alejandro Aguirre Aarhus University, Gilles Barthe MPI-SP; IMDEA Software Institute, Marco Gaboardi Boston University, Deepak Garg MPI-SWS, Shin-ya Katsumata National Institute of Informatics, Tetsuya Sato Tokyo Institute of Technology
DOI Media Attached
04:30
15m
Talk
How to Evaluate Blame for Gradual Types
Research Papers
Lukas Lazarek Northwestern University, Ben Greenman Brown University, Matthias Felleisen Northeastern University, Christos Dimoulas PLT @ Northwestern University
DOI Media Attached
04:45
15m
Talk
ProbNV: Probabilistic Verification of Network Control Planes
Research Papers
Nick Giannarakis University of Wisconsin-Madison, Alexandra Silva University College London, David Walker Princeton University
DOI Media Attached
05:00
15m
Talk
Of JavaScript AOT Compilation Performance
Research Papers
Manuel Serrano Inria, France
DOI Media Attached
05:15
15m
Talk
Symbolic and Automatic Differentiation of Languages
Research Papers
DOI Media Attached