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 | TBD |
| 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: TBD
October 9
Speaker: TBD
Title: TBD
Bio: TBD
October 16
Speaker: Ashley Samuelson
Title: TBD
Bio: TBD
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.