Bornat, R.; Boender, J.; Kammueller, F.; Poly, G.; Nagarajan, R.

Describing and simulating concurrent quantum systems

Conference paper

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

ISBN
Type	Conference paper
Title	Describing and simulating concurrent quantum systems
Authors	Bornat, R., Boender, J., Kammueller, F., Poly, G. and Nagarajan, R.
Abstract	We present a programming language for describing and analysing concurrent quantum systems. We have an interpreter for programs in the language, using a symbolic rather than a numeric calculator, and we give its performance on examples from quantum communication and cryptography.
Research Group	Foundations of Computing group
Conference	International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 20)
Page range	271-277
Editors	Biere, A. and Parker, D.
ISSN	0302-9743
Electronic	1611-3349
Hardcover	9783030452360
Electronic	9783030452377
Publisher	Springer
Publication dates
Online	17 Apr 2020
Print	18 Apr 2020
Publication process dates
Deposited	27 Feb 2020
Accepted	23 Dec 2019
Output status	Published
Publisher's version	Bornat2020_Chapter_DescribingAndSimulatingConcurr.pdf License CC BY 4.0
Accepted author manuscript	License CC BY 4.0
Copyright Statement	© The Author(s) 2020 Open Access: This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter’s Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter’s Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Additional information	Paper published as: Bornat R., Boender J., Kammueller F., Poly G., Nagarajan R. (2020) Describing and Simulating Concurrent Quantum Systems. In: Biere A., Parker D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2020. Lecture Notes in Computer Science, vol 12079. Springer, Cham
Digital Object Identifier (DOI)	https://doi.org/10.1007/978-3-030-45237-7_16
Language	English
Book title	Tools and Algorithms for the Construction and Analysis of Systems: 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings

Permalink -

https://repository.mdx.ac.uk/item/88wz1

Log in to edit

Download files

Publisher's version

	Bornat2020_Chapter_DescribingAndSimulatingConcurr.pdf
License: CC BY 4.0

File access - Request a copy

Restricted files

Accepted author manuscript

Under embargo indefinitely

79
total views
23
total downloads
4
views this month
2
downloads this month

Export as

Related outputs

Formalizing federated learning and differential privacy for GIS systems in IIIf

Kammueller, F., Piras, L., Fields, B. and Nagarajan, R. 2024. Formalizing federated learning and differential privacy for GIS systems in IIIf. 3rd International Workshop on System Security Assurance. Bydgoszcz, Poland 19 - 20 Sep 2024 Springer.

Transparency vs explanation of machine learning algorithms: perspectives from recent legal proceedings

Nnawuchi, U., George, C. and Kammueller, F. 2024. Transparency vs explanation of machine learning algorithms: perspectives from recent legal proceedings. Santos M., Machado, J., Novais, P., Cortez, P. and Moreira, P. (ed.) 23rd International Conference on Artificial Intelligence. Viana do Castelo, Portugal 03 - 06 Sep 2024 Springer. pp. 270-283 https://doi.org/10.1007/978-3-031-73497-7_22

Analyzing air-traffic security using GIS-``blur'' with information flow control in the IIIf

Kammueller, F. 2024. Analyzing air-traffic security using GIS-``blur'' with information flow control in the IIIf. 19th International Conference on Availability, Reliability and Security. Vienna, Austria 30 Jul - 02 Aug 2024 New York, NY Association for Computing Machinery (ACM). pp. 68 https://doi.org/10.1145/3664476

Introducing distributed ledger security into system specifications with the Isabelle RR-cycle

Kammueller, F. 2024. Introducing distributed ledger security into system specifications with the Isabelle RR-cycle. 28th European Symposium on Research in Computer Security: 2nd International Workshop on System Security Assurance (SecAssure). The Hague, The Netherlands 29 - 29 Sep 2023 Springer. pp. 330-340 https://doi.org/10.1007/978-3-031-54129-2_19

Explanation by automated reasoning using the Isabelle Infrastructure framework

