Accepting PhD Students

PhD projects

Please see the Informatics Security and Privacy group page for projects including some of mine: <a href="http://web.inf.ed.ac.uk/security-privacy/phd-study/phd-topics">S and P PhD topics</a>

Please contact me directly for topics in other areas.

If you made any changes in Pure these will be visible here soon.
Filter
Conference contribution

Search results

  • 1995

    Subtyping with singleton types

    Aspinall, D., 1995, Computer Science Logic: 8th Workshop, CSL '94 Kazimierz, Poland, September 25–30, 1994 Selected Papers. Pacholski, L. & Tiuryn, J. (eds.). Springer Berlin Heidelberg, Vol. 933. p. 1-15 15 p. (Lecture Notes in Computer Science; vol. 933).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Types, subtypes, and ASL+

    Aspinall, D., 1995, 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 – June 3, 1994 Selected Papers. Astesiano, E., Reggio, G. & Tarlecki, A. (eds.). Springer Berlin Heidelberg, Vol. 906. p. 116-131 16 p. (Lecture Notes in Computer Science; vol. 906).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 1996

    Subtyping dependent types (Summary)

    Aspinall, D. & Compagnoni, A., 1996, LICS '96. Proceedings., Eleventh Annual IEEE Symposium on Logic in Computer Science, 1996. Institute of Electrical and Electronics Engineers (IEEE), p. 86-97 10 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2000

    Protocols for Interactive e-Proof

    Aspinall, D., Jul 2000, Supplemental proceedings of the 13th international conference on theorem proving in higher order logics (TPHOLs 2000). p. 25-32 8 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Proof General: A Generic Tool for Proof Development

    Aspinall, D., 2000, Tools and Algorithms for the Construction and Analysis of Systems: 6th International Conference, TACAS 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000 Berlin, Germany, March 25 – April 2, 2000 Proceedings. Graf, S. & Schwartzbach, M. (eds.). Springer Berlin Heidelberg, Vol. 1785. p. 38-43 6 p. (Lecture Notes in Computer Science; vol. 1785).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Subtyping with Power Types

    Aspinall, D., 2000, Computer Science Logic: 14th Annual Conference of the EACSL, Fischbachau, Germany, August 21-26, 2000, Proceedings. Springer Berlin Heidelberg, p. 156-171 16 p. (Lecture Notes in Computer Science; vol. 1862).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2002

    Another Type System for In-Place Update

    Aspinall, D. & Hofmann, M., 2002, Programming Languages and Systems: 11th European Symposium on Programming, ESOP 2002 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8–12, 2002 Proceedings. Le Métayer, D. (ed.). Springer Berlin Heidelberg, Vol. 2305. p. 36-52 17 p. (Lecture Notes in Computer Science; vol. 2305).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • From Specifications to Code in Casl

    Aspinall, D. & Sannella, D., 2002, Algebraic Methodology and Software Technology: 9th International Conference, AMAST 2002 Saint-Gilles-les-Bains, Reunion Island, France September 9–13, 2002 Proceedings. Kirchner, H. & Ringeissen, C. (eds.). Springer Berlin Heidelberg, Vol. 2422. p. 1-14 14 p. (Lecture Notes in Computer Science; vol. 2422).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Type Checking Parametrised Programs and Specifications in ASL+_FPC

    Aspinall, D., 2002, Recent Trends in Algebraic Development Techniques: 16th International Workshop, WADT 2002, Frauenchiemsee, Germany, September 24-27, 2002, Revised Selected Papers. Springer Berlin Heidelberg, p. 129-144 16 p. (Lecture Notes in Computer Science; vol. 2755).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2004

    A Program Logic for Resource Verification

    Aspinall, D., Beringer, L., Hofmann, M., Loidl, H-W. & Momigliano, A., 2004, Theorem Proving in Higher Order Logics: 17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004. Proceedings. Slind, K., Bunker, A. & Gopalakrishnan, G. (eds.). Springer Berlin Heidelberg, Vol. 3223. p. 34-49 16 p. (Lecture Notes in Computer Science; vol. 3223).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2005

    Mobile Resource Guarantees (Project Evaluation Paper)

    Sannella, D., Hofmann, M., Aspinall, D., Gilmore, S., Stark, I., Beringer, L., Loidl, H-W., MacKenzie, K., Momigliano, A. & Shkaravska, O., 2005, 6th Symposium on Trends in Functional Programming TFP 2005. Institute of Cybernetics, p. 7-16 10 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Mobile Resource Guarantees for Smart Devices

    Aspinall, D., Gilmore, S., Hofmann, M., Sannella, D. & Stark, I., 2005, Construction and Analysis of Safe, Secure, and Interoperable Smart Devices: International Workshop, CASSIS 2004, Marseille, France, March 10-14, 2004, Revised Selected Papers. Barthe, G., Burdy, L., Huisman, M., Lanet, J-L. & Muntean, T. (eds.). Berlin: Springer-Verlag GmbH, Vol. 3362. p. 1-26 26 p. (Lecture Notes in Computer Science; vol. 3362).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • Parsing, editing, proving: The PGIP display protocol

    Aspinall, D., Lüth, C. & Winterstein, D., 2005, International Workshop on User Interfaces for Theorem Provers. Vol. 2005.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    File
  • Proof General/Eclipse: A Generic Interface for Interactive Proof

    Aspinall, D., Lüth, C. & Winterstein, D., 2005, Proceedings of the 19th International Joint Conference on Artificial Intelligence. San Francisco, CA, USA: Morgan Kaufmann Publishers Inc., p. 1587-1588 2 p. (IJCAI'05).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • 2006

    Assisted Proof Document Authoring

    Aspinall, D., Lüth, C. & Wolff, B., 2006, Mathematical Knowledge Management: 4th International Conference, MKM 2005, Bremen, Germany, July 15-17, 2005, Revised Selected Papers. Kohlhase, M. (ed.). Springer Berlin Heidelberg, p. 65-80 16 p. (Lecture Notes in Computer Science; vol. 3863).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Mobile Resource Guarantees and Policies

    Aspinall, D. & MacKenzie, K., 2006, Mobile Resource Guarantees and Policies: Construction and Analysis of Safe, Secure, and Interoperable Smart Devices. Barthe, G., Grégoire, B., Huisman, M. & Lanet, J-L. (eds.). Springer Berlin Heidelberg, p. 16-36 21 p. (Lecture Notes in Computer Science; vol. 3956).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • PG Tips: A Recommender System for an Interactive Theorem Prover

    Mercer, A. E., Bundy, A., Duncan, H. & Aspinall, D., 2006, Proceedings of Mathematical User-Interfaces Workshop (MathUI’2006). p. 1-8 8 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • Proof General in Eclipse: System and Architecture Overview

    Aspinall, D., Winterstein, D., Lüth, C. & Fayyaz, A., 2006, eclipse '06 Proceedings of the 2006 OOPSLA workshop on eclipse technology eXchange. New York, NY, USA: ACM, p. 45-49 5 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2007

    A Framework for Interactive Proof

    Aspinall, D., Lüth, C. & Winterstein, D., 2007, Towards Mechanized Mathematical Assistants: 14th Symposium, Calculemus 2007, 6th International Conference, MKM 2007, Hagenberg, Austria, June 27-30, 2007. Proceedings. Kauers, M., Kerber, M., Miner, R. & Windsteiger, W. (eds.). Springer Berlin Heidelberg, p. 161-175 15 p. (Lecture Notes in Computer Science; vol. 4573).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Datatypes in Memory

    Aspinall, D. & Hoffman, P., 2007, Proceedings of the 2nd International Conference on Algebra and Coalgebra in Computer Science. Berlin, Heidelberg: Springer-Verlag, p. 111-125 15 p. (CALCO'07).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Formalising Java’s Data Race Free Guarantee

    Aspinall, D. & Ševčík, J., 2007, Theorem Proving in Higher Order Logics: 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007. Proceedings. Schneider, K. & Brandt, J. (eds.). Springer Berlin Heidelberg, p. 22-37 16 p. (Lecture Notes in Computer Science; vol. 4732).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Isabelle with Proof General Eclipse: An Overview and User Introduction

    Aspinall, D. & Lüth, C., 2007, CADE-21 The 21st Conference on Automated Deduction : The Isabelle Workshop 2007. p. 38 1 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Java Memory Model Examples: Good, Bad and Ugly

    Aspinall, D. & Ševčík, J., 2007, Proceedings of Verification and Analysis of Multi-Threaded Java-Like Programs (VAMP 2007). 15 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • Mobile Resource Guarantees

    Sannella, D., Hofmann, M., Aspinall, D., Gilmore, S., Stark, I., Beringer, L., Loidl, H-W., MacKenzie, K., Momigliano, A. & Shkaravska, O., 2007, Trends in Functional Programming. Intellect Books, Vol. 6. p. 211-226 16 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • 2008

    Monitoring External Resources in Java MIDP

    Aspinall, D., Maier, P. & Stark, I., 21 Feb 2008, Proceedings of the First International Workshop on Run Time Enforcement for Mobile and Distributed Systems (REM 2007). Vol. 197. p. 17-30 14 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • A Tactic Language for Hiproofs

    Aspinall, D., Denney, E. & Lüth, C., 2008, Intelligent Computer Mathematics, 9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings.: Lecture Notes in Computer Science. Springer Berlin Heidelberg, Vol. 5144. p. 339-354 16 p. (Lecture Notes in Computer Scince; vol. 5144).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • On Validity of Program Transformations in the Java Memory Model

    Sevcik, J. & Aspinall, D., 2008, ECOOP 2008 — Object-Oriented Programming. Vitek, J. (ed.). Springer-Verlag GmbH, p. 27-51 25 p. (Lecture Notes in Computer Science; vol. 5142).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Safety Guarantees from Explicit Resource Management

    Aspinall, D., Maier, P. & Stark, I., 2008, Formal Methods for Components and Objects. de Boer, F., Bonsangue, M., Graf, S. & de Roever, W-P. (eds.). Springer-Verlag GmbH, Vol. 5382. p. 52-71 20 p. (Lecture Notes in Computer Science).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2009

    Towards Merging PlatΩ and PGIP

    Aspinall, D., 9 Jan 2009, Proceedings of the 8th International Workshop on User Interfaces for Theorem Provers (UITP 2008). p. 3-21 18 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • Personal choice and challenge questions: a security and usability assessment

    Just, M. & Aspinall, D., 2009, Proceedings of the 5th Symposium on Usable Privacy and Security. New York, NY, USA: ACM, p. 8:1-8:11 11 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Towards a Type System for Security APIs

    Keighren, G., Aspinall, D. & Steel, G., 2009, Foundations and Applications of Security Analysis: Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security, ARSPA-WITS 2009, York, UK, March 28-29, 2009, Revised Selected Papers. Degano, P. & Viganò, L. (eds.). Springer Berlin Heidelberg, p. 173-192 20 p. (Lecture Notes in Computer Science; vol. 5511).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • 2010

    Symbolic and Analytic Techniques for Resource Analysis of Java Bytecode

    Aspinall, D., Atkey, R., MacKenzie, K. & Sannella, D., 2010, Trustworthly Global Computing: 5th International Symposium, TGC 2010, Munich, Germany, February 24-26, 2010, Revised Selected Papers. Wirsing, M., Hofmann, M. & Rauschmayer, A. (eds.). Springer-Verlag GmbH, p. 1-22 22 p. (Lecture Notes in Computer Science; vol. 6084).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • 2011

    Probing Attacks on Multi-agent Systems from Electronic Institutions

    Bijani, S., Robertson, D. & Aspinall, D., 2011, Declarative Agent Languages and Technologies IX: 9th International Workshop, DALT 2011, Taipei, Taiwan, May 3, 2011, Revised Selected and Invited Papers. Springer-Verlag GmbH, p. 33-50 18 p. (Lecture Notes in Computer Science; vol. 7169).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Towards Formal Proof Script Refactoring

    Whiteside, I., Aspinall, D., Dixon, L. & Grov, G., 2011, Intelligent Computer Mathematics: 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011. Proceedings. Davenport, J., Farmer, W., Urban, J. & Rabe, F. (eds.). Springer Berlin Heidelberg, p. 260-275 16 p. (Lecture Notes in Computer Science; vol. 6824).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • 2012

    Recording and Refactoring HOL Light Tactic Proofs

    Adams, M. & Aspinall, D., Jun 2012, Proceedings of the IJCAR workshop on Automated Theory Exploration. 6 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • An essence of SSReflect

    Whiteside, I., Aspinall, D. & Grov, G., 1 Jan 2012, Intelligent Computer Mathematics: 11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012. Proceedings. Springer-Verlag GmbH, p. 186-201 16 p. (Lecture Notes in Computer Science; vol. 7362).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

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

    Just, M. & Aspinall, D., 1 Jan 2012, 2012 International Conference for Internet Technology and Secured Transactions, ICITST 2012. p. 259-264 6 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Querying Proofs

    Aspinall, D., Denney, E. & Lüth, C., 2012, Logic for Programming, Artificial Intelligence, and Reasoning: 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings. Bjørner, N. & Voronkov, A. (eds.). Springer-Verlag GmbH, p. 92-106 15 p. (Lecture Notes in Computer Science; vol. 7180).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2013

    A Semantic Basis for Proof Queries and Transformations

    Aspinall, D., Denney, E. & Lüth, C., 2013, Logic for Programming, Artificial Intelligence, and Reasoning: 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings. McMillan, K., Middeldorp, A. & Voronkov, A. (eds.). Springer Berlin Heidelberg, p. 53-70 18 p. (Lecture Notes in Computer Science; vol. 8312).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Capturing Hiproofs in HOL Light

    Obua, S., Adams, M. & Aspinall, D., 2013, Intelligent Computer Mathematics: Proceedings MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Springer Berlin Heidelberg, p. 184-199 16 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

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

    Aspinall, D. & Just, M., 2013, Financial Cryptography and Data Security: 17th International Conference, FC 2013, Okinawa, Japan, April 1-5, 2013, Revised Selected Papers. Sadeghi, A-R. (ed.). Springer-Verlag GmbH, p. 126-143 18 p. (Lecture Notes in Computer Science; vol. 7859).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • Polar: A Framework for Proof Refactoring

    Dietrich, D., Whiteside, I. & Aspinall, D., 2013, Logic for Programming, Artificial Intelligence, and Reasoning. McMillan, K., Middeldorp, A. & Voronkov, A. (eds.). Springer Berlin Heidelberg, Vol. 8312. p. 776-791 16 p. (Lecture Notes in Computer Science; vol. 8312).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2014

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

    Kayacik, H. G., Just, M., Baillie, L., Aspinall, D. & Micallef, N., 2014, Proceedings of the Third Workshop on Mobile Security Technologies (MoST) 2014. ArXiv, 10 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • Towards an amortized type system for JavaScript

    Franzen, D. & Aspinall, D., 2014, 6th International Symposium on Symbolic Computation in Software Science, SCSS 2014, Gammarth, La Marsa, Tunisia, December 7-8, 2014. p. 12-26 15 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Towards an Authorization Framework for App Security Checking

    Hallett, J. & Aspinall, D., 2014, Proceedings of the 2014 ESSoS Doctoral Symposium co-located with the International Symposium on Engineering Secure Software and Systems (ESSoS 2014), Munich, Germany, February 26, 2014.. 6 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • 2015

    Verifying Anti-Security Policies Learnt from Android Malware Families

    Chen, W., Sutton, C., Aspinall, D., Gordon, A., Shen, Q. & Muttik, I., 21 Oct 2015, Fourth International Seminar on Program Verification, Automated Debugging and Symbolic Computation. 6 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • Compact Explanations of Why Malware is Bad

    Chen, W., Sutton, C., Gordon, A., Aspinall, D., Muttik, I. & Shen, Q., 10 Aug 2015, (Accepted/In press) AI4FM 2015. 4 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • Type Inference for ZFH

    Obua, S., Fleuriot, J., Scott, P. & Aspinall, D., 18 Jul 2015, Intelligent Computer Mathematics : International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings. Springer International Publishing, p. 87-101 15 p. (Lecture Notes in Computer Science; vol. 9150).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • Security testing for Android mHealth apps

    Knorr, K. & Aspinall, D., Apr 2015, Software Testing, Verification and Validation Workshops (ICSTW), 2015 IEEE Eighth International Conference on. Institute of Electrical and Electronics Engineers (IEEE), p. 1-8 8 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Accessible Banking: Experiences and Future Directions

    Gor, B. & Aspinall, D., 2015, Workshop on Inclusive Privacy and Security (WIPS): Privacy and Security for Everyone, Anytime, Anywhere, held as part of Symposium on Usable Privacy and Security (SOUPS) 2015. 3 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File