Program for the winter quarter of 2020.
1/9: Organizational Lunch
Time: Thursday, January 9, 2020, 12 noon - 1pm
Location: Gates 415
Organizational lunch. Come sign up to give a talk during the quarter.
Food: Andres
1/16: Learning to learn to learn by gradient descent by gradient descent by gradient descent
Time: Thursday, January 16, 2020, 12 noon - 1pm
Location: Gates 415
Speaker: Kartik Chandra
Abstract: Working with any gradient-based machine learning algorithm involves the tedious task of tuning the optimizer's hyperparameters, such as the learning rate. There exist many techniques for automated hyperparameter optimization, but they typically introduce even more hyperparameters to control the hyperparameter optimization process. We propose to instead learn the hyperparameters themselves by gradient descent, and furthermore to learn the hyper-hyperparameters by gradient descent as well, and so on ad infinitum. As these towers of gradient-based optimizers grow, they become significantly less sensitive to the choice of top-level hyperparameters, hence decreasing the burden on the user to search for optimal values.
Food: TBD
1/23: TBD
Time: Thursday, January 23, 2020, 12 noon - 1pm
Location: Gates 415
Speaker: TBD
Abstract: TBD
Food: TBD
1/30: Programming Cryptographic Proof Systems for Mutating Large Storage
Time: Thursday, January 30, 2020, 12 noon - 1pm
Location: Gates 415
Speaker: Alex Ozdemir
Abstract: Recently there has been a lot of progress in the area of cryptographic proof systems. These systems have three important properties:
* They are _probabilistic arguments_: sound only probabilistically against computationally-bounded provers. * They are succinct & efficient: proof sizes and verification times are sub-linear in the statement size. * They are general: applicable to any NP language.
This talk will serve as a high-level introduction to these systems, with a particular emphasis on programming them: the means by which their genericity is achieved. It will focus in particular on how to program the mutation of large, public storage, as described in this paper: https://eprint.iacr.org/2019/1494
Food: Sergio
2/6: A Decision Procedure for String to Code Point Conversion
Time: Thursday, February 6, 2020, 12 noon - 1pm
Location: Gates 415
Speaker: Andres Noetzli
Abstract: Strings are sequences of code points, which can be interpreted as integers. We present a decision procedure for a (concatention-free) fragment of strings that includes length and a conversion function from strings to integer code points. Furthermore, we show that many common string operations, such as conversions between lowercase and uppercase, can be naturally encoded using this conversion function. We implement our approach in CVC4, a state-of-the-art string solver and show that the use of a native procedure for code points significantly improves its performance with respect to state-of-the-art string solvers.
Food: Yoni
2/13: Partial Order Reduction for Deep Bug Finding in Synchronous Hardware
Time: Thursday, February 13, 2020, 12 noon - 1pm
Location: Gates 415
Speaker: Makai Mann
Abstract: Symbolic model checking has become an important part of the verification flow in industrial hardware design. However, its use is still limited due to scaling issues. One way to address this is to exploit the large amounts of symmetry present in many real world designs. In this paper, we adapt partial order reduction for bounded model checking of synchronous hardware and introduce a novel technique that improves the efficacy of partial order reduction in this new domain. These approaches are largely automatic, requiring only minimal manual effort. We evaluate our technique on open-source and commercial packet mover circuits---designs containing FIFOs and arbiters.
Food: TBD
2/20: Politeness for The Theory of Algebraic Datatypes
Time: Thursday, February 20, 2020, 12 noon - 1pm
Location: Gates 415
Speaker: Ying Sheng
Abstract: Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable version, the SMT-LIB standard defines a theory of algebraic datatypes, which is currently supported by several mainstream SMT solvers. In this paper, we study this particular theory of datatypes and prove that it is strongly polite, showing also how it can be combined with other arbitrary disjoint theories using polite combination. Our results cover both inductive and finite datatypes, as well as their union. The combination method uses a new, simple, and natural notion of additivity, that enables deducing strong politeness from (weak) politeness.
Food: TBD
2/27: First Order Separation and its Application to Invariant Inference
Time: Thursday, February 27, 2020, 12 noon - 1pm
Location: Gates 415
Speaker: Jason Koenig
Abstract: Quantified first-order formulas, often with quantifier alternations, are increasingly used in the verification of complex systems. While automated theorem provers for first-order logic are becoming more robust, invariant inference tools that handle quantifiers are currently restricted to purely universal formulas. We define and analyze first-order quantified separators and their application to inferring invariants with quantifier alternations. A separator for a given set of positively and negatively labeled models is a formula that satisfies positive models and does not satisfy negative models. We investigate the problem of finding a separator from the class of formulas in prenex normal form with a bounded number of quantifiers and show this problem is NP-complete by reduction from SAT. We also give a practical separation algorithm via reduction to SAT, which we use to demonstrate the first invariant inference procedure able to infer invariants with quantifier alternations.
Food: Scott
3/5: Getafix - Learning to Fix Bugs Automatically
Time: Thursday, March 5, 2020, 12 noon - 1pm
Location: Gates 415
Speaker: Johannes Bader
Abstract: Developers spend a significant amount of their time fixing bugs. Fixes often are repetitive, so it appears that some portion of this work should be automated. Indeed, some recent approaches offer automation, but these typically explore a large space of potential fixes by making varying combinations of mutations, trying them all until one that passes the test suite. This is not only computationally expensive, but the suggested may not look natural to a developer. We present Getafix, a tool that offers readable bug fixes without requiring massive computational resources. Getafix learns from your bug fix history. It extracts past code changes that fixed bugs and learns, in an off-line phase, a set of templates from those fixes. As new bug reports appear, Getafix uses these templates to create and rank a set of suggestions in mere seconds, as well as offer fixes that resemble human-made fixes. At Facebook, Getafix has been used to auto-fix bugs reported by static analysis tools like Infer.
Food: TBD
3/12: TBD
Time: Thursday, March 12, 2020, 12 noon - 1pm
Location: Gates 415
Speaker: TBD
Abstract: TBD
Food: TBD