Program

9:00 - 9:20 - Opening Remarks

Sharon Shoham and Yakir Vizel

9:20 - 10:00 - Rajeev Alur: Safety verification of closed-loop systems with neural-network controllers

Abstract: TBD

10:00 - 10:30 - Break

10:30 - 11:10 - Moshe Vardi: The Rise and Fall of Linear Temporal Logic

Abstract: One of the surprising developments in the area of program verification in the late part of the 20th Century is the emergence of Linear Temporal Logic (LTL), a logic that emerged in philisophical studies of free will, as the cannonical language for describing temporal behavior of computer systems. LTL, however, is not expressive enough for industrial applications. The first decade of the 21 Century saw the emergence of industrial temporal logics such as ForSpec, PSL, and SVA. These logics, however, are not clean enough to serve as objects of theoretical study. This talk will describe the rise and fall of LTL, and will propose a new cannonical temporal logic: Linear Dynamic Logic (LDL).

[slides]

11:10 - 11:50 - Daniel Kroening: Verification and Test for Deep Neural Networks

Abstract: A lot of code is now "AI-enabled", which means that there is a trained component. Deep Neural Networks are a popular choice in many applications of this kind, but meaningful testing and verification of DNNs is hard. I will briefly highlight the challenges, and will then give a taster of three results: 1) a method for explaining what a DNN does, 2) a method that establishes a proof of robustness of a DNN, and 3) a method that attacks a DNN using inputs that humans consider "normal".

11:50 - 12:30 - Kenneth L. McMillan: A Look Back at Compositional Verification

Abstract: The idea of compositionality as a way to control the complexity of program proofs or derivations dates to the earliest days of formal methods. Since Orna has made a number of important contributions to compositional methods in model checking, I will take this opportunity to look back at the evolution of compositional methods over four decades, as we moved toward more automated verification techniques. I will try to explain what is difficult about compositional proofs in comparison to global proofs (especially in automating them) and make a few suggestions of possible future directions.

12:30 - 14:30 - Lunch Break

14:30 - 15:10 - Aarti Gupta: Abstractions due to Symmetry in Network Control Planes

Abstract: We develop an algorithm for compressing large networks into smaller ones with similar control plane behavior: For every stable routing solution in the large, original network, there exists a corresponding solution in the abstract compressed network, and vice versa. Our compression algorithm preserves a wide variety of properties in the abstract network including reachability, loop freedom, and path length. Consequently, operators may speed up network analysis, based on simulation, emulation, or verification, by analyzing only the abstract compressed network.

This joint work (with Ryan Beckett, Ratul Mahajan, and Dave Walker) was inspired directly by Orna Grumberg’s pioneering work on model checking and abstraction.

15:10 - 15:50 - Arie Gurfinkel: Quantified Solutions for Model Checking with Constrained Horn Clauses

Abstract: Software Model Checking is a difficult problem. The problem undecidable even for transition systems (i.e., function-free programs) over Linear Integer Arithmetic (LIA). Extending the transition system with theory of Arrays, further complicates the problem by requiring inference and reasoning with universally quantified formulas. In this talk, I will describe our work on an algorithm, called Quic3, that extends IC3 to infer universally quantified invariants over the combined theory of LIA and Arrays. Unlike other approaches that use either IC3 or an SMT solver as a black box, Quic3 carefully manages quantified generalization (to construct quantified invariants) and quantifier instantiation (to detect convergence in the presence of quantifiers). While Quic3 is not guaranteed to converge, it is guaranteed to make progress by exploring longer and longer executions.

15:50 - 16:00 - Orna Grumberg: Closing Remarks

22:00 - ... - Orna's Traditional Dance Party @ CAV