Prof Richard Bornat


NameProf Richard Bornat
Job titleProfessor
Research institute
Primary appointmentComputer Science
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). arXiv.org arXiv. 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 - POPL '08. 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. 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI), Birmingham, UK. Proceedings in Electronic Notes in Theoretical Computer Science. Elsevier B.V.. 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
  • 1
    total views of outputs
  • 0
    total downloads of outputs
  • 0
    views of outputs this month
  • 0
    downloads of outputs this month