Nate Foster, Cornell University
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.