Kammueller, F. 2022. Explanation by automated reasoning using the Isabelle Infrastructure framework. Human Computer Interaction International. Virtual 26 Jun - 01 Jul 2022

Exploring rationality of self awareness in social networking for logical modeling of unintentional insiders

Kammueller, F. and Alvarado, C. 2022. Exploring rationality of self awareness in social networking for logical modeling of unintentional insiders. Moallem, A. (ed.) HCI-CPT: 4th International Conference on HCI for Cybersecurity, Privacy and Trust. Virtual 26 Jun - 01 Jul 2022 Springer. pp. 340-357 https://doi.org/10.1007/978-3-031-05563-8_22

Explanation by automated reasoning using the Isabelle Infrastructure framework

Kammueller, F. 2021. Explanation by automated reasoning using the Isabelle Infrastructure framework. arxiv.org. https://doi.org/10.48550/arXiv.2112.14809

Explanation of black box AI for GDPR related privacy using Isabelle

Kammueller, F. 2022. Explanation of black box AI for GDPR related privacy using Isabelle. Garcia-Alfaro, J., Navarro-Arribas, G. and Dragoni, N. (ed.) 17th DPM International Workshop on Data Privacy Management. Copenhagen, Denmark 29 - 30 Sep 2022 Cham Springer. https://doi.org/10.1007/978-3-031-25734-6_5

Dependability engineering in Isabelle

Kammueller, F. 2021. Dependability engineering in Isabelle. arxiv.org.

Exploring rationality of self awareness in social networking for logical modeling of unintentional insiders

Kammueller, F. and Alvarado, C. 2021. Exploring rationality of self awareness in social networking for logical modeling of unintentional insiders. arxiv.org.

Modeling and verifying a resource allocation algorithm for secure service migration for commercial cloud systems

Karthick, G., Mapp, G., Kammueller, F. and Aiash, M. 2022. Modeling and verifying a resource allocation algorithm for secure service migration for commercial cloud systems. Computational Intelligence. 38 (3), pp. 811-828. https://doi.org/10.1111/coin.12421

Applying the Isabelle insider framework to airplane security

Kammueller, F. and Kerber, M. 2021. Applying the Isabelle insider framework to airplane security. Science of Computer Programming. 206. https://doi.org/10.1016/J.SCICO.2021.102623

A formal development cycle for security engineering in Isabelle

Kammueller, F. 2020. A formal development cycle for security engineering in Isabelle. arxiv.org.

Applying the Isabelle Insider framework to airplane security

Kammueller, F. and Kerber, M. 2020. Applying the Isabelle Insider framework to airplane security. arxiv.org.

Masterminding change by combining secure system design with security risk assessment

Kammueller, F., Legay, A. and Schivo, S. 2021. Masterminding change by combining secure system design with security risk assessment. International Journal on Software Tools for Technology Transfer. 23 (1), pp. 69-70. https://doi.org/10.1007/s10009-020-00595-8

Combining secure system design with risk assessment for IoT healthcare systems

Kammueller, F. 2019. Combining secure system design with risk assessment for IoT healthcare systems. SPT-IoT'19 - The Third Workshop on Security, Privacy and Trust in the Internet of Things, colocated with IEEE PerCom 2019. Kyoto, Japan 11 - 15 Mar 2019 Institute of Electrical and Electronics Engineers (IEEE). pp. 961-966 https://doi.org/10.1109/PERCOMW.2019.8730776

Modeling and analyzing the Corona-virus warning app with the Isabelle infrastructure framework

Kammueller, F. and Lutz, B. 2020. Modeling and analyzing the Corona-virus warning app with the Isabelle infrastructure framework. Garcia-Alfaro, J., Navarro-Arribas, G. and Herrera-Joancomarti, J. (ed.) International Workshop of Data Privacy Management, DPM'20. University of Surrey, UK 17 - 18 Sep 2020 Springer. pp. 128-144 https://doi.org/10.1007/978-3-030-66172-4_8

Inter-blockchain protocols with the Isabelle Infrastructure framework

