Formal Verification of P4 Programs
Nate Foster, Cornell University
Abstract: P4 is a domain-specific language for programming and specifying packet-processing systems. It is based on an elegant design with high-level abstractions like parsers and match-action pipelines that can be compiled to efficient implementations in software or hardware. This tutorial will be structured in two parts; (i) an introduction to the P4 language using hands-on programming examples, and (ii) a discussion of how the Petr4 framework [POPL ’21] can be used to develop language-based verification tools for networks.
Bio: Nate Foster is an Associate Professor of Computer Science at Cornell University, a Principal Research Engineer at Barefoot Networks, and Chair of the P4 Language Technical Steering Team. The goal of his research is to develop languages and tools that make it easy for programmers to build secure and reliable systems. His current work focuses on the design and implementation of languages for programming software-defined networks. In the past he has also worked on bidirectional languages (also known as “lenses”), database query languages, data provenance, type systems, mechanized proof, and formal semantics. He received a PhD in Computer Science from the University of Pennsylvania, an MPhil in History and Philosophy of Science from Cambridge University, and a BA in Computer Science from Williams College. His awards include a Sloan Research Fellowship, an NSF CAREER Award, the SIGCOMM Rising Star Award, a Most Influential POPL Paper Award, a Tien ‘72 Teaching Award, several Google Research Awards, a Yahoo! Academic Career Enhancement Award, a Cornell Engineering Resarch Excellence Award, and the Morris and Dorothy Rubinoff Award.
Introduction to Algebraic Program Analysis
Zak Kincaid (Princeton University) and Tom Reps (University of Wisconsin-Madison)
Abstract: Compositional invariant generators operate using a divide-and-conquer strategy: break the program into parts, synthesize invariants for each part, and then combine the results. Compositionality enables invariant generation to scale, to be easily parallelized, to apply to incomplete programs, and to respond quickly to changes to an input program. This tutorial provides an introduction to algebraic program analysis, a framework for compositional invariant generation that builds upon the foundation of abstract algebra and formal language theory. We will show how to design an algebraic program analysis, how to prove that it is correct, and how to implement it. We will show how this framework can be used to solve difficult invariant generation problems (in particular, generation of numerical invariants involving disjunction and non-linear arithmetic), and how it can be applied to recursive programs.
Bios: Zak Kincaid: Zachary Kincaid is an assistant professor in the Department of Computer Science at Princeton University. Kincaid’s research focuses on program analysis and automated theorem proving. He received his Ph.D. in Computer Science from the University of Toronto in 2016, under the supervision of Azadeh Farzan. He received an NSF CAREER award (2020) and an honorable mention for the ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award (2017).
Tom Reps: Thomas Reps is the J. Barkley Rosser Professor & Rajiv and Ritu Batra Chair in the Computer Sciences Department of the University of Wisconsin, which he joined in 1985. He also co-founded GrammaTech, Inc., of which he was President from 1988-2019. Reps is the author or co-author of four books and more than two hundred papers describing his research. His work has concerned a wide variety of topics, including dataflow analysis, abstract interpretation, program slicing, pointer analysis, model checking, computer security, code instrumentation, language-based program-development environments, the use of program profiling in software testing, software renovation, incremental algorithms, and attribute grammars. Professor Reps received his Ph.D. in Computer Science from Cornell University in 1982. His Ph.D. dissertation received the 1983 ACM Doctoral Dissertation Award. Reps has also been the recipient of an NSF Presidential Young Investigator Award (1986), a Packard Fellowship (1988), a Humboldt Research Award (2000), and a Guggenheim Fellowship (2000). He is also an ACM Fellow (2005). In 2013, Reps was elected a foreign member of Academia Europaea. He received the ACM SIGPLAN Programming Languages Achievement Award for 2017. Reps has held visiting positions at the Institut National de Recherche en Informatique et en Automatique (INRIA) in Rocquencourt, France (1982-83), the University of Copenhagen, Denmark (1993-94), the Consiglio Nazionale delle Ricerche in Pisa, Italy (2000-2001), and the Université Paris Diderot-Paris 7 (2007-2008).
Type-Driven Program Synthesis
Nadia Polikarpova, University of California San Diego
Abstract: Program synthesis is a promising approach to automating low-level aspects of programming by generating code from high-level declarative specifications. But what form should these specifications take? In this tutorial we will explore the use of types as the input to program synthesis. Types are widely adopted by programmers, they can vary in expressiveness and capture both functional and non-functional properties, and finally, type checking is often fully automatic and compositional, which helps the synthesizer find the right program. The tutorial is organized in three parts. The first part will focus on Synquid, a synthesizer that generates recursive programs from expressive refinement types. The second part will cover a recent extension to Synquid called ReSyn, which allows you to augment refinement types with potential annotations to specify the desired resource consumption of a program. The third part will introduce our recent work on Hoogle+, which relies on more mainstream Haskell types and generates code snippets by composing functions from Haskell libraries. It is an interactive tutorial, so bring your laptops!
Bio: Nadia Polikarpova is an assistant professor at UC San Diego. She received her Ph.D. in Computer Science from ETH Zurich in 2014, and then spent a couple of years as a postdoctoral researcher at MIT. Nadia’s research interests are in program synthesis, program verification, and type systems. She is a 2020 Sloan Fellow, and a recipient of the 2020 NSF Career Award and the 2020 Intel Rising Stars Award.