[ Software Research Lunch ]

The Stanford Software Research Lunch is a weekly event on Friday where students and researchers present their latest work to peers. Talks are open to anybody, but regular attendees are expected to give a presentation on their work.

Mailing list: software-research-lunch@lists.stanford.edu (subscribe via mailman)

Calendar: ical | Add to Google Calendar

Format: The lunch is held every week during fall, winter and spring quarter. The first week of every quarter is an organizational lunch where people can sign up to give a talk. If you'd like to give a talk, contact Stefan Heule.

Past quarters: Winter 2017, Fall 2016.

4/7: Organizational Lunch

Time: Friday, April 7, 2017, 12 noon - 1pm
Location: Gates 463a

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

Food: Stefan

4/14: Developing Bug-Free Machine Learning Systems With Formal Mathematics

Time: Friday, April 14, 2017, 12 noon - 1pm
Location: Gates 463a

Speaker: Daniel Selsam

Abstract: Noisy data, non-convex objectives, model misspecification, and numerical instability can all cause undesired behaviors in machine learning systems. As a result, detecting actual implementation errors can be extremely difficult. We demonstrate a methodology based on an interactive proof assistant, in which one writes an implementation of a machine learning system along with a formal theorem stating that the implementation is correct. The process of proving this theorem interactively in the proof assistant exposes all implementation errors since any error in the program would cause the proof to fail. As a case study, we implement a new system, Certigrad, for optimizing over stochastic computation graphs and generate a machine-checkable proof that the gradients sampled by the system are unbiased estimates of the true mathematical gradients. We train a variational autoencoder using Certigrad and find that it is nearly as efficient as TensorFlow.

Food: Wonyeol

4/21: Cracking Multi-Language Transformations

Time: Friday, April 21, 2017, 12 noon - 1pm
Location: Gates 463a

Speaker: James Koppel

Abstract: Programming languages have many similarities, and so, when writing a source-to-source transformation on one language, it would be nice to reuse code from a similar transformation for a different language. This is a fundamentally difficult problem, and previous attempts have either resorted to reimplementing the same transformation for many languages, or at best reducing multiple languages to a common intermediate representations, which necessarily destroys information and produces poor source-to-source results.
We present a new representation for programs called *incremental parametric syntax*, and show how it enables us to construct source-to-source transformations so that we can implement them once, and run them on each of C, Java, JavaScript, Lua, and Python. Instead of constructing a common representation for the languages, incremental parametric syntax allows us to instead construct a family of representations sharing common components, each specialized to a single-language, and to semi-automatically generate them from existing syntax definitions. Our evaluation shows that (1) once a transformation is written, relatively little work is required to configure it for a new language (2) transformations built this way output readable code which preserve the structure of the original, according to participants in our human study, and (3) despite dealing with many languages, our transformations can still handle language corner-cases, and pass 90% of compiler test suites.

Food: Andres

4/28: SpaceSearch: A Library for Building and Verifying Solver-Aided Tools

Time: Friday, April 28, 2017, 12 noon - 1pm
Location: Gates 463a

Speaker: Stefan Heule

Abstract: Many verification tools build on automated solvers. These tools reduce problems in a specific application domain (e.g., compiler optimization validation) to queries that can be discharged with a highly optimized solver. But the correctness of the reductions themselves is rarely verified in practice, limiting the confidence that the solver's output establishes the desired domain-level property.
This paper presents SpaceSearch, a new library for developing solver-aided tools within a proof assistant. A user builds their solver-aided tool in Coq against the SpaceSearch interface, and the user then verifies that the results provided by the interface are sufficient to establish the tool's desired high-level properties. Once verified, the tool can be extracted to an implementation in a solver-aided language (e.g., Rosette), where SpaceSearch provides an efficient instantiation of the SpaceSearch interface with calls to an underlying SMT solver. This combines the strong correctness guarantees of developing a tool in a proof assistant with the high performance of modern SMT solvers. This paper also introduces new optimizations for such verified solver-aided tools, including parallelization and incrementalization.
We evaluate SpaceSearch by building and verifying two solver-aided tools. The first, SaltShaker, checks that RockSalt's x86 semantics for a given instruction agrees with STOKE's x86 semantics. SaltShaker identified 7 bugs in RockSalt and 1 bug in STOKE. After these systems were patched by their developers, SaltShaker verified the semantics' agreement on 15,255 instruction instantiations in under 2h. The second tool, BGProof, is a verified version of an existing Border Gateway Protocol (BGP) router configuration checker. Like the existing checker, BGProof scales to checking industrial configurations spanning over 240 KLOC, identifying 19 configuration inconsistencies with no false positives. However, the correctness of BGProof has been formally proven, and we found 2 bugs in the unverified implementation. These results demonstrate that SpaceSearch is a practical approach to developing efficient, verified solver-aided tools.

Food: Todd

5/12: TBD (Manolis Papadakis)

Time: Friday, May 12, 2017, 12 noon - 1pm
Location: Gates 463a

Speaker: Manolis Papadakis

Food: Pratiksha

5/19: TBD (Manu Sridharan)

Time: Friday, May 19, 2017, 12 noon - 1pm
Location: Gates 463a

Speaker: Manu Sridharan

Food: Lázaro

5/26: TBD (Osbert Bastani)

Time: Friday, May 26, 2017, 12 noon - 1pm
Location: Gates 463a

Speaker: Osbert Bastani

Food: Cristian

6/2: TBD (Eric Schkufza)

Time: Friday, June 2, 2017, 12 noon - 1pm
Location: Gates 463a

Speaker: Eric Schkufza

Food: Manolis

6/9: TBD (Karthik Murthy)

Time: Friday, June 9, 2017, 12 noon - 1pm
Location: Gates 463a

Speaker: Karthik Murthy

Food: Guy