SERG Seminar

For this week’s SERG seminar, Finn Hackett, who is visiting our group, will be presenting his PhD work on linking formal models of concurrent and distributed systems with implementations.

Title: Linking System Models with Implementations at Compile and Runtime

Abstract: Reasoning about concurrent and distributed systems is hard. Tests are flaky, interleaving of operations is non-obvious, and failures may only occur under heavy load. Abstractly modeling a system’s intended behavior can help cut through the implementation’s incidental complexity and uncover key design flaws, but it does not answer whether an implementation actually conforms to its abstract design. This talk explores our work on addressing this gap for the TLA+ ecosystem. We go from specification to code via compilation, and code to specification by optimizing linearizability checking for TLA+. We join compile and runtime to enable push-button runtime validation via compiler instrumentation, and use our techniques to evaluate the validity of LLM-generated TLA+ models.

Bio: Finn is a PhD student in the Systopia and Software Practices labs at the University of British Columbia. His interests relate to programming language design, implementation, and formally modeling systems. He usually targets domains that are challenging to program, like concurrent and distributed systems, compilers, interpreters.

If you are interested to give a talk or host a discussion session in one of our next meetings, please contact Carolin Brandt via Mattermost or email.