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.
Publications:
“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
Mail: a.loow@imperial.ac.uk
Office: Room 433, Huxley Building, South Kensington Campus