Program for the fall quarter of 2019.

9/26: Organizational Lunch

Time: Thursday, September 26, 2019, 12 noon - 1pm
Location: Gates 415

Organizational lunch. Come sign up to give a talk during the quarter.

Food: Andres

10/3: Verification of Recurrent Neural Networks

Time: Thursday, October 3, 2019, 12 noon - 1pm
Location: Gates 415

Speaker: Yuval Jacoby

Abstract: Deep Neural Networks (DNNs) are revolutionizing the software development world. However, we still can't predict when and why a DNN might fail. Applying formal verification to DNNs is a novel approach that can give us the confidence of using DNNs in critical tasks. Verification of DNNs is an active field, but most work to date has focused on feed-forward DNNs, while ignoring recurrent neural networks (RNNs), which are widely used for many tasks. We will present a new novel approach that is based on invariants.

Food: TBD

10/10: FUDGE: Fuzz Driver Generation at Scale

Time: Thursday, October 10, 2019, 12 noon - 1pm
Location: Gates 415

Speaker: Tim King

Abstract: At Google we have found tens of thousands of security and robustness bugs by fuzzing C and C++ libraries. To fuzz a library, a fuzzer requires a fuzz driver—which exercises some library code—to which it can pass inputs. Unfortunately, writing fuzz drivers remains a primarily manual exercise, a major hindrance to the widespread adoption of fuzzing. In this paper, we address this major hindrance by introducing the Fudge system for automated fuzz driver generation. Fudge automatically generates fuzz driver candidates for libraries based on existing client code. We have used Fudge to generate thousands of new drivers for a wide variety of libraries. Each generated driver includes a synthesized C/C++ program and a corresponding build script, and is automatically analyzed for quality. Developers have integrated over 200 of these generated drivers into continuous fuzzing services and have committed to address reported security bugs. Further, several of these fuzz drivers have been upstreamed to open source projects and integrated into the OSS-Fuzz fuzzing infrastructure. Running these fuzz drivers has resulted in over 150 bug fixes, including the elimination of numerous exploitable security vulnerabilities.
The talk is based on work published at FSE 2019 (Best Paper Award).

Food: Sergio

10/17: Toward Fully-Automated Digital Design

Time: Thursday, October 17, 2019, 12 noon - 1pm
Location: Gates 415

Speaker: Alex Feldman

Abstract: Circuit design is in the heart of modern computing. Algorithms based on satisfiability have application in functional circuit design, layout, technology mapping, and various optimization techniques. Many problems in digital design, though, belong to higher classes in the computational hierarchy. Encoding those as satisfiability problems is often cumbersome.
In this talk we will discuss a class of algorithms that solve problems from digital design by constructing and solving Quantified Boolean Formulas. These encodings are intuitive and can help the designer invent novel circuits. The algorithms we discuss are generic and have use both in design and optimization.
The designs computed by our algorithms are compositions of function types specified in component libraries. Our algorithms reduce the design problem to quantified satisfiability and use advanced solvers to find solutions that represent useful systems.
The algorithms we present in this talk are sound and complete and are guaranteed to discover correct designs of optimal size, if they exist. We apply our method to the design of digital circuits and discover new and more optimal classical and quantum circuits for common arithmetic functions such as addition and multiplication.
The performance of our algorithms is evaluated through extensive experimentation. We have first created a benchmark consisting of specifications of scalable synthetic digital circuits and real-world microchips. We have then generated multiple circuits functionally equivalent to the ones in the benchmark.
Our approach generalizes circuit optimization. It uses arbitrary component libraries and has applications to areas such as digital circuit design, diagnostics, abductive reasoning, test vector generation, and combinatorial optimization.

Food: TBD

10/24: TASO: Optimizing Deep Learning Computation with Automatic Generation of Graph Substitutions

Time: Thursday, October 24, 2019, 12 noon - 1pm
Location: Gates 415

Speaker: Zhihao Jia

Abstract: Existing deep neural network (DNN) frameworks optimize the computation graph of a DNN by applying graph transformations manually designed by human experts. This approach misses possible graph optimizations and is difficult to scale, as new DNN operators are introduced on a regular basis.
We propose TASO, the first DNN computation graph optimizer that automatically generates graph substitutions. TASO takes as input a list of operator specifications and generates candidate substitutions using the given operators as basic building blocks. All generated substitutions are formally verified against the operator specifications using an automated theorem prover. To optimize a given DNN computation graph, TASO performs a cost-based backtracking search, applying the substitutions to find an optimized graph, which can be directly used by existing DNN frameworks.
Our evaluation on five real-world DNN architectures shows that TASO outperforms existing DNN frameworks by up to 2.8×, while requiring significantly less human effort. For example, TensorFlow currently contains approximately 53,000 lines of manual optimization rules, while the operator specifications needed by TASO are only 1,400 lines of code.

Food: Andres

