Time: Fridays, noon - 1:05pm (PT)
Location: The Internet / The LSD Lab (Engineering 2, Room 398)
Organizers: Sabrina Reis, Achilles Benetopoulos, and Lindsey Kuper
The Languages, Systems, and Data Seminar meets weekly to discuss interesting topics in the areas of programming languages, systems, databases, formal methods, security, software engineering, verification, architecture, and beyond. Our goal is to encourage interactions and discussions between students, researchers, and faculty with interests in these areas. The seminar is open to everyone interested. Participating UCSC students should register for the 2-credit course CSE 280O (let the organizers know if you’re an undergrad and need a permission code).
For fall 2026, we will continue to host the LSD Seminar in a hybrid fashion. Anyone can attend on Zoom, and local folks can gather in person in the lab. Speakers can join either in person or on Zoom, whichever is convenient.
Talks will be advertised on the ucsc-lsd-seminar-announce (for anyone) and lsd-group (for UCSC-affiliated people) mailing lists.
| Date | Speaker | Title |
|---|---|---|
| September 25 | Tim Goodwin | SOSP Practice Talk and New Student Welcome |
| October 2 | Yan Tong | Ironwright: A Rusty Bridge from Bounded Model Checking to Full Verification |
| October 9 | Gavin Gray | A Design Space Exploration of Async/Await |
| October 16 | Ashley Samuelson | Choreographic Programming: Abstractions for Concurrent Dynamism and Modularity |
| October 23 | TBD | TBD |
| October 30 | Clara “Clarise” Ceerla | Mocha: A Motion-Based Choreographic Language |
| November 6 | Esteban Ramos | TBD |
| November 13 | Ashton Wiersdorf | TBD |
| November 20 | Keith Allen | ChorMPI: Choreographies for HPC |
| November 27 | No Speaker | Thanksgiving Holiday |
September 25
The first half hour will consist of a practice talk for SOSP given by Tim Goodwin. The second half hour will be a social with a focus on welcoming new students to the LSD lab.
Speaker: Tim Goodwin
Title: Testing Custom Control Planes Without The Cluster
Abstract: Modern cloud infrastructure is increasingly managed by software. On platforms like Kubernetes, the control plane maintains desired system state through controllers: software components that continuously monitor cluster resources and reconcile them toward a declared specification. This pattern has proven effective, and a thriving ecosystem of projects now compose controllers into custom control planes (CCPs) to automate tasks such as managing application delivery, scaling infrastructure dynamically, and composing cloud provider APIs into higher-level abstractions. The correctness of a CCP, however, depends on how its constituent controllers interact at run time. Bugs arise from implicit assumptions about these interactions that do not hold under all possible executions. As such, finding them requires enumerating the space of possible executions and searching it systematically, which is infeasible in a live cluster environment. In this talk, I will present Kamera, a system for testing CCPs that uses partial simulation to execute the code of multiple interacting controllers against a lightweight model of the Kubernetes runtime. Thus far, Kamera has found 31 new bugs in five popular CCP projects and achieves a 1,781× speedup over existing cluster-based controller testing approaches.
Bio: Tim is a fifth-year PhD student at UC Santa Cruz co-advised by Andi Quinn and Lindsey Kuper.
October 2
Speaker: Yan Tong
Title: Ironwright: A Rusty Bridge from Bounded Model Checking to Full Verification (HATRA Talk)
Abstract: Despite decades of progress on tools for formal verification of distributed systems, it is still hard for verification engineers to close the gap from bounded model checking to full verification. Verification tools that do bridge that gap stop short of producing practically deployable code. We propose Ironwright, a verification framework that addresses these gaps through a unified Rust-based workflow. Developers model and implement distributed systems in a Rust-based shallowly embedded DSL, validate them via automated bounded model checking for rapid iteration, and then “intract” formal specifications from Rust to the Lean proof assistant for rigorous verification. The framework will let developers obtain both verified correctness guarantees and deployable code from the same program.
Bio: Yan is a fourth-year PhD student advised by Prof. Lindsey Kuper. His research focuses on distributed systems verification.
October 9
Speaker: Gavin Gray
Title: A Design Space Exploration of Async/Await
Abstract: Many modern programming languages include some form of asynchronous programming. In particular, a growing number now have what we call straight-line asynchrony: attempts to provide asynchronous functions that look similar to synchronous functions, thereby enabling asynchrony without introducing complex control. These languages often share construct names like async and await, which suggests that they have deep semantic similarities. Yet, a close examination reveals that these languages are quite different along several dimensions, often subtly. These differences have real semantic consequences: similar-looking programs can exhibit divergent behavior, confusing developers and language designers alike.
In this talk I will present our design space exploration of straight-line asynchrony with async/await. We will dissect several existing languages and show how no two of them agree as a whole on design decisions that affect the presence and ordering of effects. I will articulate a design space with nine dimensions covering the full lifecycle of an asynchronous computation, covering questions such as: What precise guarantees does a language give upon calling an asynchronous function? What happens at the end of a task’s life? How can a task handle be cancelled? We will explore these questions through concrete examples, informal design discussion, and a formal semantics.
Bio: Gavin Gray is a PhD student at Brown University advised by Will Crichton and Shriram Krishnamurthi. Gavin works on material to improve the experience of learning and using advanced languages. He currently is focusing on constructs for advanced control flow such as coroutines, effects, continuations, and async/await. Gavin works at the intersection of HCI, applied cognitive science, and programming languages, doing what he refers to as: the human factors of PL design.
October 16
Speaker: Ashley Samuelson
Title: Choreographic Programming: Abstractions for Concurrent Dynamism and Modularity
Abstract: Choreographic programming is an emerging paradigm for writing concurrent programs where developers write a single centralized program that compiles to an individual program for each node. Choreographies provide a high-level abstraction for modeling concurrent systems that both yields intuitive interfaces for programmers and enables correct-by-construction guarantees. However, there are still gaps between the features of existing choreographic languages and the features which are needed and expected by modern systems and their programmers. In this talk, I will present my prior and ongoing work to identify areas in which these disparities arise and address these gaps by designing new choreographic languages and type systems.
Note: This job talk is geared towards a general computer science audience and does not require deep knowledge of programming language theory or concurrency to comprehend. Undergraduates are encouraged to attend!
Bio: Ashley is a Ph.D. candidate in Computer Science at UW—Madison, where she is advised by Ethan Cecchetti, and also frequently collaborates with Andrew K. Hirsch at the University at Buffalo, SUNY. Her research is in the area of programming language and type system design, specifically focusing on choreographic programming, a programming paradigm for deadlock-free message-passing concurrency.
October 23
Speaker: TBD
Title: TBD
Bio: TBD
October 30
Speaker: Clara “Clarise” Ceerla
Title: Mocha: A Motion-Based Choreographic Language
Bio: TBD
November 6
Speaker: Esteban Ramos
Title: TBD
Bio: TBD
November 13
Speaker: Ashton Wiersdorf
Title: TBD
November 20
Speaker: Keith Allen
Title: ChorMPI: Choreographies for HPC
Bio: TBD
November 27
Speaker: No Speaker
No seminar due to Thanksgiving holiday.