default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDDavid Aspinall 0001
Person information
- affiliation: University of Edinburgh, UK
Other persons with the same name
- David Aspinall 0002 — University of Manchester, UK (and 1 more)
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
Books and Theses
- 1997
[b1]David Aspinall:
Type systems for modular programs and specifications. University of Edinburgh, UK, 1997
Journal Articles
- 2022
- [j12]Robert Flood
, Sheung Chi Chan, Wei Chen, David Aspinall:
Checking Contact Tracing App Implementations with Bespoke Static Analysis. SN Comput. Sci. 3(6): 496 (2022) - 2021
- [j11]Henry Clausen, Gudmund Grov, David Aspinall:
CBAM: A Contextual Model for Network Anomaly Detection. Comput. 10(6): 79 (2021) - [j10]David Butler, Andreas Lochbihler, David Aspinall, Adrià Gascón:
Formalising $\varSigma$-Protocols and Commitment Schemes Using CryptHOL. J. Autom. Reason. 65(4): 521-567 (2021) - 2019
- [j9]David Aspinall, David Butler:
Multi-Party Computation. Arch. Formal Proofs 2019 (2019) - 2018
- [j8]Shahriar Bijani, David Robertson, David Aspinall:
Secure information sharing in social agent interactions using information flow analysis. Eng. Appl. Artif. Intell. 70: 52-66 (2018) - [j7]Martin Hofmann, David Aspinall, Brian Campbell, Ian Stark, Perdita Stevens:
Foreword. Theor. Comput. Sci. 741: 1-2 (2018) - 2010
- [j6]David Aspinall, Ewen Denney, Christoph Lüth:
Tactics for Hierarchical Proof. Math. Comput. Sci. 3(3): 309-330 (2010) - 2008
- [j5]David Aspinall, Martin Hofmann, Michal Konecný:
A type system with usage aspects. J. Funct. Program. 18(2): 141-178 (2008) - 2007
- [j4]David Aspinall, Christoph Lüth:
Special Issue on User Interfaces in Theorem Proving: Preface. J. Autom. Reason. 39(2): 107-108 (2007) - [j3]David Aspinall, Lennart Beringer, Martin Hofmann, Hans-Wolfgang Loidl, Alberto Momigliano:
A program logic for resources. Theor. Comput. Sci. 389(3): 411-445 (2007) - 2003
- [j2]David Aspinall, Adriana B. Compagnoni:
Heap-Bounded Assembly Language. J. Autom. Reason. 31(3-4): 261-302 (2003) - 2001
- [j1]David Aspinall, Adriana B. Compagnoni:
Subtyping dependent types. Theor. Comput. Sci. 266(1-2): 273-309 (2001)
Conference and Workshop Papers
- 2024
- [c74]Robert Flood, David Aspinall:
Measuring the Complexity of Benchmark NIDS Datasets via Spectral Analysis. EuroS&P Workshops 2024: 335-341 - [c73]Robert Flood, Gints Engelen, David Aspinall, Lieven Desmet:
Bad Design Smells in Benchmark NIDS Datasets. EuroS&P 2024: 658-675 - [c72]Sándor Bartha, Russell Ballantine, David Aspinall:
Measuring Cyber Essentials Security Policies. CSET @ USENIX Security Symposium 2024: 17-26 - 2023
- [c71]Luca Arnaboldi, David Aspinall, Christina Kolb, Sasa Radomirovic:
Tactics for Account Access Graphs. ESORICS (3) 2023: 452-470 - 2022
- [c70]Luca Arnaboldi, David Aspinall:
Towards Interdependent Safety Security Assessments Using Bowties. SAFECOMP Workshops 2022: 211-229 - 2021
- [c69]Madeleine Schneider, David Aspinall, Nathaniel D. Bastian:
Evaluating Model Robustness to Adversarial Samples in Network Intrusion Detection. IEEE BigData 2021: 3343-3352 - [c68]Robert Flood, Sheung Shi Chan, Wei Chen, David Aspinall:
Checking Contact Tracing App Implementations. ICISSP 2021: 133-144 - [c67]Henry Clausen, Robert Flood, David Aspinall:
Controlling Network Traffic Microstructures for Machine-Learning Model Probing. SecureComm (1) 2021: 456-475 - [c66]Henry Clausen, David Aspinall:
Examining traffic microstructures to improve model development. SP (Workshops) 2021: 19-24 - 2020
- [c65]Wen Kokke, Ekaterina Komendantskaya, Daniel Kienitz, Robert Atkey, David Aspinall:
Neural Networks, Secure by Construction - An Exploration of Refinement Types. APLAS 2020: 67-85 - [c64]David Butler, David Aspinall, Adrià Gascón:
Formalising oblivious transfer in the semi-honest and malicious model in CryptHOL. CPP 2020: 229-243 - [c63]Henry Clausen, Gudmund Grov, Marc Sabate, David Aspinall:
Better Anomaly Detection for Access Attacks Using Deep Bidirectional LSTMs. MLN 2020: 1-18 - [c62]Henry Clausen, Michael Scott Gibson, David Aspinall:
Evading Stepping-Stone Detection with Enough Chaff. NSS 2020: 431-446 - 2019
- [c61]Chenghao Ye, Praburam Prabhakar Indra, David Aspinall:
Retrofitting Security and Privacy Measures to Smart Home Devices. IoTSMS 2019: 283-290 - [c60]David Butler, David Aspinall, Adrià Gascón:
On the Formalisation of Σ-Protocols and Commitment Schemes. POST 2019: 175-196 - 2018
- [c59]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: 307-322 - 2017
- [c58]David Butler, David Aspinall, Adrià Gascón:
How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation. ITP 2017: 114-130 - [c57]Joseph Hallett, David Aspinall:
Capturing Policies for BYOD. SEC 2017: 310-323 - 2016
- [c56]Martin Krämer, David Aspinall, Maria Wolters:
POSTER: Weighing in eHealth Security. CCS 2016: 1832-1834 - [c55]Daniel Franzen, David Aspinall:
PhoneWrap - Injecting the "How Often" into Mobile Apps. IMPS@ESSoS 2016: 11-19 - [c54]Wei Chen, David Aspinall, Andrew D. Gordon, Charles Sutton, Igor Muttik:
Explaining Unwanted Behaviours in Context. IMPS@ESSoS 2016: 38-45 - [c53]Joseph Hallett, David Aspinall:
AppPAL for Android - Capturing and Checking Mobile App Policies. ESSoS 2016: 216-232 - [c52]Wei Chen, David Aspinall, Andrew D. Gordon, Charles Sutton, Igor Muttik:
A text-mining approach to explain unwanted behaviours. EUROSEC 2016: 4:1-4:6 - [c51]David Aspinall, Cezary Kaliszyk:
Towards Formal Proof Metrics. FASE 2016: 325-341 - [c50]Wei Chen, David Aspinall, Andrew D. Gordon, Charles Sutton, Igor Muttik:
On Robust Malware Classifiers by Verifying Unwanted Behaviours. IFM 2016: 326-341 - [c49]David Aspinall, Cezary Kaliszyk:
What's in a Theorem Name? ITP 2016: 459-465 - [c48]Mohamed Nassim Seghir, David Aspinall, Lenka Mareková:
Certified Lightweight Contextual Policies for Android. SecDev 2016: 94-100 - [c47]Wei Chen, David Aspinall, Andrew D. Gordon, Charles Sutton, Igor Muttik:
More Semantics More Robust: Improving Android Malware Classifiers. WISEC 2016: 147-158 - 2015
- [c46]Mohamed Nassim Seghir, David Aspinall:
EviCheck: Digital Evidence for Android. ATVA 2015: 221-227 - [c45]Konstantin Knorr, David Aspinall:
Security testing for Android mHealth apps. ICST Workshops 2015: 1-8 - [c44]Steven Obua, Jacques D. Fleuriot, Phil Scott, David Aspinall:
Type Inference for ZFH. CICM 2015: 87-101 - [c43]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: 189-197 - [c42]Konstantin Knorr, David Aspinall, Maria Wolters:
On the Privacy, Security and Safety of Blood Pressure and Diabetes Apps. SEC 2015: 571-584 - 2014
- [c41]Joseph Hallett, David Aspinall:
Towards an Authorization Framework for App Security Checking. ESSoS Doctoral Symposium 2014 - [c40]Daniel Franzen, David Aspinall:
Towards an amortized type system for JavaScript. SCSS 2014: 12-26 - 2013
- [c39]David Aspinall, Mike Just:
"Give Me Letters 2, 3 and 6!": Partial Password Implementations and Attacks. Financial Cryptography 2013: 126-143 - [c38]David Aspinall, Ewen Denney, Christoph Lüth:
A Semantic Basis for Proof Queries and Transformations. LPAR 2013: 53-70 - [c37]Dominik Dietrich, Iain Whiteside, David Aspinall:
Polar: A Framework for Proof Refactoring. LPAR 2013: 776-791 - [c36]Steven Obua, Mark Adams, David Aspinall:
Capturing Hiproofs in HOL Light. MKM/Calculemus/DML 2013: 184-199 - 2012
- [c35]Iain Whiteside, David Aspinall, Gudmund Grov:
An Essence of SSReflect. AISC/MKM/Calculemus 2012: 186-201 - [c34]Mike Just, David Aspinall:
On the security and usability of dual credential authentication in UK online banking. ICITST 2012: 259-264 - [c33]David Aspinall, Ewen Denney, Christoph Lüth:
Querying Proofs. LPAR 2012: 92-106 - 2011
- [c32]Shahriar Bijani, David Robertson, David Aspinall:
Probing Attacks on Multi-Agent Systems Using Electronic Institutions. DALT 2011: 33-50 - [c31]Iain Whiteside, David Aspinall, Lucas Dixon, Gudmund Grov:
Towards Formal Proof Script Refactoring. Calculemus/MKM 2011: 260-275 - 2010
- [c30]David Aspinall, Robert Atkey, Kenneth MacKenzie, Donald Sannella:
Symbolic and Analytic Techniques for Resource Analysis of Java Bytecode. TGC 2010: 1-22 - [c29]David Aspinall, Claudio Sacerdoti Coen:
Preface. UITP 2010: 1-2 - 2009
- [c28]Gavin Keighren, David Aspinall, Graham Steel:
Towards a Type System for Security APIs. ARSPA-WITS 2009: 173-192 - [c27]Mike Just, David Aspinall:
Personal choice and challenge questions: a security and usability assessment. SOUPS 2009 - 2008
- [c26]David Aspinall, Ewen Denney, Christoph Lüth:
A Tactic Language for Hiproofs. AISC/MKM/Calculemus 2008: 339-354 - [c25]Jaroslav Sevcík, David Aspinall:
On Validity of Program Transformations in the Java Memory Model. ECOOP 2008: 27-51 - [c24]David Aspinall, Serge Autexier, Christoph Lüth, Marc Wagner:
Towards Merging PlatOmega and PGIP. UITP@TPHOLs 2008: 3-21 - 2007
- [c23]David Aspinall, Piotr Hoffman:
Datatypes in Memory. CALCO 2007: 111-125 - [c22]David Aspinall, Patrick Maier, Ian Stark:
Safety Guarantees from Explicit Resource Management. FMCO 2007: 52-71 - [c21]David Aspinall, Christoph Lüth, Daniel Winterstein:
A Framework for Interactive Proof. Calculemus/MKM 2007: 161-175 - [c20]David Aspinall, Jaroslav Sevcík:
Formalising Java's Data Race Free Guarantee. TPHOLs 2007: 22-37 - [c19]David Aspinall, Patrick Maier, Ian Stark:
Monitoring External Resources in Java MIDP. REM@ESORICS 2007: 17-30 - 2006
- [c18]David Aspinall, Daniel Winterstein, Christoph Lüth, Ahsan Fayyaz:
Proof general in Eclipse: system and architecture overview. ETX 2006: 45-49 - [c17]David Aspinall, Lennart Beringer, Alberto Momigliano:
Optimisation Validation. COCV@ETAPS 2006: 37-59 - 2005
- [c16]David Aspinall, Kenneth MacKenzie:
Mobile Resource Guarantees and Policies. CASSIS 2005: 16-36 - [c15]Daniel Winterstein, David Aspinall, Christoph Lüth:
Proof General / Eclipse: A Generic Interface for Interactive Proof. IJCAI 2005: 1587-1588 - [c14]David Aspinall, Christoph Lüth, Burkhart Wolff:
Assisted Proof Document Authoring. MKM 2005: 65-80 - [c13]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: 211-226 - 2004
- [c12]David Aspinall, Stephen Gilmore, Martin Hofmann, Donald Sannella, Ian Stark:
Mobile Resource Guarantees for Smart Devices. CASSIS 2004: 1-26 - [c11]David Aspinall, Lennart Beringer, Martin Hofmann, Hans-Wolfgang Loidl, Alberto Momigliano:
A Program Logic for Resource Verification. TPHOLs 2004: 34-49 - 2003
- [c10]David Aspinall, Christoph Lüth:
Preface. UITP@TPHOLs 2003: 1-2 - [c9]David Aspinall, Christoph Lüth:
Proof General meets IsaWin: Combining Text-Based And Graphical User Interfaces. UITP@TPHOLs 2003: 3-26 - 2002
- [c8]David Aspinall, Donald Sannella:
From Specifications to Code in CASL. AMAST 2002: 1-14 - [c7]David Aspinall, Martin Hofmann:
Another Type System for In-Place Update. ESOP 2002: 36-52 - [c6]David Aspinall:
Type Checking Parametrised Programs and Specifications in ASL+FPC. WADT 2002: 129-144 - 2000
- [c5]David Aspinall:
Subtyping with Power Types. CSL 2000: 156-171 - [c4]David Aspinall:
Proof General: A Generic Tool for Proof Development. TACAS 2000: 38-42 - 1996
- [c3]David Aspinall, Adriana B. Compagnoni:
Subtyping Dependent Types (Summary). LICS 1996: 86-97 - 1994
- [c2]David Aspinall:
Types, Subtypes, and ASL+. COMPASS/ADT 1994: 116-131 - [c1]David Aspinall:
Subtyping with Singleton Types. CSL 1994: 1-15
Editorship
- 2016
- [e6]David Aspinall, Lorenzo Cavallaro, Mohamed Nassim Seghir, Melanie Volkamer:
Proceedings of the 1st International Workshop on Innovations in Mobile Privacy and Security, IMPS 2016, co-located with the International Symposium on Engineering Secure Software and Systems (ESSoS 2016), London, UK, April 6, 2016. CEUR Workshop Proceedings 1575, CEUR-WS.org 2016 [contents] - [e5]David Aspinall, Jan Camenisch, Marit Hansen, Simone Fischer-Hübner, Charles D. Raab:
Privacy and Identity Management. Time for a Revolution? - 10th IFIP WG 9.2, 9.5, 9.6/11.7, 11.4, 11.6/SIG 9.2.2 International Summer School, Edinburgh, UK, August 16-21, 2015, Revised Selected Papers. IFIP Advances in Information and Communication Technology 476, Springer 2016, ISBN 978-3-319-41762-2 [contents] - 2013
- [e4]Christoph Lange, David Aspinall, Jacques Carette, James H. Davenport, Andrea Kohlhase, Michael Kohlhase, Paul Libbrecht, Pedro Quaresma, Florian Rabe, Petr Sojka, Iain Whiteside, Wolfgang Windsteiger:
Joint Proceedings of the MathUI, OpenMath, PLMMS and ThEdu Workshops and Work in Progress at CICM, Bath, UK. CEUR Workshop Proceedings 1010, CEUR-WS.org 2013 [contents] - [e3]Jacques Carette, David Aspinall, Christoph Lange, Petr Sojka, Wolfgang Windsteiger:
Intelligent Computer Mathematics - MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings. Lecture Notes in Computer Science 7961, Springer 2013, ISBN 978-3-642-39319-8 [contents] - 2012
- [e2]David Aspinall, Claudio Sacerdoti Coen:
Proceedings of the 9th International Workshop On User Interfaces for Theorem Provers, UITP 2010, Edinburgh, UK, July 15, 2010. Electronic Notes in Theoretical Computer Science 285, Elsevier 2012 [contents] - 2004
- [e1]David Aspinall, Christoph Lüth:
Proceedings of the User Interfaces for Theorem Provers Workshop, UITP@TPHOLs 2003, Rome, Italy, September 8, 2003. Electronic Notes in Theoretical Computer Science 103, Elsevier 2004 [contents]
Informal and Other Publications
- 2022
- [i10]Luca Arnaboldi, David Aspinall:
Towards Interdependent Safety Security Assessments using Bowties. CoRR abs/2208.03484 (2022) - 2020
- [i9]Henry Clausen, Robert Flood, David Aspinall:
Traffic Generation using Containerization for Machine Learning. CoRR abs/2011.06350 (2020) - 2019
- [i8]David Butler, Andreas Lochbihler, David Aspinall, Adrià Gascón:
Formalising Σ-Protocols and Commitment Schemes using CryptHOL. IACR Cryptol. ePrint Arch. 2019: 1185 (2019) - [i7]David Butler, David Aspinall, Adrià Gascón:
Formalising Oblivious Transfer in the Semi-Honest and Malicious Model in CryptHOL. IACR Cryptol. ePrint Arch. 2019: 1449 (2019) - 2018
- [i6]David Butler, David Aspinall, Adrià Gascón:
How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation. CoRR abs/1805.12482 (2018) - 2016
- [i5]Mohamed Nassim Seghir, David Aspinall:
DroidGen: Constraint-based and Data-Driven Policy Generation for Android. CoRR abs/1612.07586 (2016) - 2015
- [i4]Bela Gor, David Aspinall:
Accessible Banking: Experiences and Future Directions. CoRR abs/1507.04578 (2015) - 2014
- [i3]Steven Obua, Jacques D. Fleuriot, Phil Scott, David Aspinall:
ProofPeer: Collaborative Theorem Proving. CoRR abs/1404.6186 (2014) - [i2]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 abs/1410.7743 (2014) - 2013
- [i1]Steven Obua, Mark Adams, David Aspinall:
Capturing Hiproofs in HOL Light. CoRR abs/1307.2713 (2013)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-09-10 02:10 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
