Formal Analysis of Quantum Systems using Process Calculus

Timothy A.S. Davidson
(University of Warwick, UK)
Simon J. Gay
(University of Glasgow, UK)
Rajagopal Nagarajan
(University of Warwick, UK)

Quantum communication and cryptographic protocols are well on the way to becoming an important practical technology. Although a large amount of successful research has been done on proving their correctness, most of this work does not make use of familiar techniques from formal methods, such as formal logics for specification, formal modelling languages, separation of levels of abstraction, and compositional analysis. We argue that these techniques will be necessary for the analysis of large-scale systems that combine quantum and classical components, and summarize the results of initial investigation using behavioural equivalence in process calculus. This paper is a summary of Simon Gay's invited talk at ICE'11.

Invited Presentation in Alexandra Silva, Simon Bliudze, Roberto Bruni and Marco Carbone: Proceedings Fourth Interaction and Concurrency Experience (ICE 2011), Reykjavik, Iceland, 9th June 2011, Electronic Proceedings in Theoretical Computer Science 59, pp. 104–110.
Published: 31st July 2011.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: