Elizabeth Polgreen

News

• 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" with Oracle Guided Synthesis", led by Leiqi Ye (preprint to follow).
• 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.

• Our work on Guiding Enumerative Program Synthesis with Large Language Models is accepted at CAV 2024. Yixuan Li is also presenting this work at the EuroProofNet workshop. Pre-print, workshop.
• The proceedings for AAAI 2024 are now out. Our paper is here.

• Our work on Reinforcement Learning and Data-Generation for Syntax-Guided Synthesis, led by Julian Parsert, is accepted at AAAI 2024. Pre-print.
• I have a PhD studentship available. More details here.

• Our work lifting C to TACO received the Best Paper Award at GPCE

• I am giving a talk at TedXUniversityofEdinburgh on the 21st October. The theme is "The Great Unknown".
• I have received a research fellowship from the Royal Academy of Engineering which begins on the 31st October
• José Wesley De Souza Magalhães will present our work on automatically lifting tensor code to TACO at GPCE 2023
• Federico Mora will present our work on verifying distributed systems with message chains at OOPSLA 2023
• Alexander Brauckman will present our work on Automatic, Retargetable Program Raising in Multi-Level IR using Program Synthesis at PACT 2023

• Shaokai Lin presented our Verifiable CPS using Lingua Franca at EMSOFT 2023

• Yixuan Li will talk about our work using genetic algorithms to find good grammars for synthesis at SYNT 2023
• Julian Parsert will present our work using reinforcement learning in Syntax Guided Synthesis at SYNT 2023

• I have received an Amazon Research Award to fund my work on automatically modernizing code.

Talks

• 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

Students

• Yixuan Li, Phd (2021-present , co-supervisor Professor Mike O'Boyle)
• Alexander Brauckmann, Phd (2021-present , main supervisor Professor Mike O'Boyle)
• José Wesley de Souza Magalhães, Phd (2021-present , main supervisor Professor Mike O'Boyle)
• 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)