Andreas Lööw’s web page

I am a postdoctoral researcher at Imperial College London, in Philippa Gardner's group, working in the intersection of verification and testing, in particular on the analysis platform Gillian. Previously, I was a PhD student at Chalmers University of Technology, adviced by Magnus Myreen, working on interactive theorem proving and hardware verification.


“A Visual Formalisation of Verilog” (draft, tool website) in submission, by Andreas Lööw

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, 1 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


Office: Room 433, Huxley Building, South Kensington Campus

Other places: GitHub and LinkedIn