Prof Richard Bornat


NameProf Richard Bornat
Job titleProfessor
Research institute
Primary appointmentComputer Science
Email addressrichard110@mdx.ac.uk
ORCIDhttps://orcid.org/0000-0002-7261-0233
Contact categoryAcademic staff (past)

Research outputs

Describing and simulating concurrent quantum systems

Bornat, R., Boender, J., Kammueller, F., Poly, G. and Nagarajan, R. 2020. Describing and simulating concurrent quantum systems. Biere, A. and Parker, D. (ed.) International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 20). Dublin 27 - 30 Apr 2020 Springer. pp. 271-277 https://doi.org/10.1007/978-3-030-45237-7_16

New lace and arsenic: adventures in weak memory with a program logic (v2)

Bornat, R., Alglave, J. and Parkinson, M. 2016. New lace and arsenic: adventures in weak memory with a program logic (v2). https://doi.org/10.48550/arXiv.1512.01416

Cyclic proofs of program termination in separation logic

Brotherston, J., Bornat, R. and Calcagno, C. 2008. Cyclic proofs of program termination in separation logic. ACM SIGPLAN Notices. 43 (1), pp. 101-112. https://doi.org/10.1145/1328897.1328453

Explanation of two non-blocking shared-variable communication algorithms

Bornat, R. and Amjad, H. 2011. Explanation of two non-blocking shared-variable communication algorithms. Formal Aspects of Computing. https://doi.org/10.1007/s00165-011-0213-4

Separation logic and concurrency

Bornat, R. 2010. Separation logic and concurrency. in: Boca, P., Bowen, J. and Siddiqi, J. (ed.) Formal Methods: State of the Art and New Directions London Springer Verlag. pp. 217-248

Inter-process buffers in separation logic with rely-guarantee

Bornat, R. and Amjad, H. 2010. Inter-process buffers in separation logic with rely-guarantee. Formal Aspects of Computing. 22 (6), pp. 735-772. https://doi.org/10.1007/s00165-009-0141-8

Towards automatic stability analysis for rely-guarantee proofs

Amjad, H. and Bornat, R. 2009. Towards automatic stability analysis for rely-guarantee proofs. in: Jones, N. and Müller-Olm, M. (ed.) Verification, model checking, and abstract interpretation: 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings Springer.

Modular verification of a non-blocking stack.

Bornat, R., Parkinson, M. and O'Hearn, P. 2007. Modular verification of a non-blocking stack. 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '07), Nice, France. Proceedings.. https://doi.org/10.1145/1190216.1190261

Variables as resource in Hoare logic.

Bornat, R., Calcagno, C. and Parkinson, M. 2006. Variables as resource in Hoare logic. in: 21st Annual IEEE Symposium on Logic in Computer Science (LICS 2006), Seattle, Washington. Proceedings. IEEE Computer Society. pp. 137-146

Variables as resources in separation logic

Bornat, R., Calcagno, C. and Yang, H. 2006. Variables as resources in separation logic. Electronic Notes in Theoretical Computer Science. 155, pp. 247-276. https://doi.org/10.1016/j.entcs.2005.11.059

Permission accounting in separation logic.

Bornat, R., Calcagno, C., Parkinson, M. and O'Hearn, P. 2005. Permission accounting in separation logic. 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '05), Long Beach, California, USA. Proceedings. https://doi.org/10.1145/1047659.1040327
  • 1151
    total views of outputs
  • 103
    total downloads of outputs
  • 15
    views of outputs this month
  • 0
    downloads of outputs this month