Types, Subtypes, and ASL+. - David Aspinall 001 (COMPASS/ADT, 1994)

Subtyping with Singleton Types. - David Aspinall 001 (CSL, 1994)

Subtyping Dependent Types (Summary). - David Aspinall 001; Adriana B. Compagnoni (LICS, 1996)

Type systems for modular programs and specifications. - David Aspinall 001 (1997)

Subtyping with Power Types. - David Aspinall 001 (CSL, 2000)

Proof General: A Generic Tool for Proof Development. - David Aspinall 001 (TACAS, 2000)

Subtyping dependent types. - David Aspinall 001; Adriana B. Compagnoni (Theor. Comput. Sci., 2001)

From Specifications to Code in CASL. - David Aspinall 001; Donald Sannella (AMAST, 2002)

Another Type System for In-Place Update. - David Aspinall 001; Martin Hofmann 001 (ESOP, 2002)

Type Checking Parametrised Programs and Specifications in ASL+FPC. - David Aspinall 001 (WADT, 2002)

Preface. - David Aspinall 001; Christoph Lüth (UITP@TPHOLs, 2003)

Proof General meets IsaWin: Combining Text-Based And Graphical User Interfaces. - David Aspinall 001; Christoph Lüth (UITP@TPHOLs, 2003)

Heap-Bounded Assembly Language. - David Aspinall 001; Adriana B. Compagnoni (J. Autom. Reason., 2003)

Mobile Resource Guarantees for Smart Devices. - David Aspinall 001; Stephen Gilmore; Martin Hofmann 001; Donald Sannella; Ian Stark (CASSIS, 2004)

A Program Logic for Resource Verification. - David Aspinall 001; Lennart Beringer; Martin Hofmann 001; Hans-Wolfgang Loidl; Alberto Momigliano (TPHOLs, 2004)

Mobile Resource Guarantees and Policies. - David Aspinall 001; Kenneth MacKenzie (CASSIS, 2005)

Proof General / Eclipse: A Generic Interface for Interactive Proof. - Daniel Winterstein; David Aspinall 001; Christoph Lüth (IJCAI, 2005)

Assisted Proof Document Authoring. - David Aspinall 001; Christoph Lüth; Burkhart Wolff (MKM, 2005)

Mobile Resource Guarantees (project evaluation paper). - Donald Sannella; Martin Hofmann 001; David Aspinall 001; Stephen Gilmore; Ian Stark; Lennart Beringer; Hans-Wolfgang Loidl; Kenneth MacKenzie; Alberto Momigliano; Olha Shkaravska (Trends in Functional Programming, 2005)

Proof general in Eclipse: system and architecture overview. - David Aspinall 001; Daniel Winterstein; Christoph Lüth; Ahsan Fayyaz (ETX, 2006)

Optimisation Validation. - David Aspinall 001; Lennart Beringer; Alberto Momigliano (COCV@ETAPS, 2006)

Datatypes in Memory. - David Aspinall 001; Piotr Hoffman (CALCO, 2007)

Safety Guarantees from Explicit Resource Management. - David Aspinall 001; Patrick Maier 001; Ian Stark (FMCO, 2007)

A Framework for Interactive Proof. - David Aspinall 001; Christoph Lüth; Daniel Winterstein (Calculemus/MKM, 2007)

Formalising Java's Data Race Free Guarantee. - David Aspinall 001; Jaroslav Sevcík (TPHOLs, 2007)

Monitoring External Resources in Java MIDP. - David Aspinall 001; Patrick Maier 001; Ian Stark (REM@ESORICS, 2007)

Special Issue on User Interfaces in Theorem Proving: Preface. - David Aspinall 001; Christoph Lüth (J. Autom. Reason., 2007)

A program logic for resources. - David Aspinall 001; Lennart Beringer; Martin Hofmann 001; Hans-Wolfgang Loidl; Alberto Momigliano (Theor. Comput. Sci., 2007)

A Tactic Language for Hiproofs. - David Aspinall 001; Ewen Denney; Christoph Lüth (AISC/MKM/Calculemus, 2008)

On Validity of Program Transformations in the Java Memory Model. - Jaroslav Sevcík; David Aspinall 001 (ECOOP, 2008)

Towards Merging PlatOmega and PGIP. - David Aspinall 001; Serge Autexier; Christoph Lüth; Marc Wagner 001 (UITP@TPHOLs, 2008)

A type system with usage aspects. - David Aspinall 001; Martin Hofmann 001; Michal Konecný (J. Funct. Program., 2008)

Towards a Type System for Security APIs. - Gavin Keighren; David Aspinall 001; Graham Steel (ARSPA-WITS, 2009)

Personal choice and challenge questions: a security and usability assessment. - Mike Just; David Aspinall 001 (SOUPS, 2009)

Symbolic and Analytic Techniques for Resource Analysis of Java Bytecode. - David Aspinall 001; Robert Atkey; Kenneth MacKenzie; Donald Sannella (TGC, 2010)

Preface. - David Aspinall 001; Claudio Sacerdoti Coen (UITP, 2010)