10/31: Unlocking the Power of Formal Hardware Verification with CoSA and Symbolic QED

Time: Thursday, October 31, 2019, 12 noon - 1pm
Location: Gates 415

Speaker: Florian Lonsing

Abstract: As designs grow in size and complexity, design verification becomes one of the most difficult and costly tasks facing design teams. Formal verification techniques offer great promise because of their ability to exhaustively explore design behaviors. However, formal techniques also have a reputation for being labor-intensive and limited to small blocks. Is there any hope for successful application of formal techniques at design scale? We answer this question affirmatively by digging deeper to understand what the real technological issues and opportunities are. First, we look at satisfiability solvers, the engines underlying formal techniques such as model checking. Given the recent innovations in satisfiability solving, we argue that there are many reasons to be optimistic that formal techniques will scale to designs of practical interest. We use our CoSA model checker as a demonstration platform to illustrate how advances in solvers can improve scalability. However, even if solvers become blazingly fast, applying them well is still labor-intensive. This is because formal tools are only as useful as the properties they are given to prove, which traditionally have required great effort to develop. Symbolic quick error detection (SQED) addresses this issue by using a single, universal property that checks designs automatically. We demonstrate how SQED can automatically find logic bugs in a variety of designs and report on bugs found and efficiency gains realized in academic and industry designs. We also present a generator for an improved SQED module that further reduces the amount of manual effort that has to be spent by the designer.

Food: Andrew

11/7: Resilience à la carte: Application-tailored Resilience in Legion

Time: Thursday, November 7, 2019, 12 noon - 1pm
Location: Gates 415

Speaker: Karthik Murthy

Abstract: Soft failures, e.g., execution failures due to bitflips that are undetectable by error-correcting codes, inevitably occur during long-running applications on extreme-scale parallel systems. Resilience against these failures is necessary. Further, programmers desire the ability to surgically restart specific portions of an application's task graph to overcome such failures. In this talk, we present a resilience framework that addresses these challenges. Our framework allows programmers to specify what should be protected (policy) and our scalable parallel runtime implements this policy automatically (mechanism). We demonstrate the utility of our framework by allowing a suite of Lux applications to successfully complete multi-node multi-GPU executions in the presence of failures with minimal programmer effort.

Food: Oded

11/14: Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions

Time: Thursday, November 14, 2019, 12 noon - 1pm
Location: Gates 415

Speaker: Ahmed Irfan

Abstract: Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a first-order formula with respect to some theory or combination of theories; Verification Modulo Theories (VMT) is the problem of analyzing the reachability for transition systems represented in terms of SMT formulae. In this talk, we will focus on the problems of SMT and VMT over the theories of polynomials over the reals (NRA), over the integers (NIA), and of NRA augmented with transcendental functions (NTA). We propose a New abstraction-refinement approach called Incremental Linearization. The idea is to abstract nonlinear multiplication and transcendental functions as uninterpreted functions in an abstract domain limited to linear arithmetic with uninterpreted functions. The uninterpreted functions are incrementally axiomatized by means of upper- and lower-bounding piecewise-linear constraints. In the case of transcendental functions, particular care is required to ensure the soundness of the abstraction. The method has been implemented in the MathSAT SMT solver, and in the nuXmv VMT model checker. An extensive experimental evaluation on a wide set of benchmarks from verification and mathematics demonstrates the generality and the effectiveness of our approach.

Food: Makai

11/21: Deep Learning for Mathematical Reasoning

Time: Thursday, November 21, 2019, 12 noon - 1pm
Location: Gates 415

Speaker: Markus Rabe

Abstract: I will summarize recent efforts in machine learning for automated reasoning and the work of the N2Formal research group at Google. Our mission is to build an artificial mathematician, one that can understand natural mathematics found in scientific articles and books, and translate it to formal representations. So far, we have built a machine learning environment based on the interactive theorem prover HOL Light and a neural theorem prover called DeepHOL. Given a statement to prove, DeepHOL automatically selects appropriate premises and tactics, just like a human mathematician would. Training DeepHOL using imitation and reinforcement learning already achieves state-of-the-art performance in automated reasoning.

Food: Yoni

12/5: Induction Duality: Invariant Inference as Primal-Dual Search

Time: Thursday, December 5, 2019, 12 noon - 1pm
Location: Gates 415

Speaker: Oded Padon

Abstract: Invariant inference techniques reason simultaneously about states and predicates, and it is well-known that these two kinds of reasoning are in some sense dual to each other. We make this folklore precise, formalizing the first truly primal-dual algorithm for invariant inference. Our primary contributions are the duality formalism itself along with the application to developing the primal-dual inference algorithm, in which we exploit duality to design an anologue of reachability in inductive proofs that is dual to reachability in states. We also provide preliminary experiments showing that even an early prototype is able to successfully handle difficult invariant inference examples from the literature.

Food: Scott