Elizabeth Polgreen
Associate Professor
School of Informatics
University of Edinburgh
elizabeth.polgreen[at]ed.ac.uk
About
I am a Reader (~Associate Professor in US terminology) in the School of Informatics at the University of Edinburgh. I am interested in (formal and machine learning-based) synthesis techniques and the use of synthesis to increase the scalability of verification. I hold a research fellowship from the Royal Academy of Engineering.
Previously, I was a postdoctoral research scholar in Professor Sanjit Seshia's group at the University of California, Berkeley. I completed my PhD at the University of Oxford, supervised by Professor Alessandro Abate.
My CV is available here. A short bio for talk introductions is available here.
News
July 2026
- I will be giving a keynote talk at SEFM 2026 in November.
- Zoey Shepherd will be talking at the SYNT workshop about Normalised Synthesis of Computations and our tool NSynC.
- I was delighted to give the keynote talk at the Manchester conference for the Institute for Research in Schools.
- Our paper "Massively Parallel Mining of Specifications for Hardware Designs", led by Leiqi Ye and Guy Frankel, is accepted to appear at CAV 2026.
- Our paper "Tensor Program Superoptimization through Cost-Guided Symbolic Program Synthesis", led by Alexander Brauckmann, is accepted to appear at CGO 2026.
- Our paper "Accelerating Sparse Algebra with Program Synthesis", by José Wesley de Souza Magalhães, is accepted to appear at CC 2026.
- I have been promoted to Reader (~Associate Professor in US terminology).
- We have two papers accepted to appear at FMCAD 2025: "PolyVer: a Compositional Approach for PolyGlot System Modelling and Verification" (preprint here ), led by Pei-Wei Chen and in collaboration with Professor Sanjit Seshia; and "Unlocking Hardware Verification with Oracle Guided Synthesis", led by Leiqi Ye.
- Our paper "Guess, Measure & Edit: Using Lowering to Lift Tensor Code" is accepted to appear at PACT 2025
- I am part of a team of researchers that have been awarded a $5 million grant from DARPA as part of the TRACTOR program, Translating All C To Rust. This is in collaboration with Somesh Jha and Tej Chajed at The University of Wisconsin-Madison, Sanjit Seshia and Alvin Cheung at UC Berkeley and Varun Chandrasekaran at the University of Illinois Urbana-Champaign.
- Our paper, "HyGenar: An LLM-Driven Hybrid Genetic Algorithm for Few-Shot Grammar Generation" is accepted to appear in ACL findings 2025. Preprint here.
- Our paper, "Guided Tensor Lifting", is accepted at PLDI 2025. Preprint here. Yixuan Li will present this at PLDI in June 2025.
- Our paper, "Metric-Guided Synthesis of Class Activation Mapping", is accepted at The 3rd World Conference on eXplainable Artificial Intelligence. Preprint here. Alejandro will present this at XAI in July 2025.
- Tensorize received a distinguished paper award from CGO. You can find the paper here, and the code here.
- Our paper, "Online Prompt Selection for Program Synthesis", is accepted at AAAI 2025. Preprint here. Yixuan Li will present this at AAAI in February 2025.
- Our paper, "Tensorize: Fast Synthesis of Tensor Programs from Legacy Code using Symbolic Tracing, Sketching and Solving", led by Alex Brauckmann, is accepted at CGO 2025.
- Our paper on Synthetic Programming Elicitation and Repair for Text-to-Code in Very Low Resource Programming Languages is accepted at Neurips 2024
- The paper that goes along with our tutorial on The Pyramid of (Formal) Software Verification is in the FM proceedings here.
- Slides from my keynote at SYNT 2024 are here.
- A pre-print of our work on Synthetic Programming Elicitation and Repair for Text-to-Code in Very Low Resource Programming Languages is available here.
- I presented our work using program synthesis for program lifting at the VeTSS annual meeting.
- My TedX Talk on Sherlock Holmes and the Case of the Untrustworthy Software is online.
Talks
Some of the talks I have given are available on YouTube:- Sherlock Holmes and the Case of the Untrustworthy Software - TedXUniversityOfEdinburgh video
- Introduction to SAT and SMT - SPLV 2022: Part 1 video, Part 2 video
- Satisfiability and Synthesis Modulo Oracles - VMCAI 2022: video
- Should We Wake the Developer Up? Using Model Checking to Triage the Severity of Security Vulnerabilities in the Xen Hypervisor - FMCAD 2020: video
Group
- Dr Owain Parry, Postdoc (2026-present)
- Guy Frankel, PhD (2024-present, co-supervisor Professor Mike O'Boyle)
- Leiqi Ye, PhD (2024-present, co-supervisor Dr Jianyi Cheng)
- Anton Lydike, PhD (2024-present, main supervisor Dr Jackson Woodruff)
- Heba Al Kayad, PhD (2024-present, main supervisor Dr Craig Innes)
- Zoey Shepherd, PhD (2025-present, co-supervisor Dr Ohad Kammar)
- John Sykes, PhD (September 2026-present, co-supervisor Professor Mike O'Boyle)
Former Group Members
- Dr Yixuan Li, PhD (2021-2025)
- Dr Alexander Brauckmann, PhD (2021-2025)
- Dr José Wesley de Souza Magalhães, PhD (2021-2026)
- Dr Julian Parsert, Postdoc (2021-2022)