by Loris D’Antoni, University of Wisconsin-Madison
Abstract: I will present a new framework for program synthesis, called semantics-guided synthesis (SemGuS), that allows a user to provide both the syntax and the semantics for the constructs in the language. SemGuS accepts a recursively defined big-step semantics, which allows it, for example, to be used to specify and solve synthesis problems over an imperative programming language that may contain loops with unbounded behavior. The customizable nature of SemGuS also allows synthesis problems to be defined over a non-standard semantics, such as an abstract semantics. In addition to the SemGuS framework, I will present algorithms for solving SemGuS problems that is capable of both synthesizing programs and proving unrealizability, by encoding a SemGuS problem as a proof search over Constrained Horn Clauses: in particular, this approach is the first that we are aware of that can prove unrealizabilty for synthesis problems that involve imperative programs with unbounded loops, over an infinite syntactic search space.
Bio: Loris D’Antoni is an Assistant Professor in the Department of Computer Sciences at the University of Wisconsin-Madison. There, he’s affiliated with the madPL (Madison Programming Languages) Group. His research is centered on building fundamental verification and synthesis techniques that help programmers write software that meets their intent. In particular, he’s currently focused on building practical and predictable program synthesis techniques that can be applied to computer networks, program repair, and machine learning. He has won an NSF CAREER Award, the Microsoft Research Faculty Fellowship, Google and Facebook Faculty Awards, and the Morris and Dorothy Rubinoff Dissertation Award. His papers were selected for special journal issues (TOPLAS, FMSD) and nominated for best paper awards (TACAS, ESOP). Loris received his Bachelor and Masters 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.
by Corina Pasareanu, NASA
Bio: Corina Pasareanu is an ACM Distinguished Scientist, working at NASA Ames. She is affiliated with KBR and Carnegie Mellon University’s CyLab. Her research interests include model checking, symbolic execution, compositional verification, probabilistic software analysis, autonomy, and security. She is the recipient of several awards, including ASE Most Influential Paper Award (2018), ESEC/FSE Test of Time Award (2018), ISSTA Retrospective Impact Paper Award (2018), ACM Impact Paper Award (2010), and ICSE 2010 Most Influential Paper Award (2010). She has been serving as Program/General Chair for several conferences including: FM’21, ICST 2020, ISSTA 2020, ESEC/FSE 2018, CAV 2015, ISSTA 2014, ASE 2011, and NFM 2009. She is currently an associate editor for the IEEE TSE journal.
by Anna Slobodova, Centaur Technology, Inc.
Bio: Anna Slobodova is a senior principal engineer and the Technical Lead of the Formal Verification group at Centaur Technology, Inc. Centaur’s focus is on designing high-performance low-cost x86 microprocessors. Dr. Slobodova is interested in technology that can improve validation of complex industrial design (from hands-on theorem proving to automated procedures). She obtained a Masters degree and a PhD in Theoretical Computer Science (with a focus on Complexity Theory) at Comenius University, Bratislava, Slovakia. She started her career as a Research Scientist at Comenius University. She later moved to became an Assistant Professor at the University of Trier, Germany, and she was also appointed in the Fraunhofer Institute for Telematik. In 1998, she joined Digital Equipment Corporation (later Compaq) in Massachussetts, USA. Her design team was purchased by Intel, where she spent several years in the formal verification group known as “Dragon Team”. In 2008, Dr. Slobodova joined Centaur Technology, where she assumed responsibility for Centaur’s formal verification of two then PhD students that had been started by a University of Texas professor. Additional professional staff has been added, and the FV team’s work is now an indispensable part of the company’s design and validation process. Dr. Slobodova has served on multiple program committees focused on formal methods including CAV, CPP, DATE and FMCAD. For FMCAD 2009, she served as the organizational co-chair, and as the conference general co-chair in 2011. She serves on the FMCAD Steering Committee presently. She was a Test and Verification track co-chair of ICCD 2011, and FV topic co-chair for DATE 2020 and 2021.