David Aspinall
David Aspinall
Professor in Computer Science, University of Edinburgh
Verified email at ed.ac.uk
Title
Cited by
Cited by
Year
Proof General: A generic tool for proof development
D Aspinall
International Conference on Tools and Algorithms for the Construction and …, 2000
2042000
On validity of program transformations in the Java memory model
J Ševčík, D Aspinall
European Conference on Object-Oriented Programming, 27-51, 2008
1752008
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
1262009
Subtyping with singleton types
D Aspinall
International Workshop on Computer Science Logic, 1-15, 1994
881994
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
812014
Formalising Java’s data race free guarantee
D Aspinall, J Ševčík
International Conference on Theorem Proving in Higher Order Logics, 22-37, 2007
812007
Mobile resource guarantees for smart devices
D Aspinall, S Gilmore, M Hofmann, D Sannella, I Stark
International Workshop on Construction and Analysis of Safe, Secure, and …, 2004
812004
Subtyping dependent types
D Aspinall, A Compagnoni
Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, 86-97, 1996
801996
A program logic for resources
D Aspinall, L Beringer, M Hofmann, HW Loidl, A Momigliano
Elsevier 399 (3), 411-445, 2007
712007
Another type system for in-place update
D Aspinall, M Hofmann
European Symposium on Programming, 36-52, 2002
682002
Subtyping dependent types
D Aspinall, A Compagnoni
Theoretical Computer Science 266 (1), 273-309, 2001
552001
Heap-bounded assembly language
D Aspinall, A Compagnoni
Journal of automated reasoning 31 (3-4), 261-302, 2003
502003
Dependent types
D Aspinall, M Hofmann
Advanced Topics in Types and Programming Languages, 45-86, 2005
462005
A framework for interactive proof
D Aspinall, C Lüth, D Winterstein
Towards Mechanized Mathematical Assistants, 161-175, 2007
442007
A program logic for resource verification
D Aspinall, L Beringer, M Hofmann, HW Loidl, A Momigliano
International Conference on Theorem Proving in Higher Order Logics, 34-49, 2004
442004
Java memory model examples: Good, bad and ugly
D Aspinall, J Sevcik
Proc. of VAMP 7, 2007
402007
Security testing for Android mHealth apps
K Knorr, D Aspinall
2015 IEEE Eighth International Conference on Software Testing, Verification …, 2015
342015
Towards formal proof script refactoring
I Whiteside, D Aspinall, L Dixon, G Grov
International Conference on Intelligent Computer Mathematics, 260-275, 2011
312011
Mobile resource guarantees and policies
D Aspinall, K MacKenzie
International Workshop on Construction and Analysis of Safe, Secure, and …, 2005
302005
Type systems for modular programs and specifications
DR Aspinall
University of Edinburgh, 1997
281997
The system can't perform the operation now. Try again later.
Articles 1–20