Time: Fridays, noon - 1:05pm (PT)
Location: The Internet / The LSD Lab (Engineering 2, Room 398)
Organizers: Achilles Benetopoulos, Lindsey Kuper, Kyle Miller, Sabrina Reis
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 | No Speaker | Social Hour and New Graduate Student Introductions |
| October 2 | Yan Tong | Ironwright: A Rusty Bridge from Bounded Model Checking to Full Verification |
| October 9 | TBD | TBD |
| 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
Speaker: No Speaker
Social hour in place of talk. We especially encourage new graduate students to attend.
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.