| 2026 | VMCAI | Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification. | Andreas Lindner, Karl Palmskog, Scott Constable, Mads Dam, Roberto Guanciale, Hamed Nemati |
| 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 | CoNEXT | HOL4P4: semantics for a verified data plane. | Anoud Alshnakat, Didrik Lundberg, Roberto Guanciale, Mads Dam, Karl Palmskog |
| 2022 | FMCAD | Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution. | Karl Palmskog, Xiaomo Yao, Ning Dong, Roberto Guanciale, Mads Dam |
| 2021 | FMCAD | Refinement-Based Verification of Device-to-Device Information Flow. | Ning Dong, Roberto Guanciale, Mads Dam |
| 2020 | CCS | InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis. | Roberto Guanciale, Musard Balliu, Mads Dam |
| 2020 | SEFM | Hoare-Style Logic for Unstructured Programs. | Didrik Lundberg, Roberto Guanciale, Andreas Lindner, Mads Dam |
| 2017 | CHES | Compositional Verification of Security Properties for Embedded Execution Platforms. | Christoph Baumann, Oliver Schwarz, Mads Dam |
| 2016 | SP | Cache Storage Channels: Alias-Driven Attacks and Verified Countermeasures. | Roberto Guanciale, Hamed Nemati, Christoph Baumann, Mads Dam |
| 2016 | SEFM | Automatic Derivation of Platform Noninterference Properties. | Oliver Schwarz, Mads Dam |
| 2015 | ESORICS | Trustworthy Prevention of Code Injection in Linux on Embedded Devices. | Hind Chfouka, Hamed Nemati, Roberto Guanciale, Mads Dam, Patrik Ekdahl |
| 2015 | SOFSEM | Trustworthy Virtualization of the ARMv7 Memory Subsystem. | Hamed Nemati, Roberto Guanciale, Mads Dam |
| 2014 | CCS | Automating Information Flow Analysis of Low Level Code. | Musard Balliu, Mads Dam, Roberto Guanciale |
| 2014 | PDP | Location Independent Routing in Process Network Overlays. | Mads Dam, Karl Palmskog |
| 2013 | CCS | Formal verification of information flow security for a simple arm-based separation kernel. | Mads Dam, Roberto Guanciale, Narges Khakpour, Hamed Nemati, Oliver Schwarz |
| 2013 | CCS | Machine code verification of a tiny ARM hypervisor. | Mads Dam, Roberto Guanciale, Hamed Nemati |
| 2013 | CPP | Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties. | Narges Khakpour, Oliver Schwarz, Mads Dam |
| 2012 | CCS | TreeDroid: a tree automaton based approach to enforcing data processing policies. | Mads Dam, Gurvan Le Guernic, Andreas Lundblad |
| 2011 | PLDI | Epistemic temporal logic for information flow security. | Musard Balliu, Mads Dam, Gurvan Le Guernic |
| 2010 | PODC | Brief announcement: the accuracy of tree-based counting in dynamic networks. | Supriya Krishnamurthy, John Ardelius, Erik Aurell, Mads Dam, Rolf Stadler, Fetahi Zebenigus Wuhib |
| 2009 | ATVA | A Data Symmetry Reduction Technique for Temporal-epistemic Logic. | Mika Cohen, Mads Dam, Alessio Lomuscio, Hongyang Qu |
| 2009 | ECOOP | Security Monitor Inlining for Multithreaded Java. | Mads Dam, Bart Jacobs, Andreas Lundblad, Frank Piessens |
| 2009 | IJCAI | A Symmetry Reduction Technique for Model Checking Temporal-Epistemic Logic. | Mika Cohen, Mads Dam, Alessio Lomuscio, Hongyang Qu |
| 2009 | IM | Gossiping for threshold detection. | Fetahi Wuhib, Rolf Stadler, Mads Dam |
| 2008 | FM | Provably Correct Runtime Monitoring. | Irem Aktug, Mads Dam, Dilian Gurov |
| 2007 | IM | Robust Monitoring of Network-wide Aggregates through Gossiping. | Fetahi Wuhib, Mads Dam, Rolf Stadler, Alexander Clemm |
| 2007 | LICS | A Complete Axiomatization of Knowledge and Cryptography. | Mika Cohen, Mads Dam |
| 2006 | POPL | Decidability and proof systems for language-based noninterference relations. | Mads Dam |
| 2003 | ESOP | On the Secure Implementation of Security Protocols. | Pablo Giambiagi, Mads Dam |
| 2003 | FOSSACS | On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the -Calculus. | Christoph Sprenger, Mads Dam |
| 2002 | SP | Constrained Delegation. | Olav L. Bandmann, Babak Sadighi Firozabadi, Mads Dam |
| 1999 | FM | Verifying a Distributed Database Lookup Manager Written in Erlang. | Thomas Arts, Mads Dam |
| 1998 | CADE | System Description: Verification of Distributed Erlang Programs. | Thomas Arts, Mads Dam, Lars-ke Fredlund, Dilian Gurov |
| 1998 | CONCUR | From Higher-Order pi-Calculus to pi-Calculus in the Presence of Static Operators. | Jos-Luis Vivas, Mads Dam |
| 1998 | SAC | On the verification of open distributed systems. | Mads Dam, Lars-ke Fredlund |
| 1995 | CONCUR | Compositional Proof Systems for Model Checking Infinite State Processes. | Mads Dam |
| 1993 | CONCUR | Model Checking Mobile Processes. | Mads Dam |
| 1988 | LICS | Relevance Logic and Concurrent Composition | Mads Dam |
| 1986 | ESOP | Compiler Generation from Relational Semantics. | Mads Dam, Frank Jensen |