Dr Nick Papanikolaou, HP Labs
Welcome!
You are now looking at Nick Papanikolaou's personal webpage. The purpose of the site is to provide information on Nick's professional activities and research.
Nick is a Research Scientist in the Cloud and Security Lab at Hewlett-Packard Laboratories
(HP Labs), Bristol. He is currently involved in Future Internet Research in the areas of accountability, trust and security, particularly in cloud computing environments.
Previously, Nick was Research Fellow in the e-Security Group at the International Digital Laboratory within the
University of Warwick (part of the WMG institute), working in collaboration with Sadie Creese and Michael Goldsmith. In that role he worked on mathematical models of privacy, specification languages and models of policies, and design and verification of security protocols as part of the project EnCoRe ("Ensuring Consent and Revocation"). During his doctorate, he was employed on a part-time basis by Resource Development International
(RDI), as "Pathway Leader" and Tutor for the HND/C Computing (Business IT) distance learning course, and Tutor for the BA in Business IT Topup course. RDI provides these programmes to business clients and independent students. Nick studied computer science at the University of Warwick, completing a BSc
(Hons) in Computer Systems Engineering, an MSc by Research, and a PhD in Computer Science. His doctorate was supervised by Rajagopal Nagarajan.
Nick is a member of the Association for Computing Machinery
(ACM), the Institute for Electrical and Electronic Engineers
(IEEE) and the European Research Consortium for Informatics and Mathematics
(ERCIM). He is a member of the ACM Special Interest Group on Algorithms and Computation Theory
(SIGACT), the ACM Special Interest Group on Programming Languages
(SIGPLAN), the
IEEE Computer Society and the European Association for Theoretical Computer Science
(EATCS).
He actively presents research at workshops and conferences in theoretical computer science and computer security and has served on various programme committees; Nick was also on the organising committee of the Fifth Workshop on Automated Verification of Critical Systems
(AVoCS'05). Nick has received two awards:
- Computer Systems Engineering Project Prize, Department of Computer Science, University of Warwick, 2003.
- Best Presentation Award, WPCCS'06 (Warwick Postgraduate Colloquium on Computer Science), Department of Computer Science, University of Warwick, 2006.
At the University of Warwick, Nick was a teaching assistant for several course modules in the Department of Computer Science, including among others the courses CS134 (Introduction to Computer Security), CS238 (Concurrent Processes) and CS406 (Research Directions in Computing).
As of March 2011, Nick is a trained and Certified ScrumMaster
and Member of the Scrum Alliance. In May 2011 he was granted the honorary title of Associate Fellow by the
Department of Computer Science at the
University of Warwick. In 2012 Nick was named
Visiting Lecturer at the Waterford Institute of Technology in Ireland, and he serves on the Interest Group Panel of the ENDORSE research project.
Current Research
Interests:
- cloud security and privacy
- policy formalisation and enforcement
- natural language processing, applied AI
- model checking and process algebra
- quantum cryptography
Some Past Results and Contributions:
-
Design of languages, logics and tools for protocol specification and verification
- In joint work with Paulo Mateus and Pedro Baltazar (IST Lisbon), Nick helped to develop EpCTL, a probabilistic temporal logic that uses EPPL (exogenous probabilistic propositional logic) as its core.
-
Model checking
- In collaboration with Rajagopal Nagarajan and Simon Gay Nick developed a model checker, QMC, for the analysis of properties of quantum communication and quantum cryptographic protocols. QMC is the first of its kind to our knowledge. Earlier work has included the use of a classical, probabilistic model checker for the analysis of similar protocols. This work combined classical verification techniques and models with the mathematics of quantum computing and quantum information, so this is clearly interdisciplinary.
-
Syntax and semantics of languages for quantum programming
- Nick's undergraduate final year project 'Formal Specification and Verification of Quantum Protocols' extended the work of
Simon Gay and Rajagopal Nagarajan on verifying the security of the BB84 protocol using classical process algebra and the probabilistic model checker PRISM. He was involved in the early stages of development of CQP
(Communicating Quantum Processes), a quantum process algebra with a formal semantics and type system. Nick developed a quantum specification language for use in conjunction with the QMC model checker; the language has an operational semantics and an implementation.
Current Students
I am currently supervising two MSc student projects at the University of Warwick, jointly with Siani Pearson. Both students are working on natural language processing tools and techniques for analysis of security and privacy policies.
Research Projects
Nick has been involved in the following research projects.
Press and Media Coverage of Nick's Research
- Nick was interviewed by the BBC for a technology article on the future of cryptography (title: "Tricking the perfect code machine"). Selected comments from the interview have been included in the article.
- Nick was interviewed on camera at the UK Cyber Security Challenge on his research and current role at HP Labs:
Programme Committee Memberships
Nick is currently serving on the programme committee for the following events:
Publications
For an alternative listing of publications see Nick's HP Labs page and also Nick's (not complete)
DBLP entries.
Link to Nick's latest HP Labs Technical Reports
Refereed Journal Papers and Chapters in Books
2012
- WAINWRIGHT, N., AND PAPANIKOLAOU, N. The FIA research roadmap: Priorities for future internet research. In F. Alvarez et al., Ed., Future Internet — From Technological Promises to Reality, Lecture Notes in Computer Science. Springer, 2012. To appear.
- DAVIDSON, T., GAY, S. J., MLNARIK, H., NAGARAJAN, R., AND PAPANIKOLAOU, N. Model checking for communicating quantum processes.
International Journal of Unconventional Computing 8, 1 (2012), 73–98.
- PAPANIKOLAOU, N., PEARSON, S., CASASSA MONT, M., BROWN, R., MCCORRY, K., SANDER, T., AND RAO., P. An online knowledge base store (KB store). Research Disclosure (February 2012), 114–115. ID 574026.
2011
2010
- ADETOYE, A. O., AND PAPANIKOLAOU, N. Static analysis of information release in interactive programs.
Electronic Communications of the EASST 35 (2010). [Preprint: pdf]
- GAY, S. J., NAGARAJAN, R., AND PAPANIKOLAOU, N.
Specification and verification of quantum protocols. In Semantic Techniques in Quantum Computation, S. Gay and I. Mackie, Eds. Cambridge University Press, 2010, ch. 11.
2009
- PAPANIKOLAOU, N. Security versus quantum computers. BCS Information Security Now
(ISNow) 4, 2 (2009), 6–7. [Online version]
2005
-
PAPANIKOLAOU, N.
An introduction to quantum cryptography. ACM Crossroads 11, 3 (2005), 10–16.
[Online version]
- PAPANIKOLAOU, N.
Reasoning formally about quantum systems: An overview. ACM SIGACT News 36, 3 (2005), 51–66. [Available as pdf] [Technical Report CS-RR-416] [arXiv version
- cs.LO/0508005: link]
Refereed Conference and Workshop Papers
2012
- WAINWRIGHT, N. AND PAPANIKOLAOU, N. Towards A Vision for Future Internet Research. Accepted for presentation at e-Challenges e-2012, Lisbon, Portugal, 17-19 October 2012.
- PAPANIKOLAOU, N., PEARSON, S., CASASSA MONT, M., AND KO, R.
Automating compliance for cloud computing services.
In Proceedings of the 2nd International Conference on Cloud Computing and Services Science (CLOSER 2012) (January 2012), SciTePress.
- CASASSA MONT, M., MCCORRY, K., PAPANIKOLAOU, N., AND PEARSON, S. Security and privacy governance in cloud computing via SLAs and a policy orchestration service. In Proceedings of the 2nd International Conference on Cloud Computing and Services Science (CLOSER 2012) (January 2012), SciTePress.
2011
- PAPANIKOLAOU, N., PEARSON, S., AND CASASSA MONT, M.
Towards natural-language understanding and automated enforcement of privacy rules and regulations in the cloud: Survey and bibliography. In Proceedings of 1st InternationalWorkshop on Security and Trust in Virtualised Environments (STAVE 2011) (2011).
- PAPANIKOLAOU, N., PEARSON, S., AND CASASSA MONT, M.
Automated understanding of cloud terms of service and SLAs. In Proceedings of IEEE CloudCom 2011 (Athens, Greece, November 29 - December 1 2011).
- PAPANIKOLAOU, N., PEARSON, S., AND CASASSA MONT, M.
Automated understanding of cloud terms of service and SLAs. In Proceedings of The 22nd Hewlett-Packard Colloquium on Information Security (Royal Holloway, University of London, December 2011).
2010
- AGRAFIOTIS, I., CREESE, S., GOLDSMITH, M., AND PAPANIKOLAOU, N. Applying formal methods to describe privacy control requirements in a real scenario: Emerging ambiguities and proposed solutions. In Proceedings of PrimeLife/IFIP Summer School 2010: Privacy and Identity Management for Life, Helsingborg, Sweden (August 2010).
- AGRAFIOTIS, I., CREESE, S., GOLDSMITH, M., PAPANIKOLAOU, N., CASASSA MONT, M., AND PEARSON, S. Defining consent and revocation policies. In Pre-Proceedings of PrimeLife/IFIP Summer School 2010: Privacy and Identity Management for Life (Helsingborg, Sweden, August 2010). [Available as
pdf]
- CASASSA MONT, M., PEARSON, S., CREESE, S., GOLDSMITH, M., AND PAPANIKOLAOU, N. EnCoRe: Towards a conceptual model for privacy policies. In Pre-Proceedings of PrimeLife/IFIP Summer School 2010: Privacy and Identity Management for Life (Helsingborg, Sweden, August 2010). [Available as
pdf]
- CASASSA MONT, M., PEARSON, S., CREESE, S., GOLDSMITH, M., AND PAPANIKOLAOU, N. A conceptual model for privacy policies with consent and revocation requirements. In Proceedings of PrimeLife/IFIP Summer School 2010: Privacy and Identity Management for Life (2010), Lecture Notes in Computer Science, Springer-Verlag.
- PAPANIKOLAOU, N., CREESE, S., GOLDSMITH, M., CASASSA MONT, M., AND PEARSON, S. EnCoRe: Towards a holistic approach to privacy.
In Proceedings of International Conference on Security and Cryptography (SECRYPT 2010) (Athens, Greece, July 2010). [Available as pdf]
2009
- AGRAFIOTIS, I., CREESE, S., GOLDSMITH, M., AND PAPANIKOLAOU, N. Reaching for informed revocation: Shutting off the tap on personal data. In Proceedings of Fifth International Summer School on Privacy and Identity Management for Life (Nice, France, September 2009). [Available as pdf]
- CASASSA MONT, M., PEARSON, S., CREESE, S., GOLDSMITH, M., AND PAPANIKOLAOU, N. Towards an integrated approach to the management, specification and enforcement of privacy policies. In Proceedings of W3C Workshop on Access Control Application Scenarios
(Abbaye de
Neumunster, Luxembourg, November 2009). [Available as pdf]
- PAPANIKOLAOU, N., CREESE, S., AND GOLDSMITH, M.
Policy refinement checking. In Proceedings of Ninth International Workshop on Automated Verification of Critical Systems
(AVoCS 09) (Swansea University, September 2009). [Available as pdf]
2008
- GAY, S., NAGARAJAN, R., AND PAPANIKOLAOU, N. QMC: A model checker for quantum systems. In Proceedings of 20th International Conference on Automated Verification (CAV 2008) (Princeton, NJ, USA, July 2008), vol. 5123 of Lecture Notes in Computer Science, Springer.
[Original version with case study source in appendix: pdf] [DOI
978-3-540-70545-1_51 (SpringerLink)] [Case study: casestudy.qmc] [The QMC tool is available below.]
2007
- BALTAZAR, P., MATEUS, P., NAGARAJAN, R., AND PAPANIKOLAOU, N. Exogenous probabilistic computation tree logic.
In Proceedings of the Fifth Workshop on Quantitative Aspects of Programming Languages (QAPL ’07) (Braga, Portugal, March 2007). [Available as pdf]
- GAY, S., NAGARAJAN, R., AND PAPANIKOLAOU, N. QMC: A model checker for quantum systems. In Proceedings of Workshop on Quantum Cryptography and Security (Lisbon Quantum Computation, Information and Logic Meetings Series: LQCIL’07) (Lisbon, Portugal, July 2007). [Preprint: pdf] [Extended Technical Report Version: arXiv:0704.3705] [Departmental Research Report
CS-RR-432]
2006
- GAY, S., NAGARAJAN, R., AND PAPANIKOLAOU, N.
Probabilistic model-checking of quantum protocols.
In Proceedings of 2nd International Workshop on Developments on Computational Models (DCM 2006) (San Servolo, Venice, Italy, July 2006). [Extended abstract: pdf] [Pre-proceedings version: pdf]
2005
- NAGARAJAN, R., PAPANIKOLAOU, N., BOWEN, G., AND GAY, S.
An automated analysis of the security of quantum key distribution. In Proceedings of the Third International Workshop on Security Issues in Concurrency (SECCO’05) (San Francisco, USA, August 2005). [Preprint:
pdf] [arXiv version - cs.CR/0502048:
link] [PRISM input files:
[qkdv2.pm.txt] [qkdv2.pctl] [qkdv3.pm.txt] [densecod2agentsimproved.pm] [densecod2agentsimproved.pctl] [newteleportationagents.pm] [newteleportationagents.pctl] [quantumerrorcorrection.pm] [quantumerrorcorrection.pctl]]
- NAGARAJAN, R., PAPANIKOLAOU, N., AND WILLIAMS, D.
Simulating and compiling code for the sequential quantum random access machine. In Proceedings of the Third International Workshop on Quantum Programming Languages (QPL 2005) (DePaul University, Chicago, USA, July 2005), vol. 170 of Electronic Notes in Theoretical Computer Science, pp. 101–124. [Preprint: pdf]
2004
- PAPANIKOLAOU, N. A programming language for quantum communication systems design. In Proceedings of the IEEE Postgraduate Research in Electronics, Photonics, Communications and Software Conference (PREP2004) (University of Hertfordshire, United Kingdom, 2004). [Abstract:
pdf]
Theses
- PAPANIKOLAOU, N. Model Checking Quantum Protocols. PhD thesis, Department of Computer Science, University of Warwick, 2009. [Available as pdf]
- PAPANIKOLAOU, N. Techniques for design and validation of quantum protocols. Master’s thesis, Department of Computer Science, University of Warwick, 2004. [Available as pdf] [Research Report CS-RT-413 version]
- PAPANIKOLAOU, N. Formal Specification and Verification of Quantum Cryptographic Protocols. Undergraduate Computing Project Report/B.Sc. Thesis, Department of Computer Science, University of Warwick, 2003. [Available as pdf]
HP Labs Technical Reports
2012
- MONAHAN, B., AND PAPANIKOLAOU, N. Pattern Detection and Extraction from Systems and Security Simulation Models, HP Labs Technical Report HPL-2012-89, HP Laboratories, April 2012.
- PAPANIKOLAOU, N. Semi-automated information extraction for security and privacy compliance in cloud computing, HP Labs Technical Report HPL-2012-71, HP Laboratories, April 2012.
- CASASSA MONT, M., MCCORRY, K., PAPANIKOLAOU, N., AND PEARSON, S. Security and privacy governance in cloud computing via SLAs and a policy orchestration service. HP Labs Technical Report HPL-2012-55, HP Laboratories, March 2012.
- PAPANIKOLAOU, N., PEARSON, S., CASASSA MONT, M., AND KO, R.
Automating compliance for cloud computing services.
HP Labs Internal Technical Report HPL-2012-56, HP Laboratories, March 2012.
2011
- PAPANIKOLAOU, N. Achieving compliance through natural-language analysis of service level agreements for cloud services. HP Labs Technical Report HPL-2011-167, HP Laboratories, 2011.
- PAPANIKOLAOU, N., PEARSON, S., AND CASASSA MONT, M.
Towards natural-language understanding and automated enforcement of privacy rules and regulations in the cloud: Survey and bibliography. HP Labs Technical Report HPL-2011-117, HP Laboratories, 2011.
- PAPANIKOLAOU, N., PEARSON, S., CASASSA MONT, M., AND KO, R.
Towards greater accountability in cloud computing through natural-language analysis and automated policy enforcement.
HP Labs Technical Report HPL-2011-118, HP Laboratories, 2011.
2010
- CASASSA MONT, M., PEARSON, S., GOLDSMITH, M., AND PAPANIKOLAOU, N. Towards a conceptual model for privacy policies. HP Labs Technical Report HPL-2010-82, HP Laboratories, 2010.
- PAPANIKOLAOU, N., CREESE, S., GOLDSMITH, M., CASASSA MONT, M., AND PEARSON, S. EnCoRe: Towards a holistic approach to privacy.
HP Labs Technical Report HPL-2010-83, HP Laboratories, 2010.
Other Publications
2011
- PAPANIKOLAOU, N., AND WAINWRIGHT, N. Trust and Security Research Roadmap for the Future Internet. 2011. Produced under the auspices of the EC effectsplus Research Project.
- WAINWRIGHT, N., AND PAPANIKOLAOU, N. Future Internet Assembly Research Roadmap. http://fisa.future-internet.eu/index.php/FIA_Research_Roadmap, 2011. Produced under the auspices of the EC effectsplus Research Project.
2010
- PAPANIKOLAOU, N. Review of 'Algorithms and Theory of Computation Handbook' Vols I and II, Edited by : Mikhail J. Atallah and Marina Blanton, Chapman & Hall / CRC Press, 2010 (ISBN: 978-1-58488-822-2). To appear in ACM SIGACT News. [Available as pdf]
- AGRAFIOTIS, I., CREESE, S., GOLDSMITH, M., AND PAPANIKOLAOU, N. Taxonomy of consent and revocation. EnCoRe Project Deliverable, September 2010.
- AGRAFIOTIS, I., CREESE, S., GOLDSMITH, M., AND PAPANIKOLAOU, N. The logic of consent and revocation. 2010. Internal Report, EnCoRe Research Project.
- PAPANIKOLAOU, N. Review of
'The Space and Motion of Communicating Agents' by Robin Milner, Cambridge University Press, 2009 (ISBN: 978-0-521-73833-0). In ACM SIGACT News 41, 3 (2010), 51—55. [Available as pdf]
2005-2008
- DAVIDSON, T., MLNARIK, H., NAGARAJAN, R., AND PAPANIKOLAOU, N. Verifying communicating quantum processes using QMC. Internal Report, Department of Computer Science, University of Warwick., 2008.
- PAPANIKOLAOU, N. Definition of the QMC Specification Language (Syntax and Operational Semantics). Internal Report, Department of Computer Science, University of Warwick., 2008.
[Version 1]
- PAPANIKOLAOU, N. Write-up of Nick's contribution to discussion following the BCS Computer Journal Lecture "Quantum Information Flow: A Computer Science Perspective" by Samson Abramsky (12/06/2007). [Available as
pdf]
- PAPANIKOLAOU, N., AND NAGARAJAN, R. Classical security protocols for QKD systems. Technical report, EU FP6 SECOQC Project, 2006 [Available as pdf].
- PAPANIKOLAOU, N. Review of
'Classical and Quantum Computing'
by Yorick Hardy and Willi-Hans
Steeb, Birkhauser Verlag, 2001 (ISBN: 3-7643-6610-9). In ACM SIGACT News 36, 3 (2005), 5–9. [Available as
pdf]
- PAPANIKOLAOU, N. Review of
'Data Privacy and Security'
by David Salomon, Springer-Verlag, 2003 (ISBN: 0-387-00311-8).
In ACM SIGACT News 36, 2 (2005), 8–13.
[Available as pdf]
Selected Talks
- "Defining Consent and Revocation Policies". Talk given at PrimeLife/IFIP Summer School 2010, 2-6 August 2010, Helsingborg, Sweden. [Slides available here]
- "Towards a Conceptual Model for Privacy Policies". Talk given at PrimeLife/IFIP Summer School 2010, 2-6 August 2010, Helsingborg, Sweden. [Slides available here]
- "Automated Search for Quantum Secret Sharing Protocols with Graph States". Talk given at the Third QNET Workshop 2009 on Semantics of Quantum Computation, 11 December 2009, School of Informatics, University of Edinburgh, Scotland. [Slides available here]
- "Towards Integrated Policy Management for Privacy". Talk given at W3C Workshop on Access Control Application Scenarios, 17th November 2009, Abbaye de Neumunster, Luxembourg. [Slides available
here]
- "Policy Refinement Checking." Talk given at Ninth International Workshop on Automated Verification of Critical Systems (AVoCS 09), 23-25 September 2009, Swansea University, Wales, England. [Slides available
here]
- "Potential and Limitations of Quantum Key Distribution: An Introduction". Invited talk at British Computer Society, 17 September 2009, as part of BCS Security Strategic Panel on "The Future of Cryptography". [Slides available here]
- "Making Online Security Risks More Tangible". Talk given at Web Science Conference 2009: Society Online, March 18-20, 2009, Foundation of the Hellenic World, Athens, Greece. [Slides available
here]
- "Ensuring Consent and Revocation: Towards a Taxonomy of Consent". Seminar (Concurrency, Verification and Security Seminar Series), February 11, 2009, Computing Laboratory, University of Oxford, Oxford, England.
[Seminar Announcement (Oxford)]
- "Ensuring Consent and Revocation: Towards a Taxonomy of Consent". Seminar (Digital Lab Seminar Series), February 4, 2009, International Digital Laboratory, University of Warwick, Coventry, England.
[Seminar Announcement
(WMG)]
- "Verifying Quantum Secret Sharing Protocols with the Quantum Model Checker." Talk given at the Second QNET Workshop, December 18-19, 2008, School of Informatics, University of Edinburgh, Edinburgh, Scotland.
[Workshop link]
- "Model Checking a Quantum Protocol: Theory, Implementation and Issues." Talk given at the First QNET Workshop, December 10-11, 2007, The Royal Society, London, England.
[Workshop link]
- "QMC: A Model Checker for Quantum Systems." Talk given at 5th Warwick Postgraduate Colloquium on Computer Science (WPCCS'07), July 3, 2007, Department of Computer Science, University of Warwick, Coventry, England. Received Best Presentation Award (and cash prize) [Slides available here]
- "QMC: A Model Checker for Quantum Systems." Invited talk given at Central European Quantum Information Processing Workshop (CEQIP'07), June 26, 2007, Valtice, Czech Republic. [Slides available here]
- "On Model-Checking Exogenous Quantum Logic: Complexity Aspects and Implementation." Algorithms and Formal Methods Seminar, January 29th, 2007, Department of Computer Science, University of Warwick, Coventry, England. [link to Algorithms and Formal Methods Group Seminars]
- "Model Checking Quantum Stabilizer Protocols." Talk given at QNET Workshop 2006 / Qday III, December 4th, 2006, University of Glasgow, Glasgow, Scotland.
- "Towards a Model Checker for Quantum Stabilizer Protocols." Seminar given at Centro de Logica e Computacao / SQIG, November 17th, 2006, Instituto Superior Tecnico, Lisbon, Portugal.
- "Towards a Verification Tool for Quantum Communication Protocols." Talk given at Scottish Theorem Proving Seminar, June 6th, 2006, University of Glasgow, Glasgow, Scotland. [This talk was supported by
SymNet.]
- "A Framework for Automated Verification of Quantum Cryptographic Protocols." Talk given at BCTCS'06, April 5th, 2006, University of Swansea, Wales, England. [Slides available here]
- "Model-Checking Quantum Key Distribution: Techniques and Results." Q-Day II Workshop on Mathematical Structures in Quantum Informatics, December 8th, 2005, Institut Henri Poincare, Universite Pierre et Marie Curie, Paris, France. [Slides available here]
- "An Automated Analysis of the Security of Quantum Key Distribution." AVoCS'05 Workshop, September 13th, 2005, University of Warwick, Coventry, England. [Slides available here]
- "An Automated Analysis of the Security of Quantum Key Distribution." SecCo 2005, August 22, 2005, Stanford Court Hotel, San Francisco, California, USA. [Slides available here]
- "Introduction to Quantum Cryptography."
Lecture, CS406 Research Directions in Computing course, October 2004, Department of Computer Science, University of Warwick, Coventry, England. [Slides available
here]
- "Quantum Gates and Circuits." Lecture, CS406 Research Directions in Computing course, October 2004, Department of Computer Science, University of Warwick, Coventry, England. [Slides available here]
- "Basics of Quantum Computation." Lecture, CS406 Research Directions in Computing course, October 2004, Department of Computer Science, University of Warwick, Coventry, England. [Slides available here]
- "Introduction to Quantum Cryptography."
Lecture, CS406 Research Directions in Computing course, October 2003, Department of Computer Science, University of Warwick, Coventry, England. [Slides available
here]
- "Introduction to Quantum Computation and Quantum Information." Open Day Presentation, October 2003, University of Warwick, Coventry, England. [Slides available here]
Software: Quantum Model Checker (QMC)
This section is devoted to the software Nick developed as part of his PhD, namely, the Quantum Model Checker (QMC). You will find here a description of the tool and:
QMC is a tool that automatically explores all possible behaviours arising from a quantum protocol description expressed in QMCLANG and enables QCTL properties to be checked over the resulting structure. Quantum protocols include only Clifford group operations on stabilizer states.
The QMC tool has three main components: (1) a process scheduler, (2) a language interpreter, and (3) a model checker. The role of component (1) is essentially to perform the tasks described in the previous paragraph. The language interpreter handles the execution of individual commands and keeps track of the overall classical and quantum state at each step. Finally, the verifier is responsible for evaluating QCTL formulae over the structure generated by (1) and (2). QMC has a graphical user interface which includes a user–friendly editor for models and properties.
A protocol model consists of definitions of one or more processes. The commands performed by these processes are interleaved, in order to simulate concurrent execution. Nondeterministic choices are resolved in all possible ways, producing a tree of all possible executions of the protocol.
QMC provides an interface to the GraphViz graph layout tool, and the ZGRVIEWER application, which can display the program execution tree.
Given a model and a QCTL formula for verification, QMC outputs the following:
- a summary of the files provided as input and basic feedback on the model provided including the number of states and the total number of runs,
- a verification result for the formula provided,
- a list of states (if any) that serve as counter-examples to the formula,
- a prompt which allows the user to track individual states and trace runs of interest, as well as to verify further formulae.
Teaching
Nick's teaching at the University of Warwick (before moving to HP) has included lectures
for CS406 Research Directions in Computing and seminars
for CS134 Introduction to Computer Security.
Nick was Teaching Assistant to Rajagopal Nagarajan for the 4th year module
CS406 Research Directions in Computing. He taught a lecture-based mini-course on Lexical and Syntactic Analysis as part of the 2nd year module CS245 Automata and Formal Languages (academic years 2005-6, 2006-7, 2007-8, 2008-9). Lecture notes are available below.
Nick would give a yearly Guest Lecture on Quantum Cryptography for the 1st year module CS134 Introduction to Computer Security (course organiser: Jane Sinclair).
Nick was Teaching Assistant to Sara Kalvala for the 2nd year module CS238 Concurrent Processes during the academic years 2003-2004 and 2004-2005.
Also, he assisted in surgery classes for CS120 Programming Laboratory during the academic year 2003-2004 and was involved in providing feedback and marking coursework for CS237 Concurrent Programming
during the academic year 2003-2004.
More information and course notes are available below.
Seminars for CS134
Course materials for CS134 including seminar handouts are available here (Warwick campus access only).
Lectures for CS406 (Lecture Notes below)
Handouts and Slides for Lectures and Seminars
- CS134 (Introduction to Computer Security) Guest Lecture on Quantum Cryptography [2007-8 version] pdf
[446 KB]
- CS245 (Automata and Formal Languages) Lecture 1 (31/01/2008)
- Lexical Analysis. Slides (2-3 per page) pdf [112 KB]
- CS245 (Automata and Formal Languages) Lecture 2 (01/02/2008)- Top-Down Parsing. Slides (2-3 per page): pdf [111 KB]
- CS245 (Automata and Formal Languages) Lecture 3 (04/02/2008)- Bottom-Up Parsing. Slides (2-3 per page): pdf [97 KB]
- CS238 (Concurrent Processes) Seminar
1 - Basics of CCS (agents, actions, synchronisation, semaphores): pdf [186 KB]
- CS238 (Concurrent Processes) Seminar 2
- CCS Examples (Buffers, Producers/Consumers problem): pdf [203 KB]
- CS238 (Concurrent Processes) Seminar 3
- CCS Equivalences and Bisimulation. Slides (handwritten):
pdf [260 KB]
- CS406 (Research Directions in Computing) - Revision class on Quantum Cryptography. Slides (handwritten): pdf [1,222 KB]
- CS406 (Research Directions in Computing) - Notes on Quantum Teleportation and Deutsch's algorithm: pdf [127 KB]
- CS406 (Research Directions in Computing) - Introduction to Quantum Cryptography. Lecture, October 2004, Department of Computer Science, University of Warwick. pdf [388 KB]
- CS406 (Research Directions in Computing) - Quantum Gates and Circuits. Lecture, October 2004, Department of Computer Science, University of Warwick. pdf [328 KB]
- CS406 (Research Directions in Computing) - Basics of Quantum Computation. Lecture, October 2004, Department of Computer Science, University of Warwick. pdf [199 KB]
- CS406 (Research Directions in Computing) - Introduction to Quantum Cryptography. Lecture, October 2003, Department of Computer Science, University of Warwick. pdf [781 KB]
- University of Warwick Open Day Presentation - Introduction to Quantum Computation and Quantum Information, October 2003. pdf [308 KB]
The content of this webpage is copyright of Nick Papanikolaou. Please make sure to cite this webpage if using/referring to materials available here.
"All points of view are my own and not necessarily HP's as well."
[back to top]
![[European Commission]](EU%20logo.jpg)