Kammueller, F. and Nestmann, U. 2020. Inter-blockchain protocols with the Isabelle Infrastructure framework. Bernardo, B. and Marmsoler, D. (ed.) 2nd Workshop on Formal Methods for Blockchain, co-located with CAV'20. Los Angeles, CA, USA Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH. pp. 11:1-11:12 https://doi.org/10.4230/OASIcs.FMBC.2020.11

Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems

Kammueller, F. 2020. Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems.

Exploring a security protocol for secure service migration in commercial cloud environments

Karthick, G., Mapp, G., Kammueller, F. and Aiash, M. 2017. Exploring a security protocol for secure service migration in commercial cloud environments. ICC’17. Cambridge University, Cambridge 22 Mar 2019 ICC’17, Cambridge, United Kingdom © 2017 ACM.. pp. 1-6 https://doi.org/10.1145/3018896.3056795

Attack trees in Isabelle

Kammueller, F. 2018. Attack trees in Isabelle. 20th International Conference on Information and Communications Security, ICICS 2018. Lille, France 29 - 31 Oct 2018 Springer. pp. 611-628 https://doi.org/10.1007/978-3-030-01950-1_36

Attack trees in Isabelle extended with probabilities for Quantum Cryptography

Kammueller, F. 2019. Attack trees in Isabelle extended with probabilities for Quantum Cryptography. Computers and Security. 87. https://doi.org/10.1016/j.cose.2019.101572

Edit distance Kernelization of NP theorem proving for polynomial-time machine learning of proof heuristics

Windridge, D. and Kammueller, F. 2020. Edit distance Kernelization of NP theorem proving for polynomial-time machine learning of proof heuristics. FICC 2019: Future of Information and Communications Conference. San Francisco, USA 14 - 15 Mar 2019 Springer. pp. 271-283 https://doi.org/10.1007/978-3-030-12385-7_22

Formal modeling and analysis of data protection for GDPR compliance of IoT healthcare systems

Kammueller, F. 2018. Formal modeling and analysis of data protection for GDPR compliance of IoT healthcare systems. IEEE SMC 2018: IEEE International Conference on Systems, Man and Cybernetics. Miyazaki, Japan 08 - 10 Oct 2018 Institute of Electrical and Electronics Engineers (IEEE).

Automated equivalence checking of concurrent quantum systems

Ardeshir-Larijani, E., Gay, S. and Nagarajan, R. 2018. Automated equivalence checking of concurrent quantum systems. ACM Transactions on Computational Logic. 19 (4), pp. 1-32. https://doi.org/10.1145/3231597

Formalization and analysis of a resource allocation security protocol for secure service migration

Karthick, G., Mapp, G., Kammueller, F. and Aiash, M. 2018. Formalization and analysis of a resource allocation security protocol for secure service migration. IEEE/ACM International Conference on Utility and Cloud Computing (UCC2018). Zurich, Switzerland 17 - 20 Dec 2018 IEEE. pp. 207-212 https://doi.org/10.1109/UCC-Companion.2018.00058

Quantum error-correcting output codes

Windridge, D., Mengoni, R. and Nagarajan, R. 2018. Quantum error-correcting output codes. International Journal of Quantum Information. 16 (8). https://doi.org/10.1142/S0219749918400038

A proof calculus for attack trees in Isabelle

Kammueller, F. 2017. A proof calculus for attack trees in Isabelle. 12th International Workshop on Data Privacy Management (DPM 2017). Oslo, Norway 14 - 15 Sep 2017 Springer. pp. 3-18 https://doi.org/10.1007/978-3-319-67816-0_1

A proof-theoretic trust and reputation model for VANET

Primiero, G., Raimondi, F., Chen, T. and Nagarajan, R. 2017. A proof-theoretic trust and reputation model for VANET. S4CIP’17: 2nd Workshop on Safety & Security aSSurance for Critical Infrastructures Protection. Paris, France 29 Apr 2017 Institute of Electrical and Electronics Engineers (IEEE). pp. 146-152 https://doi.org/10.1109/EuroSPW.2017.64

Exploring a security protocol for secure service migration in commercial cloud environments

