[ 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 Scott Viteri.

Past quarters: Fall 2020, Spring 2020, Winter 2020, Fall 2019, Spring 2019, Winter 2019, Fall 2018, Spring 2018, Winter 2018, Fall 2017, Spring 2017, Winter 2017, Fall 2016.

Ordering Food: For suggestions for those ordering food for the lunch, see here.

1/14: Resource-Aware Session Types for Digital Contracts

Time: Tuesday, January 14, 2020, 12 noon - 1pm
Location: Zoom

Speaker: Ankush Das

Abstract: While there exist several successful techniques for supporting programmers in deriving static resource bounds for sequential code, analyzing the resource usage of message-passing concurrent processes poses additional challenges. To meet these challenges, this talk presents an analysis for statically deriving worst-case bounds on the computational complexity of message-passing processes, respectively. The analysis is based on novel resource-aware session types that describe resource contracts by allowing both messages and processes to carry potential and amortize cost. The talk then applies session types to implement digital contracts. Digital contracts are protocols that describe and enforce execution of a contract, often among mutually distrusting parties. Programming digital contracts comes with its unique challenges, which include describing and enforcing protocols of interaction, analyzing resource usage and tracking linear assets. The talk presents the type-theoretic foundations of Nomos, a programming language for digital contracts whose type system addresses the aforementioned domain-specific requirements. To express and enforce protocols, Nomos is based on shared binary session types rooted in linear logic. To control resource usage, Nomos uses resource-aware session types and automatic amortized resource analysis, a type-based technique for inferring resource bounds. To track assets, Nomos employs a linear type system that prevents assets from being duplicated or discarded. The talk concludes with future work directions on designing an efficient implementation for Nomos and making it robust to attacks from malicious entities.

Food: Doordash,

2/4: AutoMap

Time: Tuesday, February 4, 2020, 12 noon - 1pm
Location: Zoom

Speaker: Rohan Yadav

Abstract: Mapping is the process of selecting a processor for each computation, or task, and memories for the data collections that those tasks access. On parallel, heterogeneous, and distributed computing platforms, finding a mapping that yields high performance for a given application is challenging. We show that fast mappings are sensitive to the machine, application, and even input used. Porting to a new machine, modifying the application, or running on a substantially different input may all necessitate re-tuning the application mapping to maintain the best possible performance.
We present AutoMap, a system which, given an application and an input, automatically tunes the mapping to the hardware used. AutoMap searches over the space of possible mappings dynamically, using a search algorithm and judicious pruning methods. We demonstrate that AutoMap finds fast mappings in minutes to a few hours, whereas handwritten mappings often require days of experimentation.
We also describe em constrained coordinate-wise descent (CCD), a search algorithm that explicitly balances the trade-off between running computations as quickly as possible and minimizing data movement. CCD discovers mappings that are as fast as, or up to 20% faster than, hand-tuned mappings, even on the hardware for which the hand-tuned mapping was designed. We find greater speedups (up to 40%) when re-tuning an existing mapping for different hardware or inputs.

Food: Doordash,

2/11: Programming Systems for Bug-Free and Robust Probabilistic Software

Time: Tuesday, February 11, 2020, 12 noon - 1pm
Location: Zoom

Speaker: Sasa Misailovic

Abstract: Probabilistic programming languages offer an intuitive way to model uncertainty by representing complex probability models as simple probabilistic programs. Thus, even a programmer with limited exposure to statistical machine learning can benefit from powerful probabilistic inference. A programmer only needs to write a high-level model in a programming language with support for random sampling and conditioning on data. The underlying probabilistic programming systems (which execute the high-level probabilistic programs) hide the complexity of inference algorithms from the program developer. Understanding how to test and debug probabilistic software will have a key role in improving programmer productivity in this emerging domain.
In this talk, I will present our work on testing and analyzing probabilistic programming systems and discuss some common classes of real-world problems that impact the accuracy and correctness in probabilistic programming. Our systems helped discover over 50 bugs in the popular probabilistic programming systems Pyro, Edward, and Stan, as well as their underlying infrastructures PyTorch and TensorFlow.

2/18: Pono Model Checker

Time: Tuesday, February 18, 2020, 12 noon - 1pm
Location: Zoom

Speaker: Makai Mann

Abstract: Symbolic model checking is an important tool for finding bugs (or proving the absence of bugs) in modern system designs. Because of this, improving the ease of use, scalability, and performance of model checking tools and algorithms continues to be an important research direction. In service of this goal, we present Pono, an open-source SMT-based model checker. Pono is designed to be both a research platform for developing and improving model checking algorithms, as well as a performance-competitive tool that can be used for academic and industry verification applications. In addition to performance, Pono prioritizes transparency (developed as an open-source project on GitHub), flexibility (Pono can be adapted to a variety of tasks by exploiting its general SMT-based interface), and extensibility (it is easy to add new algorithms and new back-end solvers).


2/25: Reifying Concurrent Programs

Time: Tuesday, February 25, 2020, 12 noon - 1pm
Location: Zoom

Speaker: Shaz Qadeer

Abstract: Program reification is a new approach to the construction of verified concurrent programs and their proofs. This approach simplifies and scales (human and automated) reasoning by enabling a concurrent program to be represented and manipulated at multiple layers of abstraction. These abstraction layers are chained together via simple program transformations; each transformation is justified by a collection of automatically checked verification conditions. Program reification makes proofs maintainable and reusable, specifically eliminating the need to write complex invariants on the low-level encoding of the concurrent program as a flat transition system.
I will present Civl, a reifier for concurrent programs. Civl has been used to construct verified low-level implementations of complex systems such as a concurrent garbage collector, consensus protocol, and shared-memory data structures. Civl is publicly available: https://civl-verifier.github.io/.
This work has been done jointly with Bernhard Kragl (IST Austria).