David Aspinall
David Aspinall
Professor in Computer Science, University of Edinburgh
Verified email at
Cited by
Cited by
Proof General: A generic tool for proof development
D Aspinall
Tools and Algorithms for the Construction and Analysis of Systems: 6th …, 2000
On validity of program transformations in the Java memory model
J Ševčík, D Aspinall
European Conference on Object-Oriented Programming, 27-51, 2008
Personal choice and challenge questions: a security and usability assessment
M Just, D Aspinall
Proceedings of the 5th Symposium on Usable Privacy and Security, 1-11, 2009
Data driven authentication: On the effectiveness of user behaviour modelling with mobile device sensors
HG Kayacik, M Just, L Baillie, D Aspinall, N Micallef
arXiv preprint arXiv:1410.7743, 2014
Subtyping with singleton types
D Aspinall
International Workshop on Computer Science Logic, 1-15, 1994
Mobile resource guarantees for smart devices
D Aspinall, S Gilmore, M Hofmann, D Sannella, I Stark
Construction and Analysis of Safe, Secure, and Interoperable Smart Devices …, 2005
A program logic for resources
D Aspinall, L Beringer, M Hofmann, HW Loidl, A Momigliano
Theoretical Computer Science 389 (3), 411-445, 2007
Subtyping dependent types
D Aspinall, A Compagnoni
Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, 86-97, 1996
Formalising Java’s data race free guarantee
D Aspinall, J Ševčík
International Conference on Theorem Proving in Higher Order Logics, 22-37, 2007
Another type system for in-place update
D Aspinall, M Hofmann
European Symposium on Programming, 36-52, 2002
Security testing for Android mHealth apps
K Knorr, D Aspinall
2015 IEEE Eighth International Conference on Software Testing, Verification …, 2015
Subtyping dependent types
D Aspinall, A Compagnoni
Theoretical Computer Science 266 (1-2), 273-309, 2001
Heap-bounded assembly language
D Aspinall, A Compagnoni
Journal of automated reasoning 31, 261-302, 2003
Dependent types
D Aspinall, M Hofmann
Advanced topics in types and programming languages, 45-86, 2004
A program logic for resource verification
D Aspinall, L Beringer, M Hofmann, HW Loidl, A Momigliano
Theorem Proving in Higher Order Logics: 17th International Conference …, 2004
An IoT analysis framework: An investigation of IoT smart cameras' vulnerabilities
R Alharbi, D Aspinall
IET Digital Library, 2018
A framework for interactive proof
D Aspinall, C Lüth, D Winterstein
International Conference on Mathematical Knowledge Management, 161-175, 2007
Java memory model examples: Good, bad and ugly
D Aspinall, J Ševčík
Proceedings of Verification and Analysis of Multi-Threaded Java-Like …, 2007
On the privacy, security and safety of blood pressure and diabetes apps
K Knorr, D Aspinall, M Wolters
ICT Systems Security and Privacy Protection: 30th IFIP TC 11 International …, 2015
Towards formal proof script refactoring
I Whiteside, D Aspinall, L Dixon, G Grov
Intelligent Computer Mathematics: 18th Symposium, Calculemus 2011, and 10th …, 2011
The system can't perform the operation now. Try again later.
Articles 1–20