Andreas Lööw’s web page

I am a postdoctoral researcher at Imperial College London, in Philippa Gardner's group, working on 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 small, but important, concurrency problem in Verilog’s semantics? (Work in progress)” (draft) 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