# David Aspinall

According to our database

Collaborative distances:

^{1}, David Aspinall authored at least 74 papers between 1994 and 2018.Collaborative distances:

## Timeline

#### Legend:

Book In proceedings Article PhD thesis Other## Links

#### Homepages:

#### On csauthors.net:

## Bibliography

2018

Foreword.

Theor. Comput. Sci., 2018

Secure information sharing in social agent interactions using information flow analysis.

Eng. Appl. of AI, 2018

How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation.

CoRR, 2018

Formal Analysis of Sneak-Peek: A Data Centre Attack and Its Mitigations.

Proceedings of the ICT Systems Security and Privacy Protection, 2018

2017

Capturing Policies for BYOD.

Proceedings of the ICT Systems Security and Privacy Protection, 2017

How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation.

Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

2016

DroidGen: Constraint-based and Data-Driven Policy Generation for Android.

CoRR, 2016

More Semantics More Robust: Improving Android Malware Classifiers.

Proceedings of the 9th ACM Conference on Security & Privacy in Wireless and Mobile Networks, 2016

Certified Lightweight Contextual Policies for Android.

Proceedings of the IEEE Cybersecurity Development, 2016

What's in a Theorem Name?

Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

On Robust Malware Classifiers by Verifying Unwanted Behaviours.

Proceedings of the Integrated Formal Methods - 12th International Conference, 2016

Towards Formal Proof Metrics.

Proceedings of the Fundamental Approaches to Software Engineering, 2016

A text-mining approach to explain unwanted behaviours.

Proceedings of the 9th European Workshop on System Security, 2016

AppPAL for Android - Capturing and Checking Mobile App Policies.

Proceedings of the Engineering Secure Software and Systems - 8th International Symposium, 2016

PhoneWrap - Injecting the "How Often" into Mobile Apps.

Proceedings of the 1st International Workshop on Innovations in Mobile Privacy and Security, 2016

Explaining Unwanted Behaviours in Context.

Proceedings of the 1st International Workshop on Innovations in Mobile Privacy and Security, 2016

POSTER: Weighing in eHealth Security.

Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, 2016

2015

Accessible Banking: Experiences and Future Directions.

CoRR, 2015

On the Privacy, Security and Safety of Blood Pressure and Diabetes Apps.

Proceedings of the ICT Systems Security and Privacy Protection, 2015

Sensor use and usefulness: Trade-offs for data-driven authentication on mobile devices.

Proceedings of the 2015 IEEE International Conference on Pervasive Computing and Communications, 2015

Type Inference for ZFH.

Proceedings of the Intelligent Computer Mathematics - International Conference, 2015

Security testing for Android mHealth apps.

Proceedings of the Eighth IEEE International Conference on Software Testing, 2015

EviCheck: Digital Evidence for Android.

Proceedings of the Automated Technology for Verification and Analysis, 2015

2014

ProofPeer: Collaborative Theorem Proving.

CoRR, 2014

Data Driven Authentication: On the Effectiveness of User Behaviour Modelling with Mobile Device Sensors.

CoRR, 2014

Towards an amortized type system for JavaScript.

Proceedings of the 6th International Symposium on Symbolic Computation in Software Science, 2014

Towards an Authorization Framework for App Security Checking.

Proceedings of the 2014 ESSoS Doctoral Symposium co-located with the International Symposium on Engineering Secure Software and Systems (ESSoS 2014), 2014

2013

Capturing Hiproofs in HOL Light.

CoRR, 2013

Capturing Hiproofs in HOL Light.

Proceedings of the Intelligent Computer Mathematics, 2013

Polar: A Framework for Proof Refactoring.

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

A Semantic Basis for Proof Queries and Transformations.

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

"Give Me Letters 2, 3 and 6!": Partial Password Implementations and Attacks.

Proceedings of the Financial Cryptography and Data Security, 2013

2012

Preface.

Electr. Notes Theor. Comput. Sci., 2012

Querying Proofs.

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

On the security and usability of dual credential authentication in UK online banking.

Proceedings of the 7th International Conference for Internet Technology and Secured Transactions, 2012

An Essence of SSReflect.

Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2012

2011