Tactics for Hierarchical Proof. - David Aspinall 001; Ewen Denney; Christoph Lüth (Math. Comput. Sci., 2010)

Probing Attacks on Multi-Agent Systems Using Electronic Institutions. - Shahriar Bijani; David Robertson 001; David Aspinall 001 (DALT, 2011)

Towards Formal Proof Script Refactoring. - Iain Whiteside; David Aspinall 001; Lucas Dixon; Gudmund Grov (Calculemus/MKM, 2011)

An Essence of SSReflect. - Iain Whiteside; David Aspinall 001; Gudmund Grov (AISC/MKM/Calculemus, 2012)

On the security and usability of dual credential authentication in UK online banking. - Mike Just; David Aspinall 001 (ICITST, 2012)

Querying Proofs. - David Aspinall 001; Ewen Denney; Christoph Lüth (LPAR, 2012)

"Give Me Letters 2, 3 and 6!": Partial Password Implementations and Attacks. - David Aspinall 001; Mike Just (Financial Cryptography, 2013)

A Semantic Basis for Proof Queries and Transformations. - David Aspinall 001; Ewen Denney; Christoph Lüth (LPAR, 2013)

Polar: A Framework for Proof Refactoring. - Dominik Dietrich; Iain Whiteside; David Aspinall 001 (LPAR, 2013)

Capturing Hiproofs in HOL Light. - Steven Obua; Mark Adams; David Aspinall 001 (MKM/Calculemus/DML, 2013)

Towards an Authorization Framework for App Security Checking. - Joseph Hallett; David Aspinall 001 (ESSoS Doctoral Symposium, 2014)

Towards an amortized type system for JavaScript. - Daniel Franzen; David Aspinall 001 (SCSS, 2014)

Data Driven Authentication: On the Effectiveness of User Behaviour Modelling with Mobile Device Sensors. - Hilmi Günes Kayacik; Mike Just; Lynne Baillie; David Aspinall 001; Nicholas Micallef (CoRR, 2014)

ProofPeer: Collaborative Theorem Proving. - Steven Obua; Jacques D. Fleuriot; Phil Scott; David Aspinall 001 (CoRR, 2014)

EviCheck: Digital Evidence for Android. - Mohamed Nassim Seghir; David Aspinall 001 (ATVA, 2015)

Security testing for Android mHealth apps. - Konstantin Knorr; David Aspinall 001 (ICST Workshops, 2015)

Type Inference for ZFH. - Steven Obua; Jacques D. Fleuriot; Phil Scott; David Aspinall 001 (CICM, 2015)

Sensor use and usefulness: Trade-offs for data-driven authentication on mobile devices. - Nicholas Micallef; Hilmi Günes Kayacik; Mike Just; Lynne Baillie; David Aspinall 001 (PerCom, 2015)

On the Privacy, Security and Safety of Blood Pressure and Diabetes Apps. - Konstantin Knorr; David Aspinall 001; Maria Wolters (SEC, 2015)

Accessible Banking: Experiences and Future Directions. - Bela Gor; David Aspinall 001 (CoRR, 2015)

POSTER: Weighing in eHealth Security. - Martin Krämer; David Aspinall 001; Maria Wolters (CCS, 2016)

Explaining Unwanted Behaviours in Context. - Wei Chen 023; David Aspinall 001; Andrew D. Gordon 001; Charles Sutton; Igor Muttik (IMPS@ESSoS, 2016)

PhoneWrap - Injecting the "How Often" into Mobile Apps. - Daniel Franzen; David Aspinall 001 (IMPS@ESSoS, 2016)

AppPAL for Android - Capturing and Checking Mobile App Policies. - Joseph Hallett; David Aspinall 001 (ESSoS, 2016)

A text-mining approach to explain unwanted behaviours. - Wei Chen 023; David Aspinall 001; Andrew D. Gordon 001; Charles Sutton; Igor Muttik (EUROSEC, 2016)

Towards Formal Proof Metrics. - David Aspinall 001; Cezary Kaliszyk (FASE, 2016)

On Robust Malware Classifiers by Verifying Unwanted Behaviours. - Wei Chen 023; David Aspinall 001; Andrew D. Gordon 001; Charles Sutton; Igor Muttik (IFM, 2016)

What's in a Theorem Name? - David Aspinall 001; Cezary Kaliszyk (ITP, 2016)

Certified Lightweight Contextual Policies for Android. - Mohamed Nassim Seghir; David Aspinall 001; Lenka Mareková (SecDev, 2016)

More Semantics More Robust: Improving Android Malware Classifiers. - Wei Chen 023; David Aspinall 001; Andrew D. Gordon 001; Charles Sutton; Igor Muttik (WISEC, 2016)

DroidGen: Constraint-based and Data-Driven Policy Generation for Android. - Mohamed Nassim Seghir; David Aspinall 001 (CoRR, 2016)

How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation. - David Butler 002; David Aspinall 001; Adrià Gascón (ITP, 2017)

