| 2024 | ECOOP | Compositional Symbolic Execution for Correctness and Incorrectness Reasoning. | Andreas Lw, Daniele Nantes-Sobrinho, Sacha-lie Ayoun, Caroline Cronjger, Petar Maksimovic, Philippa Gardner |
| 2024 | ECOOP | Matching Plans for Frame Inference in Compositional Reasoning. | Andreas Lw, Daniele Nantes-Sobrinho, Sacha-lie Ayoun, Petar Maksimovic, Philippa Gardner |
| 2023 | ECOOP | Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding. | Petar Maksimovic, Caroline Cronjger, Andreas Lw, Julian Sutherland, Philippa Gardner |
| 2023 | FMCAD | Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor. | Ning Dong, Roberto Guanciale, Mads Dam, Andreas Lw |
| 2022 | FMCAD | Reconciling Verified-Circuit Development and Verilog Development. | Andreas Lw |
| 2022 | MEMOCODE | A small, but important, concurrency problem in Verilog's semantics? (Work in progress). | Andreas Lw |
| 2021 | CPP | Lutsig: a verified Verilog compiler for verified circuit development. | Andreas Lw |
| 2019 | ICSE | A proof-producing translator for verilog development in HOL. | Andreas Lw, Magnus O. Myreen |
| 2019 | PLDI | Verified compilation on a verified processor. | Andreas Lw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, Anthony C. J. Fox |