A proof-producing translator for verilog development in HOL. - Andreas Lööw; Magnus O. Myreen (FormaliSE@ICSE, 2019)

Verified compilation on a verified processor. - Andreas Lööw; Ramana Kumar; Yong Kiam Tan; Magnus O. Myreen; Michael Norrish; Oskar Abrahamsson; Anthony C. J. Fox (PLDI, 2019)

Lutsig: a verified Verilog compiler for verified circuit development. - Andreas Lööw (CPP, 2021)

Reconciling Verified-Circuit Development and Verilog Development. - Andreas Lööw (FMCAD, 2022)

A small, but important, concurrency problem in Verilog's semantics? (Work in progress). - Andreas Lööw (MEMOCODE, 2022)

Exact Separation Logic. - Petar Maksimovic 001; Caroline Cronjäger; Julian Sutherland; Andreas Lööw; Sacha-Élie Ayoun; Philippa Gardner (CoRR, 2022)

Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding. - Petar Maksimovic 001; Caroline Cronjäger; Andreas Lööw; Julian Sutherland; Philippa Gardner (ECOOP, 2023)

Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor. - Ning Dong; Roberto Guanciale; Mads Dam; Andreas Lööw (FMCAD, 2023)

Compositional Symbolic Execution for Correctness and Incorrectness Reasoning. - Andreas Lööw; Daniele Nantes-Sobrinho; Sacha-Élie Ayoun; Caroline Cronjäger; Petar Maksimovic 001; Philippa Gardner (ECOOP, 2024)

Matching Plans for Frame Inference in Compositional Reasoning. - Andreas Lööw; Daniele Nantes-Sobrinho; Sacha-Élie Ayoun; Petar Maksimovic 001; Philippa Gardner (ECOOP, 2024)

Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Extended Version). - Andreas Lööw; Daniele Nantes-Sobrinho; Sacha-Élie Ayoun; Caroline Cronjäger; Petar Maksimovic 001; Philippa Gardner (CoRR, 2024)

Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Artifact). - Andreas Lööw; Daniele Nantes-Sobrinho; Sacha-Élie Ayoun; Caroline Cronjäger; Nat Karmios; Petar Maksimovic 001; Philippa Gardner (Dagstuhl Artifacts Ser., 2024)

The Simulation Semantics of Synthesisable Verilog. - Andreas Lööw (Proc. ACM Program. Lang., 2025)