David Aspinall

ORCID

Publication Activity (10 Years)

Years Active: 1994-2024
Publications (10 Years): 38

Top Venues

University of Edinburgh, UK (PHD)

Education History

University of Edinburgh, UK

PHD

Publications

Sándor Bartha, Russell Ballantine, David Aspinall
Measuring Cyber Essentials Security Policies. CSET @ USENIX Security Symposium (2024)
Luca Arnaboldi, David Aspinall, Christina Kolb, Sasa Radomirovic
Tactics for Account Access Graphs. ESORICS (3) (2023)
Luca Arnaboldi, David Aspinall
Towards Interdependent Safety Security Assessments Using Bowties. SAFECOMP Workshops (2022)
Robert Flood, Sheung Chi Chan, Wei Chen, David Aspinall
Checking Contact Tracing App Implementations with Bespoke Static Analysis. SN Comput. Sci. 3 (6) (2022)
Luca Arnaboldi, David Aspinall
Towards Interdependent Safety Security Assessments using Bowties. CoRR (2022)
Henry Clausen, David Aspinall
Examining traffic microstructures to improve model development. SP Workshops (2021)
Robert Flood, Sheung Shi Chan, Wei Chen, David Aspinall
Checking Contact Tracing App Implementations. ICISSP (2021)
Madeleine Schneider, David Aspinall, Nathaniel D. Bastian
Evaluating Model Robustness to Adversarial Samples in Network Intrusion Detection. IEEE BigData (2021)
Henry Clausen, Gudmund Grov, David Aspinall
CBAM: A Contextual Model for Network Anomaly Detection. Comput. 10 (6) (2021)
David Butler, Andreas Lochbihler, David Aspinall, Adrià Gascón
Formalising $\varSigma$-Protocols and Commitment Schemes Using CryptHOL. J. Autom. Reason. 65 (4) (2021)
Henry Clausen, Robert Flood, David Aspinall
Controlling Network Traffic Microstructures for Machine-Learning Model Probing. SecureComm (1) (2021)
Henry Clausen, Robert Flood, David Aspinall
Traffic Generation using Containerization for Machine Learning. CoRR (2020)
Henry Clausen, Michael S. Gibson, David Aspinall
Evading Stepping-Stone Detection with Enough Chaff. NSS (2020)
Henry Clausen, Gudmund Grov, Marc Sabate, David Aspinall
Better Anomaly Detection for Access Attacks Using Deep Bidirectional LSTMs. MLN (2020)
Wen Kokke, Ekaterina Komendantskaya, Daniel Kienitz, Robert Atkey, David Aspinall
Neural Networks, Secure by Construction - An Exploration of Refinement Types. APLAS (2020)
David Butler, David Aspinall, Adrià Gascón
Formalising oblivious transfer in the semi-honest and malicious model in CryptHOL. CPP (2020)
David Butler, David Aspinall, Adrià Gascón
On the Formalisation of Σ-Protocols and Commitment Schemes. POST (2019)
David Aspinall, David Butler
Multi-Party Computation. Arch. Formal Proofs 2019 (2019)
Chenghao Ye, Praburam Prabhakar Indra, David Aspinall
Retrofitting Security and Privacy Measures to Smart Home Devices. IoTSMS (2019)
David Butler, Andreas Lochbihler, David Aspinall, Adrià Gascón
Formalising Σ-Protocols and Commitment Schemes using CryptHOL. IACR Cryptol. ePrint Arch. 2019 (2019)
David Butler, David Aspinall, Adrià Gascón
Formalising Oblivious Transfer in the Semi-Honest and Malicious Model in CryptHOL. IACR Cryptol. ePrint Arch. 2019 (2019)
Martin Hofmann, David Aspinall, Brian Campbell, Ian Stark, Perdita Stevens
Foreword. Theor. Comput. Sci. 741 (2018)
Wei Chen, Yuhui Lin, Vashti Galpin, Vivek Nigam, Myungjin Lee, David Aspinall
Formal Analysis of Sneak-Peek: A Data Centre Attack and Its Mitigations. SEC (2018)
Shahriar Bijani, David Robertson, David Aspinall
Secure information sharing in social agent interactions using information flow analysis. Eng. Appl. Artif. Intell. 70 (2018)
David Butler, David Aspinall, Adrià Gascón
How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation. CoRR (2018)
Joseph Hallett, David Aspinall
Capturing Policies for BYOD. SEC (2017)
David Butler, David Aspinall, Adrià Gascón
How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation. ITP (2017)
Mohamed Nassim Seghir, David Aspinall, Lenka Mareková
Certified Lightweight Contextual Policies for Android. SecDev (2016)
Mohamed Nassim Seghir, David Aspinall
DroidGen: Constraint-based and Data-Driven Policy Generation for Android. CoRR (2016)
Martin Krämer, David Aspinall, Maria Wolters
POSTER: Weighing in eHealth Security. CCS (2016)
David Aspinall, Cezary Kaliszyk
What's in a Theorem Name? ITP (2016)
Wei Chen, David Aspinall, Andrew D. Gordon, Charles Sutton, Igor Muttik
A text-mining approach to explain unwanted behaviours. EUROSEC (2016)
Daniel Franzen, David Aspinall
PhoneWrap - Injecting the "How Often" into Mobile Apps. IMPS@ESSoS (2016)
Wei Chen, David Aspinall, Andrew D. Gordon, Charles Sutton, Igor Muttik
Explaining Unwanted Behaviours in Context. IMPS@ESSoS (2016)
Wei Chen, David Aspinall, Andrew D. Gordon, Charles Sutton, Igor Muttik
On Robust Malware Classifiers by Verifying Unwanted Behaviours. IFM (2016)
David Aspinall, Cezary Kaliszyk
Towards Formal Proof Metrics. FASE (2016)
Joseph Hallett, David Aspinall
AppPAL for Android - Capturing and Checking Mobile App Policies. ESSoS (2016)
Wei Chen, David Aspinall, Andrew D. Gordon, Charles Sutton, Igor Muttik
More Semantics More Robust: Improving Android Malware Classifiers. WISEC (2016)
Mohamed Nassim Seghir, David Aspinall
EviCheck: Digital Evidence for Android. ATVA (2015)
Bela Gor, David Aspinall
Accessible Banking: Experiences and Future Directions. CoRR (2015)
Steven Obua, Jacques D. Fleuriot, Phil Scott, David Aspinall
Type Inference for ZFH. CICM (2015)
Nicholas Micallef, Hilmi Günes Kayacik, Mike Just, Lynne Baillie, David Aspinall
Sensor use and usefulness: Trade-offs for data-driven authentication on mobile devices. PerCom (2015)
Konstantin Knorr, David Aspinall
Security testing for Android mHealth apps. ICST Workshops (2015)
Konstantin Knorr, David Aspinall, Maria Wolters
On the Privacy, Security and Safety of Blood Pressure and Diabetes Apps. SEC (2015)
Steven Obua, Jacques D. Fleuriot, Phil Scott, David Aspinall
ProofPeer: Collaborative Theorem Proving. CoRR (2014)
Hilmi Günes Kayacik, Mike Just, Lynne Baillie, David Aspinall, Nicholas Micallef
Data Driven Authentication: On the Effectiveness of User Behaviour Modelling with Mobile Device Sensors. CoRR (2014)
Daniel Franzen, David Aspinall
Towards an amortized type system for JavaScript. SCSS (2014)
Joseph Hallett, David Aspinall
Towards an Authorization Framework for App Security Checking. ESSoS Doctoral Symposium (2014)
Steven Obua, Mark Adams, David Aspinall
Capturing Hiproofs in HOL Light. CoRR (2013)
David Aspinall, Mike Just
"Give Me Letters 2, 3 and 6!": Partial Password Implementations and Attacks. Financial Cryptography (2013)
David Aspinall, Ewen Denney, Christoph Lüth
A Semantic Basis for Proof Queries and Transformations. LPAR (2013)
Steven Obua, Mark Adams, David Aspinall
Capturing Hiproofs in HOL Light. MKM/Calculemus/DML (2013)
Dominik Dietrich, Iain Whiteside, David Aspinall
Polar: A Framework for Proof Refactoring. LPAR (2013)
Mike Just, David Aspinall
On the security and usability of dual credential authentication in UK online banking. ICITST (2012)
David Aspinall, Claudio Sacerdoti Coen
Preface. Electron. Notes Theor. Comput. Sci. 285 (2012)
David Aspinall, Ewen Denney, Christoph Lüth
Querying Proofs. LPAR (2012)
Iain Whiteside, David Aspinall, Gudmund Grov
An Essence of SSReflect. AISC/MKM/Calculemus (2012)
Iain Whiteside, David Aspinall, Lucas Dixon, Gudmund Grov
Towards Formal Proof Script Refactoring. Calculemus/MKM (2011)
Shahriar Bijani, David Robertson, David Aspinall
Probing Attacks on Multi-Agent Systems Using Electronic Institutions. DALT (2011)
David Aspinall, Ewen Denney, Christoph Lüth
Tactics for Hierarchical Proof. Math. Comput. Sci. 3 (3) (2010)
David Aspinall, Robert Atkey, Kenneth MacKenzie, Donald Sannella
Symbolic and Analytic Techniques for Resource Analysis of Java Bytecode. TGC (2010)
Gavin Keighren, David Aspinall, Graham Steel
Towards a Type System for Security APIs. ARSPA-WITS (2009)
Mike Just, David Aspinall
Personal choice and challenge questions: a security and usability assessment. SOUPS (2009)
David Aspinall, Serge Autexier, Christoph Lüth, Marc Wagner
Towards Merging PlatOmega and PGIP. Electron. Notes Theor. Comput. Sci. 226 (2009)
David Aspinall, Martin Hofmann, Michal Konecný
A type system with usage aspects. J. Funct. Program. 18 (2) (2008)
Jaroslav Sevcík, David Aspinall
On Validity of Program Transformations in the Java Memory Model. ECOOP (2008)
David Aspinall, Ewen Denney, Christoph Lüth
A Tactic Language for Hiproofs. AISC/MKM/Calculemus (2008)
David Aspinall, Patrick Maier, Ian Stark
Monitoring External Resources in Java MIDP. Electron. Notes Theor. Comput. Sci. 197 (1) (2008)
David Aspinall, Jaroslav Sevcík
Formalising Java's Data Race Free Guarantee. TPHOLs (2007)
David Aspinall, Patrick Maier, Ian Stark
Safety Guarantees from Explicit Resource Management. FMCO (2007)
David Aspinall, Lennart Beringer, Alberto Momigliano
Optimisation Validation. Electron. Notes Theor. Comput. Sci. 176 (3) (2007)
David Aspinall, Christoph Lüth, Daniel Winterstein
A Framework for Interactive Proof. Calculemus/MKM (2007)
David Aspinall, Piotr Hoffman
Datatypes in Memory. CALCO (2007)
David Aspinall, Lennart Beringer, Martin Hofmann, Hans-Wolfgang Loidl, Alberto Momigliano
A program logic for resources. Theor. Comput. Sci. 389 (3) (2007)
David Aspinall, Christoph Lüth
Special Issue on User Interfaces in Theorem Proving: Preface. J. Autom. Reason. 39 (2) (2007)
David Aspinall, Daniel Winterstein, Christoph Lüth, Ahsan Fayyaz
Proof general in Eclipse: system and architecture overview. ETX (2006)
Daniel Winterstein, David Aspinall, Christoph Lüth
Proof General / Eclipse: A Generic Interface for Interactive Proof. IJCAI (2005)
David Aspinall, Kenneth MacKenzie
Mobile Resource Guarantees and Policies. CASSIS (2005)
Donald Sannella, Martin Hofmann, David Aspinall, Stephen Gilmore, Ian Stark, Lennart Beringer, Hans-Wolfgang Loidl, Kenneth MacKenzie, Alberto Momigliano, Olha Shkaravska
Mobile Resource Guarantees (project evaluation paper). Trends in Functional Programming (2005)
David Aspinall, Christoph Lüth, Burkhart Wolff
Assisted Proof Document Authoring. MKM (2005)
David Aspinall, Lennart Beringer, Martin Hofmann, Hans-Wolfgang Loidl, Alberto Momigliano
A Program Logic for Resource Verification. TPHOLs (2004)
David Aspinall, Stephen Gilmore, Martin Hofmann, Donald Sannella, Ian Stark
Mobile Resource Guarantees for Smart Devices. CASSIS (2004)
David Aspinall, Christoph Lüth
Preface. Electron. Notes Theor. Comput. Sci. 103 (2004)
David Aspinall, Christoph Lüth
Proof General meets IsaWin: Combining Text-Based And Graphical User Interfaces. Electron. Notes Theor. Comput. Sci. 103 (2004)
David Aspinall, Adriana B. Compagnoni
Heap-Bounded Assembly Language. J. Autom. Reason. 31 (3-4) (2003)
David Aspinall, Donald Sannella
From Specifications to Code in CASL. AMAST (2002)
David Aspinall, Martin Hofmann
Another Type System for In-Place Update. ESOP (2002)
David Aspinall
. WADT (2002)
David Aspinall, Adriana B. Compagnoni
Subtyping dependent types. Theor. Comput. Sci. 266 (1-2) (2001)
David Aspinall
Subtyping with Power Types. CSL (2000)
David Aspinall
Proof General: A Generic Tool for Proof Development. TACAS (2000)
David Aspinall, Adriana B. Compagnoni
Subtyping Dependent Types (Summary). LICS (1996)
David Aspinall
Subtyping with Singleton Types. CSL (1994)
David Aspinall
Types, Subtypes, and ASL+. COMPASS/ADT (1994)

David Aspinall.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

David Aspinall