| 2025 | SAC | Formally Verifying Robustness and Generalisation of Network Intrusion Detection Models. | Robert Flood, Marco Casadio, David Aspinall, Ekaterina Komendantskaya |
| 2025 | SAFECOMP | From Bouncing Break-ins to Frictional Firewalls: Ideas About Interacting Requirements for Vehicle Safety and Security. | Luca Arnaboldi, David Aspinall, Christina Kolb, Sasa Radomirovic |
| 2024 | ESORICS | Generating Traffic-Level Adversarial Examples from Feature-Level Specifications. | Robert Flood, Marco Casadio, David Aspinall, Ekaterina Komendantskaya |
| 2023 | ESORICS | Tactics for Account Access Graphs. | Luca Arnaboldi, David Aspinall, Christina Kolb, Sasa Radomirovic |
| 2022 | SAFECOMP | Towards Interdependent Safety Security Assessments Using Bowties. | Luca Arnaboldi, David Aspinall |
| 2021 | ICISSP | Checking Contact Tracing App Implementations. | Robert Flood, Sheung Shi Chan, Wei Chen, David Aspinall |
| 2021 | SP | Examining traffic microstructures to improve model development. | Henry Clausen, David Aspinall |
| 2021 | SecureComm | Controlling Network Traffic Microstructures for Machine-Learning Model Probing. | Henry Clausen, Robert Flood, David Aspinall |
| 2020 | APLAS | Neural Networks, Secure by Construction - An Exploration of Refinement Types. | Wen Kokke, Ekaterina Komendantskaya, Daniel Kienitz, Robert Atkey, David Aspinall |
| 2020 | CPP | Formalising oblivious transfer in the semi-honest and malicious model in CryptHOL. | David Butler, David Aspinall, Adri Gascn |
| 2020 | NSS | Evading Stepping-Stone Detection with Enough Chaff. | Henry Clausen, Michael Scott Gibson, David Aspinall |
| 2018 | SEC | Formal Analysis of Sneak-Peek: A Data Centre Attack and Its Mitigations. | Wei Chen, Yuhui Lin, Vashti Galpin, Vivek Nigam, Myungjin Lee, David Aspinall |
| 2017 | ITP | How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation. | David Butler, David Aspinall, Adri Gascn |
| 2017 | SEC | Capturing Policies for BYOD. | Joseph Hallett, David Aspinall |
| 2016 | CCS | POSTER: Weighing in eHealth Security. | Martin Krmer, David Aspinall, Maria Wolters |
| 2016 | FASE | Towards Formal Proof Metrics. | David Aspinall, Cezary Kaliszyk |
| 2016 | IFM | On Robust Malware Classifiers by Verifying Unwanted Behaviours. | Wei Chen, David Aspinall, Andrew D. Gordon, Charles Sutton, Igor Muttik |
| 2016 | ITP | What's in a Theorem Name? | David Aspinall, Cezary Kaliszyk |
| 2015 | ATVA | EviCheck: Digital Evidence for Android. | Mohamed Nassim Seghir, David Aspinall |
| 2015 | ICST | Security testing for Android mHealth apps. | Konstantin Knorr, David Aspinall |
| 2015 | PERCOM | Sensor use and usefulness: Trade-offs for data-driven authentication on mobile devices. | Nicholas Micallef, Hilmi Gnes Kayacik, Mike Just, Lynne Baillie, David Aspinall |
| 2015 | SEC | On the Privacy, Security and Safety of Blood Pressure and Diabetes Apps. | Konstantin Knorr, David Aspinall, Maria Wolters |
| 2013 | FC | "Give Me Letters 2, 3 and 6!": Partial Password Implementations and Attacks. | David Aspinall, Mike Just |
| 2013 | LPAR | A Semantic Basis for Proof Queries and Transformations. | David Aspinall, Ewen Denney, Christoph Lth |
| 2013 | LPAR | Polar: A Framework for Proof Refactoring. | Dominik Dietrich, Iain Whiteside, David Aspinall |
| 2012 | AISC | An Essence of SSReflect. | Iain Whiteside, David Aspinall, Gudmund Grov |
| 2012 | LPAR | Querying Proofs. | David Aspinall, Ewen Denney, Christoph Lth |
| 2009 | SOUPS | Personal choice and challenge questions: a security and usability assessment. | Mike Just, David Aspinall |
| 2008 | AISC | A Tactic Language for Hiproofs. | David Aspinall, Ewen Denney, Christoph Lth |
| 2008 | ECOOP | On Validity of Program Transformations in the Java Memory Model. | Jaroslav Sevck, David Aspinall |
| 2007 | CALCO | Datatypes in Memory. | David Aspinall, Piotr Hoffman |
| 2005 | IJCAI | Proof General / Eclipse: A Generic Interface for Interactive Proof. | Daniel Winterstein, David Aspinall, Christoph Lth |
| 2002 | ESOP | Another Type System for In-Place Update. | David Aspinall, Martin Hofmann |
| 2000 | CSL | Subtyping with Power Types. | David Aspinall |
| 2000 | TACAS | Proof General: A Generic Tool for Proof Development. | David Aspinall |
| 1996 | LICS | Subtyping Dependent Types (Summary). | David Aspinall, Adriana B. Compagnoni |
| 1994 | COMPASS | Types, Subtypes, and ASL+. | David Aspinall |
| 1994 | CSL | Subtyping with Singleton Types. | David Aspinall |
| 1990 | ICASSP | Architecture of a highly reliable systolic correlator array. | Ravi Ramaswamy, Gavin Brebner, David Aspinall |