Towards Formal Proof Script Refactoring.

Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

Probing Attacks on Multi-Agent Systems Using Electronic Institutions.

Proceedings of the Declarative Agent Languages and Technologies IX, 2011

2010

Tactics for Hierarchical Proof.

Mathematics in Computer Science, 2010

Symbolic and Analytic Techniques for Resource Analysis of Java Bytecode.

Proceedings of the Trustworthly Global Computing - 5th International Symposium, 2010

2009

Towards Merging PlatOmega and PGIP.

Electr. Notes Theor. Comput. Sci., 2009

Personal choice and challenge questions: a security and usability assessment.

Proceedings of the 5th Symposium on Usable Privacy and Security, 2009

Towards a Type System for Security APIs.

Proceedings of the Foundations and Applications of Security Analysis, 2009

2008

A type system with usage aspects.

J. Funct. Program., 2008

Monitoring External Resources in Java MIDP.

Electr. Notes Theor. Comput. Sci., 2008

On Validity of Program Transformations in the Java Memory Model.

Proceedings of the ECOOP 2008, 2008

A Tactic Language for Hiproofs.

Proceedings of the Intelligent Computer Mathematics, 9th International Conference, 2008

2007

A program logic for resources.

Theor. Comput. Sci., 2007

Special Issue on User Interfaces in Theorem Proving: Preface.

J. Autom. Reasoning, 2007

Optimisation Validation.

Electr. Notes Theor. Comput. Sci., 2007

Formalising Java's Data Race Free Guarantee.

Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

A Framework for Interactive Proof.

Proceedings of the Towards Mechanized Mathematical Assistants, 14th Symposium, 2007

Safety Guarantees from Explicit Resource Management.

Proceedings of the Formal Methods for Components and Objects, 6th International Symposium, 2007

Datatypes in Memory.

Proceedings of the Algebra and Coalgebra in Computer Science, 2007

2006

Proof general in Eclipse: system and architecture overview.

Proceedings of the 2006 OOPSLA workshop on Eclipse Technology eXchange, 2006

2005

Mobile Resource Guarantees (project evaluation paper).

Proceedings of the Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, 2005

Assisted Proof Document Authoring.

Proceedings of the Mathematical Knowledge Management, 4th International Conference, 2005

Proof General / Eclipse: A Generic Interface for Interactive Proof.

Proceedings of the IJCAI-05, Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, Edinburgh, Scotland, UK, July 30, 2005

Mobile Resource Guarantees and Policies.

Proceedings of the Construction and Analysis of Safe, 2005

2004

Proof General meets IsaWin: Combining Text-Based And Graphical User Interfaces.

Electr. Notes Theor. Comput. Sci., 2004

Preface.

Electr. Notes Theor. Comput. Sci., 2004

A Program Logic for Resource Verification.

Proceedings of the Theorem Proving in Higher Order Logics, 17th International Conference, 2004

Mobile Resource Guarantees for Smart Devices.

Proceedings of the Construction and Analysis of Safe, 2004

2003

Heap-Bounded Assembly Language.

J. Autom. Reasoning, 2003

2002

Type Checking Parametrised Programs and Specifications in ASL+

_{FPC}.
Proceedings of the Recent Trends in Algebraic Development Techniques, 2002

Another Type System for In-Place Update.

Proceedings of the Programming Languages and Systems, 2002

From Specifications to Code in CASL.

Proceedings of the Algebraic Methodology and Software Technology, 2002

2001

Subtyping dependent types.

Theor. Comput. Sci., 2001

2000

Proof General: A Generic Tool for Proof Development.

Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 2000

Subtyping with Power Types.

Proceedings of the Computer Science Logic, 2000

1997

Type systems for modular programs and specifications.

PhD thesis, 1997

1996

Subtyping Dependent Types (Summary).

Proceedings of the Proceedings, 1996

1994

Subtyping with Singleton Types.

Proceedings of the Computer Science Logic, 8th International Workshop, 1994

Types, Subtypes, and ASL+.

Proceedings of the Recent Trends in Data Type Specification, 10th Workshop on Specification of Abstract Data Types Joint with the 5th COMPASS Workshop, S. Margherita, Italy, May 30, 1994