SafeDNN: Understanding and Verifying Neural Networks
by Corina Pasareanu, NASA
Date: July 20
Abstract:
The SafeDNN project at NASA Ames explores analysis techniques and tools to ensure that systems that use Deep Neural Networks (DNN) are safe, robust and interpretable. Research directions we are pursuing include: symbolic execution for DNN analysis, label-guided clustering to automatically identify input regions that are robust, parallel and compositional approaches to improve formal SMT-based verification, property inference and automated program repair for DNNs, adversarial training and detection, probabilistic reasoning for DNNs. In this talk I will highlight some of the research advances from SafeDNN, with focus on DNN repair.
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.
Programmable Program Synthesis
by Loris D’Antoni, University of Wisconsin-Madison
Date: July 22
Abstract:
Program synthesis is now a reality and we are approaching the point where domain-specific synthesizers can now handle problems of practical sizes. Moreover, some of these tools are finding adoption in industry. However, for synthesis to become a mainstream technique adopted at large by programmers as well as by end-users, we need to design programmable synthesis frameworks that (i) are not tailored to specific domains or languages, (ii) enable one to specify synthesis problems with a variety of qualitative and quantitative objectives in mind, and (iii) come equipped with theoretical as well as practical guarantees. We report on our work on designing such frameworks and on building synthesis engines that can handle program-synthesis problems describable in such frameworks, and describe open challenges and opportunities.
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.
Balancing Automation And Control For Formal Verification Of Microprocessors
by Anna Slobodova, Centaur Technology, Inc.
Date: July 23
Abstract:
Formal methods are becoming an indispensable part of the design process in software and hardware industry. It takes robust tools and proofs to make formal validation of large scale projects reliable. In this talk, we will describe the current status of formal verification at Centaur Technology. We will explain our challenges and our methodology–how various proofs and verification artifacts are interconnected and how we keep them consistent over the duration of a project. We also describe our main engine–a powerful symbolic simulator with rewriting capabilities, that is integrated in a theorem prover and proven correct.
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.