Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Tue 19 Jan 2021 18:15 - 18:30 at VMCAI - Case Studies Chair(s): Roderick Bloem

We study the problem of using probabilistic network models to formally analyze their quantitative properties, such as the effect of different load-balancing strategies on the long-term traffic on a server farm. Compared to prior work, we explore a different design space in terms of tradeoffs between model expressiveness and analysis scalability, which we realize in a language we call Netter. Netter code is compiled to probabilistic automata, undergoing optimization passes to reduce the state space of the generated models, thus helping verification scale. We evaluate Netter on several case studies, including a probabilistic load balancer, a routing scheme reminiscent of MPLS, and a network defense mechanism against link-flooding attacks. Our results show that Netter can analyze quantitative properties of interesting routing schemes that prior work hadn’t addressed, for networks of small size (4–9 nodes and a few different types of flows). Moreover, when specialized to simpler, stateless networks, Netter can parallel the performance of previous state- of-the-art tools, scaling up to millions of nodes.

Tue 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:00 - 18:30: Case StudiesVMCAI at VMCAI
Chair(s): Roderick BloemInstitute of Software Technology, Graz University of Technology
18:00 - 18:15
Formal Semantics and Verification of Network Based Biocomputation Circuits
Michelle Aluf-MedinaBar Ilan University, Till KortenTU Dresden, Avraham RavivBar Ilan University, Dan Nicolau Jr.Molecular Sense, Hillel KuglerBar Ilan University
Media Attached
18:15 - 18:30
Netter: Probabilistic, Stateful Network Models
Han ZhangCarnegie Mellon University, Chi Zhang, Arthur Azevedo de AmorimCarnegie Mellon University, USA, Yuvraj AgarwalCarnegie Mellon University, Matt FredriksonCarnegie Mellon University, Limin JiaCarnegie Mellon University
Media Attached