[ Software Research Lunch ]

The Stanford Software Research Lunch is a weekly event on Thursday 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: Spring 2017, Winter 2017, Fall 2016.

Upcoming quarters: Winter 2018.

1/11: Organizational Lunch

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

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

Food: Stefan

1/18: Bonsai: Synthesis-Based Reasoning for Type Systems

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

Speaker: Kartik Chandra

Abstract: We describe algorithms for symbolic reasoning about executable models of type systems, supporting three queries intended for designers of type systems. First, we check for type soundness bugs and synthesize a counterexample program if such a bug is found. Second, we compare two versions of a type system, synthesizing a program accepted by one but rejected by the other. Third, we minimize the size of synthesized counterexample programs.
These algorithms symbolically evaluate typecheckers and interpreters, producing formulas that characterize the set of programs that fail or succeed in the typechecker and the interpreter. However, symbolically evaluating interpreters poses efficiency challenges, which are caused by having to merge execution paths of the various possible input programs. Our main contribution is the Bonsai tree, a novel symbolic representation of programs and program states which addresses these challenges. Bonsai trees encode complex syntactic information in terms of logical constraints, enabling more efficient merging.
We implement these algorithms in the BONSAI tool, an assistant for type system designers. We perform case studies on how BONSAI helps test and explore a variety of type systems. BONSAI efficiently synthesizes counterexamples for soundness bugs that have been inaccessible to automatic tools, and is the first automated tool to find a counterexample for the recently discovered Scala soundness bug SI-9633.

Food: Todd

1/25: Improving Stochastic Search for Program Optimization

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

Speaker: Stefan Heule

Abstract: Writing optimizing compilers remains challenging as modern CPU architectures are incredibly complex and make it difficult to statically determine the performance of a program. Recently stochastic superoptimization has been proposed to randomly search the space of programs, guided by a cost function that estimates the performance of a proposed program during the search. Previous work on superoptimization has used a instruction latency based cost function, which fails to capture many important performance nuances. Instead, we propose a new cost function that runs the program on a test input several times, measuring its actual execution time. We address several technical challenges implementing this apparently simply idea. We find that the new cost function outperforms the latency based estimate on all metrics, sometimes by a wide margin. Perhaps surprisingly, we also show that for some benchmarks, the poorer latency estimate is still able to find programs almost as fast as the ones found by our more sophisticated cost function.

Food: Ben

2/15: TBD (Todd Warszawski)

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

Speaker: Todd Warszawski

3/1: TBD (Berkeley Churchill)

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

Speaker: Berkeley Churchill

Food: Andres

3/8: TBD (Ben Parks)

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

Speaker: Ben Parks

Food: Makai

3/15: TBD (Andres Nötzli)

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

Speaker: Andres Nötzli