Capturing Policies for BYOD. - Joseph Hallett; David Aspinall 001 (SEC, 2017)

Formal Analysis of Sneak-Peek: A Data Centre Attack and Its Mitigations. - Wei Chen 023; Yuhui Lin; Vashti Galpin; Vivek Nigam; Myungjin Lee; David Aspinall 001 (SEC, 2018)

Secure information sharing in social agent interactions using information flow analysis. - Shahriar Bijani; David Robertson 001; David Aspinall 001 (Eng. Appl. Artif. Intell., 2018)

Foreword. - Martin Hofmann 001; David Aspinall 001; Brian Campbell 001; Ian Stark; Perdita Stevens (Theor. Comput. Sci., 2018)

Retrofitting Security and Privacy Measures to Smart Home Devices. - Chenghao Ye; Praburam Prabhakar Indra; David Aspinall 001 (IoTSMS, 2019)

On the Formalisation of Σ-Protocols and Commitment Schemes. - David Butler 002; David Aspinall 001; Adrià Gascón (POST, 2019)

Multi-Party Computation. - David Aspinall 001; David Butler 002 (Arch. Formal Proofs, 2019)

Formalising Oblivious Transfer in the Semi-Honest and Malicious Model in CryptHOL. - David Butler 002; David Aspinall 001; Adrià Gascón (IACR Cryptol. ePrint Arch., 2019)

Formalising Σ-Protocols and Commitment Schemes using CryptHOL. - David Butler 002; Andreas Lochbihler; David Aspinall 001; Adrià Gascón (IACR Cryptol. ePrint Arch., 2019)

Neural Networks, Secure by Construction - An Exploration of Refinement Types. - Wen Kokke; Ekaterina Komendantskaya; Daniel Kienitz; Robert Atkey; David Aspinall 001 (APLAS, 2020)

Better Anomaly Detection for Access Attacks Using Deep Bidirectional LSTMs. - Henry Clausen; Gudmund Grov; Marc Sabate; David Aspinall 001 (MLN, 2020)

Evading Stepping-Stone Detection with Enough Chaff. - Henry Clausen; Michael Scott Gibson; David Aspinall 001 (NSS, 2020)

Traffic Generation using Containerization for Machine Learning. - Henry Clausen; Robert Flood; David Aspinall 001 (CoRR, 2020)

Evaluating Model Robustness to Adversarial Samples in Network Intrusion Detection. - Madeleine Schneider; David Aspinall 001; Nathaniel D. Bastian (IEEE BigData, 2021)

Checking Contact Tracing App Implementations. - Robert Flood; Sheung Shi Chan; Wei Chen 023; David Aspinall 001 (ICISSP, 2021)

Controlling Network Traffic Microstructures for Machine-Learning Model Probing. - Henry Clausen; Robert Flood; David Aspinall 001 (SecureComm (1), 2021)

Examining traffic microstructures to improve model development. - Henry Clausen; David Aspinall 001 (SP (Workshops), 2021)

CBAM: A Contextual Model for Network Anomaly Detection. - Henry Clausen; Gudmund Grov; David Aspinall 001 (Comput., 2021)

Formalising $ varSigma$-Protocols and Commitment Schemes Using CryptHOL. - David Butler 002; Andreas Lochbihler; David Aspinall 001; Adrià Gascón (J. Autom. Reason., 2021)

Towards Interdependent Safety Security Assessments Using Bowties. - Luca Arnaboldi 001; David Aspinall 001 (SAFECOMP Workshops, 2022)

Checking Contact Tracing App Implementations with Bespoke Static Analysis. - Robert Flood; Sheung Chi Chan; Wei Chen 023; David Aspinall 001 (SN Comput. Sci., 2022)

Tactics for Account Access Graphs. - Luca Arnaboldi 001; David Aspinall 001; Christina Kolb; Sasa Radomirovic (ESORICS (3), 2023)

Generating Traffic-Level Adversarial Examples from Feature-Level Specifications. - Robert Flood; Marco Casadio; David Aspinall 001; Ekaterina Komendantskaya (ESORICS Workshops (2), 2024)

Measuring the Complexity of Benchmark NIDS Datasets via Spectral Analysis. - Robert Flood; David Aspinall 001 (EuroS&P Workshops, 2024)

Bad Design Smells in Benchmark NIDS Datasets. - Robert Flood; Gints Engelen; David Aspinall 001; Lieven Desmet (EuroS&P, 2024)

Measuring Cyber Essentials Security Policies. - Sándor Bartha; Russell Ballantine; David Aspinall 001 (CSET @ USENIX Security Symposium, 2024)

Formally Verifying Robustness and Generalisation of Network Intrusion Detection Models. - Robert Flood; Marco Casadio; David Aspinall 001; Ekaterina Komendantskaya (SAC, 2025)

From Bouncing Break-ins to Frictional Firewalls: Ideas About Interacting Requirements for Vehicle Safety and Security. - Luca Arnaboldi 001; David Aspinall 001; Christina Kolb; Sasa Radomirovic (SAFECOMP (Workshops), 2025)