Karthick, G., Mapp, G., Kammueller, F. and Aiash, M. 2017. Exploring a security protocol for secure service migration in commercial cloud environments. 2nd International Conference on Internet of Things, Data and Cloud Computing (ICC 2017). Churchill College, University of Cambridge, United Kingdom 22 - 23 Mar 2017 Association for Computing Machinery (ACM). https://doi.org/10.1145/3018896.3056795

Model based analysis of insider threats

Chen, T., Han, T., Kammueller, F., Nemli, I. and Probst, C. 2016. Model based analysis of insider threats. 2016 International Conference on Cyber Security and Protection of Digital Services (Cyber Security). London, United Kingdom 13 - 14 Jun 2016 Institute of Electrical and Electronics Engineers (IEEE). https://doi.org/10.1109/CyberSecPODS.2016.7502350

Security and privacy requirements engineering for human centric IoT systems using eFRIEND and Isabelle

Kammueller, F., Augusto, J. and Jones, S. 2017. Security and privacy requirements engineering for human centric IoT systems using eFRIEND and Isabelle. IEEE/ACIS 15th International Conference on Software Engineering Research, Management and Application, SERA2017. University of Greenwich, London, United Kingdom 07 - 09 Jun 2017 Institute of Electrical and Electronics Engineers (IEEE). https://doi.org/10.1109/SERA.2017.7965758

Formal modeling and analysis with humans in infrastructures for IoT health care systems

Kammueller, F. 2017. Formal modeling and analysis with humans in infrastructures for IoT health care systems. 5th International Conference on Human Aspects of Security, Privacy and Trust, HCII-HAS 2017. Vancouver, BC, Canada 09 - 14 Jul 2017 Springer. pp. 339-352 https://doi.org/10.1007/978-3-319-58460-7_24

Human centric security and privacy for the IoT using formal techniques

Kammueller, F. 2018. Human centric security and privacy for the IoT using formal techniques. 3rd International Conference on Human Factors in Cybersecurity. Los Angeles, CA, United States 17 - 21 Jul 2017 Springer. pp. 106-116 https://doi.org/10.1007/978-3-319-60585-2_12

Insider threats for auctions: formalization, mechanized proof, and code generation

Kammueller, F., Kerber, M. and Probst, C. 2017. Insider threats for auctions: formalization, mechanized proof, and code generation. Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA). 8 (1), pp. 44-78. https://doi.org/10.22667/JOWUA.2017.03.31.044

Quantum Bootstrap Aggregation

Windridge, D. and Nagarajan, R. 2017. Quantum Bootstrap Aggregation. de Barros, J., Coecke, B. and Pothos, E. (ed.) Quantum Interaction. San Francisco, CA, USA 20 - 22 Jul 2016 Springer. pp. 115-121 https://doi.org/10.1007/978-3-319-52289-0_9

Hamming distance kernelisation via topological quantum computation

Di Pierro, A., Mengoni, R., Nagarajan, R. and Windridge, D. 2017. Hamming distance kernelisation via topological quantum computation. Martín-Vide C., Neruda R. and Vega-Rodríguez M. (ed.) 6th International Conference on the Theory and Practice of Natural Computing. Prague, Czech Republic 18 - 20 Dec 2017 Springer. pp. 269-280 https://doi.org/10.1007/978-3-319-71069-3_21

Modeling and verification of insider threats using logical analysis

Kammueller, F. and Probst, C. 2017. Modeling and verification of insider threats using logical analysis. IEEE Systems Journal. 11 (2), pp. 534-545. https://doi.org/10.1109/JSYST.2015.2453215

Towards formal analysis of insider threats for auctions

Kammueller, F., Kerber, M. and Probst, C. 2016. Towards formal analysis of insider threats for auctions. ACM-CCS Workshop on Management of Security of Insider Threats. Vienna, Austria 28 Oct 2016 Association for Computing Machinery (ACM). pp. 23-34 https://doi.org/10.1145/2995959.2995963

Isabelle Modelchecking for insider threats

