SAS 2023
Sun 22 - Tue 24 October 2023 Cascais, Portugal
co-located with SPLASH 2023
Tue 24 Oct 2023 11:00 - 12:00 at Room I - Session 10 Chair(s): Jerome Feret

In traditional program verification, the goal is to automati- cally prove whether a program meets a given property. However, in some cases one might need to prove that a (potentially infinite) set of programs meets a given property. For example, to establish that no program in a set of possible programs (i.e., a search space) is a valid solution to a synthesis problem specification, e.g., a property φ, one needs to verify that all programs in the search space are incorrect, e.g., satisfy the property ¬φ. The need to verify multiple programs at once also arises in other domains such as reasoning about partially specified code (e.g., in the presence of library functions) and self-modifying code. This paper discusses our recent work in designing systems for verifying properties of infinitely many programs at once

Loris D’Antoni is an Associate Professor in the Department of Computer Sciences at the University of Wisconsin-Madison. His research is centered around building fundamental verification and synthesis techniques that help programmers write software that meets their intent. He has won the Phillip R. Certain-Gary D. Sandefur Letters & Science Distinguished Faculty Award, an NSF CAREER Award, the Microsoft Research Faculty Fellowship, Google and Facebook Faculty Awards, and the Morris and Dorothy Rubinoff Dissertation Award. Loris received his Bachelor and master’s in computer science from the University of Torino in 2008 and 2010, respectively, and his PhD in Computer Science from the University of Pennsylvania in 2015.

Tue 24 Oct

Displayed time zone: Lisbon change

11:00 - 12:30
Session 10SAS 2023 at Room I
Chair(s): Jerome Feret INRIA Paris
Verifying Infinitely Many Programs at OnceKeynote
SAS 2023
I: Loris D'Antoni University of Wisconsin-Madison
Mutual Refinements of Context-Free Language Reachability
SAS 2023
Shuo Ding Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology