[ Software Research Lunch ]


Program for the fall quarter of 2018.


9/27: Organizational Lunch

Time: Thursday, September 27, 2018, 12 noon - 1pm
Location: Gates 415

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

Food: Todd


10/4: A First Step Towards Understanding Stochastic Synthesis

Time: Thursday, October 4, 2018, 12 noon - 1pm
Location: Gates 415

Speaker: Jason Koenig

Abstract: Abstract: We consider the problem of understanding the behavior of program synthesis from input-output examples via stochastic search. We show the distribution of synthesis times is defined by the log-normal and gamma distributions, show why these distributions arise and give an algorithm that exploits this behavior to speed up synthesis by a factor of up to 27x. Our experimental results are obtained using a new program synthesis benchmark distilled from widely used production code.

Food: Todd


10/11: Optimizing DNN Computation with Automatically Generated Graph Substitutions

Time: Thursday, October 11, 2018, 12 noon - 1pm
Location: Gates 415

Speaker: Zhihao Jia

Abstract: Existing deep learning frameworks generally optimize computation in a DNN model by performing rule-based transformations on its computation graph. This approach depends on human experts to manually design graph transformations and has two limitations. First, existing systems only consider a limited set of commonly used graph transformations and may miss subtle optimizations for particular graphs. Second, this approach can hardly scale when today's DNN models continuously introduce new DNN operators, as optimizing new DNNs requires exploring various combinations of new operators with existing operators.
To address both limitations, I will talk about MetaFlow, an ongoing research project that aims at optimizing DNN computation with automatically generated graph substitutions. I will first show that it is possible to translate an arbitrary graph substitution to a set of SMT (satisfiability modulo theories) problems and uses a SMT solver to verify the correctness of the substitution. I will also present an efficient backtracking search algorithm to explore a large space of potential computation graphs and find optimized candidates. Our initial results show that MetaFlow improves DNN inference and training performance by up to 1.6x and 1.2x respectively over existing deep learning frameworks.

Food: Oded


10/18: Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems

Time: Thursday, October 18, 2018, 12 noon - 1pm
Location: Gates 415

Speaker: Oded Padon

Abstract: Various verification techniques for temporal properties transform temporal verification to safety verification. For infinite-state systems, these transformations are inherently imprecise. That is, for some instances, the temporal property holds, but the resulting safety property does not. This paper introduces a mechanism for tackling this imprecision. This mechanism, which we call *temporal prophecy*, is inspired by prophecy variables. Temporal prophecy refines an infinite-state system using first-order linear temporal logic formulas, via a suitable tableau construction. For a specific liveness-to-safety transformation based on first-order logic, we show that using temporal prophecy strictly increases the precision. Furthermore, temporal prophecy leads to robustness of the proof method, which is manifested by a cut elimination theorem. We integrate our approach into the Ivy deductive verification system, and show that it can handle challenging temporal verification examples.
Practice talk for a paper to be presented in FMCAD 2018. Joint work with: Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelsk, Mooly Sagiv, and Sharon Shoham.

Food: Zhihao


10/25: AI-driven software quality assurance

Time: Thursday, October 25, 2018, 12 noon - 1pm
Location: Gates 415

Speaker: Roni Stern

Abstract: In this talk I will present our recent successful integration of various techniques from the Artificial Intelligence (AI) literature into the software debugging and testing process.
First, we show how data that is already stored by industry standard software engineering tools can be used to learn a fault prediction model able to predict accurate the software components that are likely to contain bugs. This allows focusing testing efforts on such error-prone components.
Then, we show how this learned fault prediction model can be used to augment existing software diagnosis algorithms, providing a better understanding of which software components need to be replaced to correct an observed bug. Moreover, for the case where further tests are needed to identify the faulty software component, we present a test-planning algorithm based on Markov Decision Processes (MDP). Importantly, the presented approach for considering both a fault prediction model, learned from past failures, and a diagnosis algorithm that is model-based, is general, and can be applied to other fields, beyond software troubleshooting. If time permits, I will also show more recent work in which we extended our software diagnosis approach to diagnose system exploits and vulnerabilities.

Food: Jason


11/1: Aroma – Code Recommendation via Structural Code Search

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

Speaker: Frank Luan

Abstract: Programmers often write code that is similar to existing code written somewhere. A tool that could help programmers to search such similar code would be immensely useful. Such a tool could enable programmers to find idiomatic code patterns, cross-check against similar code, and discover extensions to partially written code that would avoid common mistakes and errors. We describe Aroma, a tool and technique for creating code recommendation via structural code search. Aroma indexes a huge code corpus, takes a partial code snippet as input, and returns a set of “code recommendations” – succinct code snippets created from a cluster of similar code fragments containing the query code snippet. This is joint work with Di Yang, Koushik Sen and Satish Chandra carried out at Facebook.

Food: Sierra


11/8: Dynamic Tracing: Memoization of Task Graphs for Dynamic Task-Based Runtimes

Time: Thursday, November 8, 2018, 12 noon - 1pm
Location: Gates 415

Speaker: Wonchan Lee

Abstract: Many recent programming systems for both supercomputing and data center workloads generate task graphs to express computations that run on parallel and distributed machines. Due to the overhead associated with constructing these graphs the dependence analysis that generates them is often statically computed and memoized, and the resulting graph executed repeatedly at runtime. However, many applications require a dynamic dependence analysis due to data dependent behavior, but there are new challenges in capturing and re- executing task graphs at runtime. In this work, we introduce dynamic tracing, a technique to capture a dynamic dependence analysis of a trace that generates a task graph, and replay it. We show that an implementation of dynamic tracing improves strong scaling by an average of 4.9X and up to 7.0X on a suite of already optimized benchmarks.

Food: Karthik


11/15: TBD (Jason Koenig)

Time: Thursday, November 15, 2018, 12 noon - 1pm
Location: Gates 415

Speaker: Jason Koenig

Food: Oded


11/22: Thanksgiving - No Lunch

Time: Thursday, November 22, 2018, 12 noon - 1pm
Location: Gates 415

Speaker: N/A


11/29: TBD

Time: Thursday, November 29, 2018, 12 noon - 1pm
Location: Gates 415

Speaker:


12/6: TBD (Daniel Fremont)

Time: Thursday, December 6, 2018, 12 noon - 1pm
Location: Gates 415

Speaker: Daniel Fremont


12/13: TBD (Karthik Murthy)

Time: Thursday, December 13, 2018, 12 noon - 1pm
Location: Gates 415

Speaker: Karthik Murthy