Kammueller, F. 2016. Isabelle Modelchecking for insider threats. 11th DPM International Workshop on Data Privacy Management (DPM 2016) co-located with ESORICS 2016. Heraklion, Crete, Greece 26 - 27 Sep 2016 Springer. pp. 196-210 https://doi.org/10.1007/978-3-319-47072-6_13

Refactoring preserves security

Kammueller, F. 2016. Refactoring preserves security. 11th DPM International Workshop on Data Privacy Management (DPM 2016) co-located with ESORICS 2016. Heraklion, Crete, Greece 26 - 27 Sep 2016 Springer. pp. 238-245 https://doi.org/10.1007/978-3-319-47072-6_17

Verification of statecharts using data abstraction

Helke, S. and Kammueller, F. 2016. Verification of statecharts using data abstraction. International Journal of Advanced Computer Science and Applications. 7 (1), pp. 571-583. https://doi.org/10.14569/IJACSA.2016.070179

Formal modelling and analysis of socio-technical systems

Probst, C., Kammueller, F. and Hansen, R. 2016. Formal modelling and analysis of socio-technical systems. in: Semantics, Logics, and Calculi Springer International.

Attack tree analysis for insider threats on the IoT using Isabelle

Kammueller, F., Nurse, J. and Probst, C. 2016. Attack tree analysis for insider threats on the IoT using Isabelle. 4th International Conference on Human Aspects of Security, Privacy and Trust, HCII-HAS 2016. Toronto, ON, Canada 17 - 24 Jul 2016 Springer International. pp. 234-246 https://doi.org/10.1007/978-3-319-39381-0_21

Investigating airplane safety and security against insider threats using logical modeling

Kammueller, F. and Kerber, M. 2016. Investigating airplane safety and security against insider threats using logical modeling. 2016 IEEE Security and Privacy Workshops SPW'16: Workshop on Research in Insider Threats WRIT'16. San Jose, CA, USA 22 - 26 May 2016 Institute of Electrical and Electronics Engineers (IEEE). pp. 304-313 https://doi.org/10.1109/SPW.2016.47

Secure refactoring with Java information flow

Helke, S., Kammueller, F. and Probst, C. 2016. Secure refactoring with Java information flow. 10th International Workshop on Data Privacy Management (DPM 2015). Vienna, Austria 21 - 22 Sep 2015 Springer. pp. 264-272 https://doi.org/10.1007/978-3-319-29883-2_19

Transforming graphical system models to graphical attack models

Ivanova, M., Probst, C., Hansen, R. and Kammueller, F. 2016. Transforming graphical system models to graphical attack models. 2nd International Workshop on Graphical Models for Security, GraMSec 2015, co-located with CSF2015. Verona, Italy 13 Jul 2015 Springer. pp. 82-96 https://doi.org/10.1007/978-3-319-29968-6_6

Attack tree generation by policy invalidation

Ivanova, M., Probst, C., Hansen, R. and Kammueller, F. 2015. Attack tree generation by policy invalidation. 9th WISTP International Conference on Information Security Theory and Practice (WISTP 2015). Heraklion, Crete, Greece 24 - 25 Aug 2015 Springer. pp. 249-259 https://doi.org/10.1007/978-3-319-24018-3_16

Techniques for formal modelling and analysis of quantum systems

Gay, S. and Nagarajan, R. 2013. Techniques for formal modelling and analysis of quantum systems. in: Computation, logic, games, and quantum foundations. The many facets of Samson Abramsky Springer Verlag.

Formalization of quantum protocols using Coq

Boender, J., Kammueller, F. and Nagarajan, R. 2015. Formalization of quantum protocols using Coq. The 12th International Workshop on Quantum Physics and Logic (QPL 2015). Oxford, United Kingdom 15 - 17 Jul 2015 pp. 71-83

Invalidating policies using structural information

Kammueller, F. and Probst, C. 2013. Invalidating policies using structural information. IEEE CS Security and Privacy Workshops, SPW, WRIT'13.

Network information flow control: proof of concept

