I am a postdoctoral researcher at Imperial College London, in Philippa Gardner's group. I am currently working on the analysis platform Gillian, specifically, the formal foundations of Gillian and similar platforms/tools. This work builds on and extends ideas from symbolic execution, separation logic, and incorrectness logic. Previously, I was a PhD student at Chalmers University of Technology, adviced by Magnus Myreen, working on interactive theorem proving and hardware verification.
Publications:
“Betterlog: a clean-slate, backwards-compatible alternative simulation semantics for Verilog; or: Verilog without the quirks” (work in progress – looking for collaborators so drop an e-mail if this project sounds interesting to you)
“The Simulation Semantics of Synthesisable Verilog” (extended version, visualisation tool) at OOPSLA'25, by Andreas Lööw
“Compositional Symbolic Execution for Correctness and Incorrectness Reasoning” (distinguished paper, extended version) at ECOOP'24, by Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Petar Maksimović, and Philippa Gardner
“Matching Plans for Frame Inference in Compositional Reasoning” at ECOOP'24, by Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Petar Maksimović, and Philippa Gardner
“Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor” at FMCAD'23, by Ning Dong, Roberto Guanciale, Mads Dam, and Andreas Lööw
“Exact Separation Logic” (extended version) at ECOOP'23, by Petar Maksimović, Caroline Cronjäger, Andreas Lööw, Julian Sutherland, and Philippa Gardner
“A small, but important, concurrency problem in Verilog’s semantics?” (local copy) at MEMOCODE'22, by Andreas Lööw
“Reconciling Verified-Circuit Development and Verilog Development” (local copy) at FMCAD'22, by Andreas Lööw
“Lutsig: A Verified Verilog Compiler for Verified Circuit Development” (local copy, video) at CPP'21, by Andreas Lööw
“Verified Compilation on a Verified Processor” (local copy, one-minute video abstract) at PLDI'19, by Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, and Anthony Fox
“A Proof-Producing Translator for Verilog Development in HOL” (local copy) at FormaliSE'19, by Andreas Lööw and Magnus O. Myreen
Other (e.g., workshop papers):
“Unified Compositional Formal Methods: Exact Separation Logic and the Gillian Platform for Correctness and Incorrectness Reasoning” (local copy of abstract for talk) at Incorrectness'24, by Andreas Lööw, Daniele Nantes Sobrinho, Sacha-Élie Ayoun, Nat Karmios, Seung Hoon Park, Petar Maksimović, and Philippa Gardner
“They're the same picture: a software-verification flow adapted for hardware verification” (local copy of abstract for talk, talk) at PLARCH'23, by Andreas Lööw and Magnus O. Myreen
Mail: a.loow@imperial.ac.uk
Office: Room 433, Huxley Building, South Kensington Campus
Other places: Google Scholar, LinkedIn, and GitHub