Time: Fridays, noon - 1:05pm (PT)
Location: The Internet / The LSD Lab (Engineering 2, Room 398)
Organizers: Lindsey Kuper, Tyler Sorensen, Reese Levine, and Achilles Benetopoulos
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 winter 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 |
|---|---|---|
| Jan. 9 | Shanto Rahman | Reliable Software Testing Using LLM and Program Analysis |
| Jan. 16 | Lef Ioannidis | Structural temporal logic for mechanized program verification |
| Jan. 23 | George Pîrlea | Veil: Automated and Interactive Verification of Transition Systems |
| Jan. 30 | Stephen Mell | Designing Programming Languages for Compound AI Systems |
| Feb. 6 | Martin Kleppmann | Collaborative editors are distributed databases |
| Feb. 13 | Alexandre Moine | All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs |
| Feb. 20 | TBD | TBD |
| Feb. 27 | Shardul Chiplunkar | TBD |
| March 6 | Justine Frank | TBD |
| March 13 | Shraddha Barke | TBD |
Jan. 9
Speaker: Shanto Rahman
Title: Reliable Software Testing Using LLM and Program Analysis
Abstract: Software testing is essential for software reliability, yet modern test suites frequently suffer from broken tests caused by nondeterminism or code evolution. These failures mislead developers, reduce trust in testing, and allow real bugs to escape into production. In this talk, I present my work on making software testing reliable using program analysis and large language models. I introduce techniques to automatically identify and explain the root causes of flaky tests using context-aware attribution, enabling developers to understand why nondeterministic failures occur. I then present automated repair techniques, including FlakeSync for repairing asynchronous flaky tests and UTFix for repairing unit tests broken by code changes. These techniques achieve high repair success with low overhead and have been evaluated on large-scale, real-world datasets. I conclude by outlining a vision for nondeterminism-aware reliability in emerging domains such as cloud services, ML systems, and quantum software.
Bio: Shanto Rahman is a Ph.D. candidate in Electrical and Computer Engineering at The University of Texas at Austin, advised by Professor August Shi. Her research spans software engineering and AI, focusing on reliable software testing under nondeterminism and code evolution. She develops program-analysis- and LLM-based techniques to detect, explain, reproduce, and repair broken tests, with publications in ICSE, OOPSLA, ASE, and ICST. She has gained industry experience through internships at Google and Amazon Web Services (AWS). Her recognitions include MIT EECS Rising Stars, UC Berkeley NextProf Nexus, and multiple UT Austin fellowships and awards.
Jan. 16
Speaker: Lef Ioannidis
Title: Structural temporal logic for mechanized program verification
Abstract: Mechanized verification of liveness properties for infinite programs with effects and nondeterminism is challenging. Existing temporal reasoning frameworks operate at the level of models such as traces and automata. Reasoning happens at a very low-level, requiring complex nested (co-)inductive proof techniques and familiarity with proof assistant mechanics (e.g., the guardedness checker). Further, reasoning at the level of models instead of program constructs creates a verification gap that loses the benefits of modularity and composition enjoyed by structural program logics such as Hoare Logic. To address this verification gap, and the lack of compositional proof techniques for temporal specifications, we propose Ticl, a new structural temporal logic. Using ticl, we encode complex (co-)inductive proof techniques as structural lemmas and focus our reasoning on variants and invariants. We show that it is possible to perform compositional proofs of general temporal properties in a proof assistant, while working at a high level of abstraction. We demonstrate the benefits of Ticl by giving mechanized proofs of safety and liveness properties for programs with scheduling, concurrent shared memory, and distributed consensus, demonstrating a low proof-to-code ratio.
Bio: I work in Programming Languages (PL) and Verification (Proof Assistants) in Microsoft Research’s RiSE group. I completed my PhD in the University of Pennsylvania advised by Sebastian Angel and Steve Zdancewic, where I developed Domain-Specific Programming Languages (DSLs) to improve the reliability, security and privacy of computer systems, combining techniques from formal verification and cryptographic protocols. Before starting my PhD I worked in industry as a Software Engineer (Bridgewater Associates, Apple) and Tech Lead at UnifyID. I completed by Bachelor’s and Masters in MIT and my thesis advisors were Frans Kaashoek and Nickolai Zeldovich. I am from Thessaloniki, Greece and started my academic career at the Aristotle University of Thessaloniki (AUTH).
Jan. 23
Speaker: George Pîrlea
Title: Veil: Automated and Interactive Verification of Transition Systems
Abstract: Veil is a foundational verification framework embedded in the Lean 4 proof assistant that makes distributed protocol verification both powerful and accessible. Improving on tools such as TLA+ and Ivy, Veil provides a unified environment where testing and automated push-button verification coexist with the full power of a modern proof assistant, all while maintaining foundational soundness guarantees.
Unlike traditional verifiers, which are implemented as standalone tools and (optionally) use proof assistants as backend certificate checkers, Veil is a Lean library, with all its functionality entirely embedded in the proof assistant. We believe this approach has significant advantages over traditional verifiers and that, in the near future, more verifiers will be built in this way.
In this talk, we describe our vision for building verifiers in Lean, and share our experience of writing (and rewriting) Veil, and the lessons we have learned along the way. We will also give a small tutorial of Veil, which you can try online at https://try.veil.dev/
Bio: George Pîrlea is a final year PhD student at the School of Computing, National University of Singapore, where he works on formal verification and testing of distributed systems. His research focuses on making formal methods practical and accessible, with a particular emphasis on combining automated and interactive approaches to verification. George is the lead developer of Veil.
Jan. 30
Speaker: Stephen Mell
Title: Designing Programming Languages for Compound AI Systems
Abstract: AI systems, such as LLMs, have proven successful at a wide range of tasks, from natural language processing to code generation. Recently, there has been a trend toward building compound AI systems, which combine one or more neural models with more traditional software components, such as search procedures and software APIs. Thus, an important question is how such systems should be built, and in particular how the programming languages used can be enhanced to support them. This talk addresses two facets of this question.
First, compound AI systems are glue scripts, in the sense that their performance bottleneck is waiting for external AI models to return, rather than in the developer-written code, rendering traditional performance optimizations ineffective. To address this, we propose a novel opportunistic evaluation strategy for scripting languages based on a core lambda calculus, which automatically dispatches independent external calls in parallel and streams their results. We prove that this is sound, and we show that it yields large speedups (running time up to 6.2× and latency up to 12.7×) on five compound AI systems.
Second, LLM agents take actions by invoking tools; in many cases, this is done via code actions, where the agent generates code, typically in Python, which is then executed. Though LLMs are quite proficient at Python, it may not be the optimal language for actions. Instead we propose Quasar, a language offering automated parallelization to improve performance, uncertainty quantification to improve reliability and mitigate hallucinations, and security features enabling the user to validate actions. LLMs writes code in a subset of Python, which is then transpiled to Quasar before execution.
Bio: Stephen is a final-year PhD student at the University of Pennsylvania, advised by Osbert Bastani and Steve Zdancewic, and is an incoming postdoc at CMU, advised by Zhihao Jia. He is interested in building better programming abstractions both for compound AI systems in particular and high-level scripting more generally.
Feb. 6
Speaker: Martin Kleppmann
Title: Collaborative editors are distributed databases
Abstract: Collaborative editors for text, (e.g. Google Docs, Overleaf), spreadsheets (e.g. Excel in Microsoft 365), graphics (e.g. Figma), and other file types have become an essential part of how we work. However, their current architecture relies on centralised, trusted cloud services. This is risky for various reasons: What if the government forces the cloud provider to disclose your sensitive documents, or to stop serving you entirely? What if the provider is a startup that gets acquired and shut down?
In this talk I will provide an overview of our research around Automerge, a library for building decentralised, local-first collaboration software. It brings together ideas from CRDTs, distributed databases, column-oriented data formats, version control systems, and end-to-end encrypted messaging apps in order to enable collaboration without depending on any one trusted company.
Bio: Martin Kleppmann is an Associate Professor at the University of Cambridge, working on decentralised systems and cryptographic protocols. He works with the Ink & Switch research lab on local-first collaboration software, and advises the decentralised social network Bluesky. In a previous life he was a Silicon Valley software engineer and entrepreneur, cofounding and selling two startups and working on large-scale data infrastructure at LinkedIn. He is the author of the best-selling O’Reilly book Designing Data-Intensive Applications.
Feb. 13
Speaker: Alexandre Moine
Title: All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs
Abstract: Nondeterminism makes parallel programs challenging to write and reason about. To avoid these challenges, researchers have developed techniques for internally deterministic parallel programming, in which the steps of a parallel computation proceed in a deterministic way. Internal determinism is useful because it lets a programmer reason about a program as if it executed in a sequential order. However, no verification framework exists to exploit this property and simplify formal reasoning.
To capture the essence of why internally deterministic programs should be easier to reason about, we define a property called schedule-independent safety. A program satisfies schedule-independent safety, if, to show that the program is safe across all interleavings, it suffices to show that one terminating execution of the program is safe. We then present Musketeer, a separation logic for proving that a program satisfies schedule-independent safety. Once schedule independence is guaranteed, correctness can be shown in Angelic, a companion logic in which the user may select interactively one sequential interleaving and reason about it alone.
Using Musketeer, we prove the soundness of MiniDet, an affine type system for enforcing internal determinism. All results are mechanized in Rocq on top of the Iris separation logic framework.
This work was presented at POPL’26 and received a distinguished paper award.
Bio: Alexandre is a postdoctoral associate at New York University working with Joe Tassarotti on formal verification of parallel programs. Before that, he was a PhD student at Inria Paris (France) working with Arthur Charguéraud and François Pottier on formal verification of heap space bounds. Most of his work has a link to separation logic, resource consumption or parallelism.
Feb. 20
Speaker: TBD
Title: TBD
Abstract: TBD
Feb. 27
Speaker: Shardul Chiplunkar
Title: TBD
Abstract: TBD
March 6
Speaker: Justine Frank
Title: TBD
Abstract: TBD
March 13
Speaker: Shraddha Barke
Title: TBD
Abstract: TBD