Alghothami, A. and Kammueller, F. 2013. Network information flow control: proof of concept. IEEE Int. Conf. on Systems, Man, and Cybernetics, SMC. Manchester, UK 13 - 16 Oct 2013 IEEE. pp. 2957-2962 https://doi.org/10.1109/SMC.2013.504

Privacy analysis of a hidden friendship protocol

Kammueller, F. and Preibusch, S. 2013. Privacy analysis of a hidden friendship protocol. The 8th International Workshop on Data Privacy Management, DPM 2013. Egam, UK 12 - 13 Sep 2013 Springer. pp. 83-99

Externalizing behaviour for analysing system models

Ivanova, M., Probst, C., Hansen, R. and Kammueller, F. 2013. Externalizing behaviour for analysing system models. 5th International Workshop on Managing Insider Security Threats, MIST, 2013..

Verification of quantum protocols using Coq

Boender, J., Kammueller, F. and Nagarajan, R. 2014. Verification of quantum protocols using Coq. 17th Conference on Quantum Information Processing (QIP). Barcelona, Spain 03 - 07 Feb 2014

Reviews for the American Mathematical Society (AMS): Paul Howells, Mark d’Inverno. Specifying termination in CSP. Theoretical Computer Science, 503:31–61, 2013.

Kammueller, F. 2014. Reviews for the American Mathematical Society (AMS): Paul Howells, Mark d’Inverno. Specifying termination in CSP. Theoretical Computer Science, 503:31–61, 2013. MathSciNet: Mathematical Reviews.

Combining generated data models with formal invalidation for insider threat analysis

Kammueller, F. and Probst, C. 2014. Combining generated data models with formal invalidation for insider threat analysis. 2014 IEEE Security and Privacy Workshops (SPW): Workshop on Research for Insider Threat (WRIT 2014). San Jose, California, USA 17 - 18 May 2014 Institute of Electrical and Electronics Engineers (IEEE). pp. 229-235 https://doi.org/10.1109/SPW.2014.45

Verification of DNSsec delegation signatures

Kammueller, F. 2014. Verification of DNSsec delegation signatures. 21st International IEEE Conference on Telecommunication. Lisbon 04 - 07 May 2014 Institute of Electrical and Electronics Engineers (IEEE). pp. 298-392 https://doi.org/10.1109/ICT.2014.6845127

Invalidating policies using structural information

Kammueller, F. and Probst, C. 2014. Invalidating policies using structural information. Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications. 5 (2), pp. 59-79. https://doi.org/10.22667/JOWUA.2014.06.31.059

Modeling human behaviour with higher order logic: insider threats

Boender, J., Kammueller, F., Ivanova, M. and Primiero, G. 2014. Modeling human behaviour with higher order logic: insider threats. 4th Workshop on Socio-Technical Aspects in Security and Trust. Vienna Technical University, Vienna, Austria 18 Jul 2014 Institute of Electrical and Electronics Engineers (IEEE). pp. 31-39

A probabilistic analysis framework for malicious insider threats

Chen, T., Kammueller, F., Nemli, I. and Probst, C. 2015. A probabilistic analysis framework for malicious insider threats. 3rd International Conference on Human Aspects of Information Security, Privacy and Trust, HAS 2015, held as part of HCI International 2015. Los Angeles, California, USA 02 - 07 Aug 2015 Springer. pp. 178-189

Confinement for active objects

Kammueller, F. 2015. Confinement for active objects. International Journal of Advanced Computer Science and Applications. 6 (2), pp. 246-261. https://doi.org/10.14569/IJACSA.2015.060236

Modeling human behaviour with higher order logic: insider threats

Boender, J., Ivanova, M., Kammueller, F. and Primiero, G. 2014. Modeling human behaviour with higher order logic: insider threats. 4th Workshop on Socio-Technical Aspects in Security and Trust (STAST 2014). Vienna, Austria 18 Jul 2014 Institute of Electrical and Electronics Engineers. pp. 31-39 https://doi.org/10.1109/STAST.2014.13

Verification of concurrent quantum protocols by equivalence checking

Ardeshir-Larijani, E., Gay, S. and Nagarajan, R. 2014. Verification of concurrent quantum protocols by equivalence checking. TACAS 2014: 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Grenoble, France 05 - 13 Apr 2014 Springer. https://doi.org/10.1007/978-3-642-54862-8_42

Model checking for communicating quantum processes

Davidson, T., Gay, S., Mlnařík, H., Nagarajan, R. and Papanikolaou, N. 2012. Model checking for communicating quantum processes. International Journal of Unconventional Computing. 8 (1), pp. 73-98.

Lossless quantum prefix compression for communication channels that are always open

Müller, M., Rogers, C. and Nagarajan, R. 2009. Lossless quantum prefix compression for communication channels that are always open. Physical Review A. 79 (1). https://doi.org/10.1103/PhysRevA.79.012302

Equivalence checking of quantum protocols

Ardeshir-Larijani, E., Gay, S. and Nagarajan, R. 2013. Equivalence checking of quantum protocols. in: Piterman, N. and Smolka, S. (ed.) Tools and Algorithms for the Construction and Analysis of Systems : 19th International Conference Proceedings (TACAS 2013). Berlin Springer.

QMC: a model checker for quantum systems

Gay, S., Nagarajan, R. and Papanikolaou, N. 2008. QMC: a model checker for quantum systems. in: Gupta, A. and Malik, S. (ed.) Computer Aided Verification : 20th International Conference, (CAV 2008) Proceedings Berlin Springer.

DNSsec in Isabelle – replay attack and origin authentication

Kammueller, F., Kirsal-Ever, Y. and Cheng, X. 2013. DNSsec in Isabelle – replay attack and origin authentication. SMC 2013: IEEE International Conference on Systems, Man, and Cybernetics. Manchester, UK 13 - 16 Oct 2013 IEEE. pp. 4772-4777 https://doi.org/10.1109/SMC.2013.812

A semi-lattice model for multi-lateral security

Kammueller, F. 2013. A semi-lattice model for multi-lateral security. in: Data privacy management and autonomous spontaneous security Berlin, Germany Springer.

A security model for functional active objects

Kammueller, F. 2012. A security model for functional active objects. Francisco, C., Kim, V., Miguel, C. and Andreas, K. (ed.) First International Symposium Communicability, Computer Graphics and Innovative Design for Interactive Systems (CCGIDIS 2011). Berlin Springer. https://doi.org/10.1007/978-3-642-33760-4_4

A security model for functional active objects with an implementation in Erlang

Fleck, A. and Kammueller, F. 2011. A security model for functional active objects with an implementation in Erlang. in: Ficarra, F., Kratky, A., Veltman, K., Ficarra, M., Nicol, E. and Brie, M. (ed.) Computational informatics, social factors and new information technologies: hypermedia perspectives and avant-garde experiences in the era of communicability expansion Bergamo, Italy Blue Herons.

Engineering security protocols with modelchecking – Radius-SHA256 and secured simple protocol.

Kammueller, F., Mapp, G., Patel, S. and Sani, A. 2012. Engineering security protocols with modelchecking – Radius-SHA256 and secured simple protocol. International Conference on Internet Monitoring and Protection (ICIMP 2012). Stuttgart, Germany 27 May - 01 Jun 2012 Xpert Publishing Service.

Review for the American Mathematical Society (AMS): A. Francalanza et al. Permission-based separation logic for message-passing concurrency. Logical methods in computer science, 7: 1-47, 2011

Kammueller, F. 2012. Review for the American Mathematical Society (AMS): A. Francalanza et al. Permission-based separation logic for message-passing concurrency. Logical methods in computer science, 7: 1-47, 2011. Mathematical Reviews.

Reviews for the American Mathematical Society (AMS): Russell O’Connor. Classical mathematics for a constructive world. MSCS (21): 861–882, Cambridge University Press. 2010.

Kammueller, F. 2012. Reviews for the American Mathematical Society (AMS): Russell O’Connor. Classical mathematics for a constructive world. MSCS (21): 861–882, Cambridge University Press. 2010. Mathematical Reviews.

A locally nameless theory of objects

Henrio, L., Kammueller, F., Lutz, B. and Sudhof, H. 2010. A locally nameless theory of objects. SAFA Annual Workshop on Formal Techniques (SAFA’2010). 2229 Route des Crêtes, 06560, Valbonne, Provence-Alpes-Côte d'Azur, France

Locally nameless sigma calculus

Henrio, L., Kammueller, F., Lutz, B. and Sudhof, H. 2010. Locally nameless sigma calculus. Archive of Formal Proof.

Formalizing statecharts using hierarchical automata

Helke, S. and Kammueller, F. 2010. Formalizing statecharts using hierarchical automata. Archive of Formal Proof.

Radius-SHA256 – verified remote authentication with secure hashing.

Kammueller, F. and Patel, S. 2011. Radius-SHA256 – verified remote authentication with secure hashing. First Global Conference on Communication, Science and Information Engineering, CCSIE’11. Middlesex University 25 - 27 Jul 2011

ASPfun: a typed functional active object calculus

Henrio, L., Kammueller, F. and Lutz, B. 2012. ASPfun: a typed functional active object calculus. Science of Computer Programming. 77 (7-8), pp. 823-847. https://doi.org/10.1016/j.scico.2010.12.008

Application of verification techniques to security: model checking insider attacks

Kammueller, F., Probst, C. and Raimondi, F. 2012. Application of verification techniques to security: model checking insider attacks. 1st International Conference on Software and Emerging Technologies for Education, Culture, Entertainment, and Commerce (SETECEC 2012): New Directions in Multimedia Mobile Computing, Social Networks, Human-Computer Interaction and Communicability. Venice, Italy 28 - 29 Mar 2012 Blue Herons editions.

Modelchecking non-functional requirements for interface specifications.

Kammueller, F. and Preibusch, S. 2008. Modelchecking non-functional requirements for interface specifications. European Joint Conference on Theory and Practice of Software, 2008, (Foundations of Interface technologies). Budapest 29 Mar - 06 Apr 2008

Compositionality of aspect weaving.

Kammueller, F. and Sudhof, H. 2008. Compositionality of aspect weaving. in: Mahr, B. and Sheng, H. (ed.) Autonomous systems: self-organisation, management, and control. Springer Verlag. pp. 87-96

Interactive theorem proving in software engineering.

Kammueller, F. 2008. Interactive theorem proving in software engineering. Saarbrücken, Germany VDM Verlag Dr. Mueller.

Using functional active objects to enforce privacy

Kammueller, F. 2010. Using functional active objects to enforce privacy. 5th Conference on Network Architectures and Information Systems Security. Menton, France 18 - 21 May 2010

Enhancing privacy implementations of database enquiries

Kammueller, F. and Kammueller, R. 2009. Enhancing privacy implementations of database enquiries. IEEE. pp. 45-50 https://doi.org/10.1109/ICIMP.2009.15

Implementing privacy with Erlang active objects

Fleck, A. and Kammueller, F. 2010. Implementing privacy with Erlang active objects. International Conference on Internet Monitoring and Protection. Barcelona 09 - 15 May 2010 IEEE. pp. 141-146 https://doi.org/10.1109/ICIMP.2010.27

Privacy by flexible parameterization with Erlang active objects.

Fleck, A. and Kammueller, F. 2010. Privacy by flexible parameterization with Erlang active objects. International Journal on Advances in Software. 3 (3-4), pp. 461-473.

Functional active objects: typing and formalisation

Henrio, L. and Kammueller, F. 2009. Functional active objects: typing and formalisation. Elsevier. https://doi.org/10.1016/j.entcs.2009.10.026

Feature link propagation across variability representations with Isabelle/HOL

Kammueller, F., Rein, A. and Reiser, M. 2010. Feature link propagation across variability representations with Isabelle/HOL. Rubin, J., Botterweck, G., Mezini, M., Maman, I. and Lero, A. (ed.) New York Association for Computing Machinery (ACM). pp. 48-53