Application of verification techniques to security: model checking insider attacks

Conference paper

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.
TypeConference paper
TitleApplication of verification techniques to security: model checking insider attacks
AuthorsKammueller, F., Probst, C. and Raimondi, F.
Abstract

In this paper, we give a short overview over the state of the art of formal verification techniques to the engineering of safe and secure systems. The main focus is on the support of security of real-world systems with mechanized verification techniques, in particular, model checking. Based on our prior experience with safety analysis – in particular the TWIN elevator (ThyssenKrupp) case study – the current case study ventures into the rising field of of social engineering attacks on security. This main focus and original contribution of this paper considers the security analysis of an insider attack illustrating the benefits of model checking with belief logics and actor system modeling.

Research GroupArtificial Intelligence group
Foundations of Computing group
Research Group on Development of Intelligent Environments
SensoLab group
Conference1st 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
Proceedings TitleSoftware and Emerging Technologies for Education, Culture, Entertainment and commerce
PublisherBlue Herons editions
Publication process dates
Deposited25 May 2012
Output statusPublished
Web address (URL)http://www.alaipo.com/setecec/conference_setecec_2012.html
LanguageEnglish
Permalink -

https://repository.mdx.ac.uk/item/83q3x

Log in to edit
  • 80
    total views
  • 0
    total downloads
  • 1
    views this month
  • 0
    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.
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 ACM. pp. 68 https://doi.org/10.1145/3664476
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
Differential cost analysis with simultaneous potentials and anti-potentials
Žikelić, Ð., Chang, B., Bolignano, P. and Raimondi, F. 2022. Differential cost analysis with simultaneous potentials and anti-potentials. Programming Language Design and Implementation (PLDI 2022). San Diego, USA 13 - 17 Jun 2022 Association for computing machinery. pp. 442-457 https://doi.org/10.1145/3519939.3523435
Automatic annotation of confidential data in java code
Bastys, I., Bolignano, P., Raimondi, F. and Schoepe, D. 2021. Automatic annotation of confidential data in java code. FPS 2021: The 14th International Symposium on Foundations & Practice of Security. Paris, France 08 - 12 Dec 2021
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 LIPICS --Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany. 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.
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
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
Comparing approaches for model-checking strategies under imperfect information and fairness constraints
Busard, S., Pecheur, C., Qu, H. and Raimondi, F. 2019. Comparing approaches for model-checking strategies under imperfect information and fairness constraints. International Journal on Software Tools for Technology Transfer. 21 (4), pp. 449-469. https://doi.org/10.1007/s10009-018-0505-6
Teaching functional patterns through robotic applications
Boender, J., Currie, E., Loomes, M., Primiero, G. and Raimondi, F. 2016. Teaching functional patterns through robotic applications. The 4th International Workshop on Trends in Functional Programming in Education, TFPIE 2015. Sophia-Antipolis, France 02 Jun 2015 Open Publishing Association. pp. 17-29 https://doi.org/10.4204/EPTCS.230.2
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).
Multi-agent based simulations of block-free distributed ledgers
Bottone, M., Raimondi, F. and Primiero, G. 2018. Multi-agent based simulations of block-free distributed ledgers. The 32nd IEEE International Conference on Advanced Information Networking and Applications Workshops (WAINA). Krakow, Poland 16 - 18 May 2018 IEEE. pp. 585-590 https://doi.org/10.1109/WAINA.2018.00149
Analysis and verification of ECA rules in intelligent environments
Cacciagrano, D., Corradini, F., Culmone, R., Gorogiannis, N., Mostarda, L., Raimondi, F. and Vannucchi, C. 2018. Analysis and verification of ECA rules in intelligent environments. Journal of Ambient Intelligence and Smart Environments. 10 (3), pp. 261-273. https://doi.org/10.3233/ais-180487
MIRTO: an open-source robotic platform for education
Androutsopoulos, K., Aristodemou, L., Boender, J., Bottone, M., Currie, E., El-Aroussi, I., Fields, B., Gheri, L., Gorogiannis, N., Heeney, M., Micheletti, M., Loomes, M., Margolis, M., Petridis, M., Piermarteri, A., Primiero, G., Raimondi, F. and Weldin, N. 2018. MIRTO: an open-source robotic platform for education. 3rd European Conference on Software Engineering Education. Seeon, Germany 14 - 15 Jun 2018 Association for Computing Machinery (ACM). pp. 55-62 https://doi.org/10.1145/3209087.3209106
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
CoSMed: a confidentiality-verified social media platform
Bauereiß, T., Pesenti Gritti, A., Popescu, A. and Raimondi, F. 2018. CoSMed: a confidentiality-verified social media platform. Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings. Nancy, France 22 - 27 Aug 2016 Springer. https://doi.org/10.1007/s10817-017-9443-3
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
CoSMed: a confidentiality-verified social media platform
Bauereiß, T., Pesenti Gritti, A., Popescu, A. and Raimondi, F. 2016. CoSMed: a confidentiality-verified social media platform. ITP 2016: 7th International Conference on Interactive Theorem Proving. Nancy, France 22 - 25 Aug 2016 Springer. pp. 87-106 https://doi.org/10.1007/978-3-319-43144-4_6
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
The packing chromatic number of the infinite square lattice is between 13 and 15
Martin, B., Raimondi, F., Chen, T. and Martin, J. 2017. The packing chromatic number of the infinite square lattice is between 13 and 15. Discrete Applied Mathematics. 225, pp. 136-142. https://doi.org/10.1016/j.dam.2017.03.013
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
Implementing virtual pheromones in BDI robots using MQTT and Jason
Bottone, M., Palumbo, F., Primiero, G., Raimondi, F. and Stocker, R. 2016. Implementing virtual pheromones in BDI robots using MQTT and Jason. 2016 5th IEEE International Conference on Cloud Networking (Cloudnet). Pisa, Italy 03 - 05 Oct 2016 Institute of Electrical and Electronics Engineers (IEEE). pp. 196-199 https://doi.org/10.1109/CloudNet.2016.22
From raw data to agent perceptions for simulation, verification, and monitoring
Bottone, M., Primiero, G., Raimondi, F. and Rungta, N. 2016. From raw data to agent perceptions for simulation, verification, and monitoring. 12th International Conference on Intelligent Environment 2016:- 5th International Workshop on Reliability of Intelligent Environments (WoRIE’16). London, United Kingdom 14 - 16 Sep 2016 IOS Press. pp. 66-75 https://doi.org/10.3233/978-1-61499-690-3-66
Trust and distrust in contradictory information transmission
Primiero, G., Raimondi, F., Bottone, M. and Tagliabue, J. 2017. Trust and distrust in contradictory information transmission. Applied Network Science. 2 (1). https://doi.org/10.1007/s41109-017-0029-0
Examining the interaction between fourth estate and Twitter: an exploratory case study
Barn, B., Barn, R., Raimondi, F. and Mukherjee, U. 2017. Examining the interaction between fourth estate and Twitter: an exploratory case study. HUSO 2017: Third International Conference on Human and Social Analytics. Nice, France 23 - 27 Jul 2017 IARIA. pp. 11-17
Symbolic verification of event–condition–action rules in intelligent environments
Vannucchi, C., Diamanti, M., Mazzante, G., Cacciagrano, D., Culmone, R., Gorogiannis, N., Mostarda, L. and Raimondi, F. 2017. Symbolic verification of event–condition–action rules in intelligent environments. Journal of Reliable Intelligent Environments. 3 (2), pp. 117-130. https://doi.org/10.1007/s40860-017-0036-z
A novel symbolic approach to verifying epistemic properties of programs
Gorogiannis, N., Raimondi, F. and Boureanu, I. 2017. A novel symbolic approach to verifying epistemic properties of programs. Twenty-Sixth International Joint Conference on Artificial Intelligence. Melbourne, Australia 19 - 25 Aug 2017 International Joint Conferences on Artificial Intelligence. pp. 206-212 https://doi.org/10.24963/ijcai.2017/30
CoSMeDis: a distributed social media platform with formally verified confidentiality guarantees
Bauereiß, T., Pesenti Gritti, A., Popescu, A. and Raimondi, F. 2017. CoSMeDis: a distributed social media platform with formally verified confidentiality guarantees. 38th IEEE Symposium on Security and Privacy. San Jose, CA, USA 22 - 26 May 2017 Institute of Electrical and Electronics Engineers (IEEE). pp. 729-748 https://doi.org/10.1109/SP.2017.24
MCMAS: an open-source model checker for the verification of multi-agent systems
Lomuscio, A., Qu, H. and Raimondi, F. 2017. MCMAS: an open-source model checker for the verification of multi-agent systems. International Journal on Software Tools for Technology Transfer. 19 (1), pp. 9-30. https://doi.org/10.1007/s10009-015-0378-x
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
Contradictory information flow in networks with trust and distrust
Primiero, G., Bottone, M., Raimondi, F. and Tagliabue, J. 2016. Contradictory information flow in networks with trust and distrust. 5th International Workshop on Complex Networks and their Applications (COMPLEX NETWORKS 2016). Milan 01 - 06 Dec 2016 Springer. https://doi.org/10.1007/978-3-319-50901-3_29
A model for trustworthy orchestration in the internet of things
Bottone, M., Primiero, G., Raimondi, F. and De Florio, V. 2016. A model for trustworthy orchestration in the internet of things. 2016 12th International Conference on Intelligent Environments (IE). London, United Kingdom 14 - 16 Sep 2016 IEEE. pp. 171-174 https://doi.org/10.1109/IE.2016.37
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
Using multi-agent systems to go beyond temporal patterns verification
Raimondi, F. 2016. Using multi-agent systems to go beyond temporal patterns verification. ACM SIGLOG News. 3 (2), pp. 69-77.
A computationally grounded, weighted doxastic logic
Chen, T., Primiero, G., Raimondi, F. and Rungta, N. 2016. A computationally grounded, weighted doxastic logic. Studia Logica. 104 (4), pp. 679-703. https://doi.org/10.1007/s11225-015-9621-4
Minimizing transitive trust threats in software management systems
Boender, J., Primiero, G. and Raimondi, F. 2015. Minimizing transitive trust threats in software management systems. 13th Annual Conference on Privacy, Security and Trust (PST 2015). Izmir, Turkey 21 - 23 Jul 2015 Institute of Electrical and Electronics Engineers (IEEE). pp. 191-198 https://doi.org/10.1109/PST.2015.7232973
Symbolic model-checking for resource-bounded ATL
Alechina, N., Logan, B., Nguyen, H., Raimondi, F. and Mostarda, L. 2015. Symbolic model-checking for resource-bounded ATL. 2015 International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015. Istanbul, Turkey 04 - 08 May 2015 pp. 1809-1810
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
Taking Arduino to the Internet of things: the ASIP programming model
Barbon, G., Margolis, M., Palumbo, F., Raimondi, F. and Weldin, N. 2016. Taking Arduino to the Internet of things: the ASIP programming model. Computer Communications. 89-90, pp. 128-140. https://doi.org/10.1016/j.comcom.2016.03.016
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
Software theory change for resilient near-complete specifications
Primiero, G. and Raimondi, F. 2015. Software theory change for resilient near-complete specifications. Procedia Computer Science. 52, pp. 988-995. https://doi.org/10.1016/j.procs.2015.05.091
Temporal planning for business process optimisation
Magazzeni, D., Mercorio, F., Barn, B., Clark, T., Raimondi, F. and Kulkarni, V. 2014. Temporal planning for business process optimisation. ICAPS 2014: 8th Scheduling and Planning Application woRKshop (SPARK 2014). Portsmouth, New Hampshire, USA 22 Jun 2014
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
Towards cyber-physical systems as services: the ASIP protocol
Bordoni, M., Bottone, M., Fields, B., Gorogiannis, N., Margolis, M., Primiero, G. and Raimondi, F. 2015. Towards cyber-physical systems as services: the ASIP protocol. 2015 IEEE/ACM 1st International Workshop on Software Engineering for Smart Cyber-Physical Systems (SEsCPS). Florence, Italy 17 - 17 May 2015 IEEE. pp. 52-55 https://doi.org/10.1109/SEsCPS.2015.18
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
Programming the MIRTO robot with neurons
Huyck, C., Primiero, G. and Raimondi, F. 2014. Programming the MIRTO robot with neurons. Procedia Computer Science. 41, pp. 75-82. https://doi.org/10.1016/j.procs.2014.11.087
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
A typed natural deduction calculus to reason about secure trust
Primiero, G. and Raimondi, F. 2014. A typed natural deduction calculus to reason about secure trust. 2014 Twelfth Annual Conference on Privacy, Security and Trust (PST). Toronto, Canada 23 - 24 Jul 2014 Institute of Electrical and Electronics Engineers (IEEE). pp. 379-382 https://doi.org/10.1109/PST.2014.6890963
Decidable model-checking for a resource logic with production of resources
Alechina, N., Logan, B., Nguyen, H. and Raimondi, F. 2014. Decidable model-checking for a resource logic with production of resources. 21st European Conference on Artificial Intelligence (ECAI-2014). Prague, Czech Republic 18 - 22 Aug 2014 Prague, Czech Republic IOS Press. pp. 9-14 https://doi.org/10.3233/978-1-61499-419-0-9
Aviation safety: modeling and analyzing complex interactions between humans and automated systems
Rungta, N., Brat, G., Clancey, W., Linde, C., Raimondi, F., Seah, C. and Shafto, M. 2013. Aviation safety: modeling and analyzing complex interactions between humans and automated systems. ATACCS 2013. Naples, Italy 28 - 30 May 2013 Association for computing machinery. pp. 27-37 https://doi.org/10.1145/2494493.2494498
A synergistic and extensible framework for multi-agent system verification
Hunter, J., Raimondi, F., Rungta, N. and Stocker, R. 2013. A synergistic and extensible framework for multi-agent system verification. AAMAS 2013 :12th International Conference on Autonomous Agents and Multiagent Systems. Saint Paul, Minnesota, USA. 06 - 10 May 2013 Richland, SC International Foundation for Autonomous Agents and Multiagent Systems. pp. 869-876
Domain types: abstract-domain selection based on variable usage
Apel, S., Beyer, D., Friedberger, K., Raimondi, F. and von Rhein, A. 2013. Domain types: abstract-domain selection based on variable usage. Hardware and Software: Verification and Testing. 8244 (1), pp. 262-278. https://doi.org/10.1007/978-3-319-03077-7_18
Implementing adaptation and reconfiguration strategies in heterogeneous WSN
Di Marco, A., Gallo, F., Gemikonakli, O., Mostarda, L. and Raimondi, F. 2013. Implementing adaptation and reconfiguration strategies in heterogeneous WSN. 27th IEEE International Conference on Advanced Information Networking and Applications (AINA-2013). Barcelona, Spain 25 - 28 Mar 2013 IEEE. pp. 477-483 https://doi.org/10.1109/AINA.2013.102
The anonymous subgraph problem
Bettinelli, A., Liberti, L., Raimondi, F. and Savourey, D. 2013. The anonymous subgraph problem. Computers and Operations Research. 40 (4), pp. 973-979. https://doi.org/10.1016/j.cor.2012.11.018
Introducing Binary Decision Diagrams in the explicit-state verification of Java code
von Rhein, A., Apel, S. and Raimondi, F. 2011. Introducing Binary Decision Diagrams in the explicit-state verification of Java code. The Java Pathfinder Workshop (co-located with ASE 2011). Oread, Lawrence, Kansas 12 Nov 2011
Symbolic model checking for one-resource RB±ATL
Alechina, N., Logan, B., Nguyen, H. and Raimondi, F. 2015. Symbolic model checking for one-resource RB±ATL. Yang, Q. and Wooldridge, M. (ed.) 24th International Joint Conference on Artificial Intelligence (IJCAI 2015). Buenos Aires, Argentina 25 - 31 Jul 2015 Buenos Aires, Argentina AAAI Press / International Joint Conferences on Artificial Intelligence. pp. 1069-1075
On the role of value sensitive concerns in software engineering practice
Barn, B., Barn, R. and Raimondi, F. 2015. On the role of value sensitive concerns in software engineering practice. 37th International Conference on Software Engineering, ICSE 2015. Florence, Italy 16 - 24 May 2015 IEEE. pp. 497-500 https://doi.org/10.1109/ICSE.2015.182
A racket-based robot to teach first-year computer science
Androutsopoulos, K., Gorogiannis, N., Loomes, M., Margolis, M., Primiero, G., Raimondi, F., Varsani, P., Weldin, N. and Zivanovic, A. 2014. A racket-based robot to teach first-year computer science. 7 th European Lisp Symposium. IRCAM, Paris, France 05 - 06 May 2014 pp. 54-61
Model checking degrees of belief in a system of agents
Primiero, G., Raimondi, F. and Rungta, N. 2014. Model checking degrees of belief in a system of agents. AAMAS 2014: 13th International Conference on Autonomous Agents and Multiagent Systems. Paris, France 05 - 09 May 2014 International Foundation for Autonomous Agents and Multiagent Systems. pp. 133-140
Improving the model checking of strategies under partial observability and fairness constraints
Busard, S., Pecheur, C., Qu, H. and Raimondi, F. 2014. Improving the model checking of strategies under partial observability and fairness constraints. 16th International Conference on Formal Engineering Methods, ICFEM 2014. Luxembourg 03 - 05 Nov 2014 Springer International Publishing. https://doi.org/10.1007/978-3-319-11737-9_3
Slrtool: a tool to support collaborative systematic literature reviews
Barn, B., Raimondi, F., Athiappan, L. and Clark, T. 2014. Slrtool: a tool to support collaborative systematic literature reviews. 16th International Conference on Enterprise Information Systems. Lisbon, Portugal 27 - 30 Apr 2014 SciTePress. pp. 440-447 https://doi.org/10.5220/0004972204400447
Context-aware adaptive applications: fault patterns and their automated identification
Sama, M., Elbaum, S., Raimondi, F., Rosenblum, D. and Wang, Z. 2010. Context-aware adaptive applications: fault patterns and their automated identification. IEEE Transactions on Software Engineering. 36 (5), pp. 644-661. https://doi.org/10.1109/TSE.2010.35
Evaluation of collaborative filtering algorithms using a small dataset
Roda, F., Liberti, L. and Raimondi, F. 2011. Evaluation of collaborative filtering algorithms using a small dataset. WEBIST 2011. http://www.webist.org/WEBIST2011/
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
Reasoning about strategies under partial observability and fairness constraints
Busard, S., Pecheur, C., Qu, H. and Raimondi, F. 2013. Reasoning about strategies under partial observability and fairness constraints. 1st International Workshop on Strategic Reasoning. Rome, Italy 16 - 17 Mar 2013 Open Publishing Association. https://doi.org/10.4204/EPTCS.112.12
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
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 ACM. pp. 48-53
Checking the TWIN elevator system by translating object-Z to SMV
Preibusch, S. and Kammueller, F. 2008. Checking the TWIN elevator system by translating object-Z to SMV. Lecture Notes in Computer Science. 4916, pp. 38-55. https://doi.org/10.1007/978-3-540-79707-4
Composing safely: a type system for aspects
Kammueller, F. and Sudhof, H. 2008. Composing safely: a type system for aspects. Lecture Notes in Computer Science. 4954, pp. 231-247. https://doi.org/10.1007/978-3-540-78789-1_18
Security analysis of private data enquiries in Erlang
Kammueller, F. and Kammueller, R. 2009. Security analysis of private data enquiries in Erlang. International Journal on Advances in Security. 2 (2&3), pp. 242-255.
An asynchronous distributed component model and its semantics
Henrio, L., Kammueller, F. and Rivera, M. 2009. An asynchronous distributed component model and its semantics. Lecture Notes in Computer Science. 5751, pp. 159-179. https://doi.org/10.1007/978-3-642-04167-9_9
A framework for reasoning on component composition
Henrio, L., Kammueller, F. and Khan, M. 2010. A framework for reasoning on component composition. Lecture Notes in Computer Science. 6286, pp. 1-20. https://doi.org/10.1007/978-3-642-17071-3_1
Formalizing non-interference for a simple bytecode language in Coq
Kammueller, F. 2008. Formalizing non-interference for a simple bytecode language in Coq. Formal Aspects of Computing. 20 (3), pp. 259-275.
Mechanical analysis of finite idempotent relations
Kammueller, F. 2011. Mechanical analysis of finite idempotent relations. Fundamenta Informaticae. 107 (1), pp. 43-65. https://doi.org/10.3233/FI-2011-392
Privacy enforcement and analysis for functional active objects
Kammueller, F. 2011. Privacy enforcement and analysis for functional active objects. Lecture Notes in Computer Science. 6514, pp. 93-107. https://doi.org/10.1007/978-3-642-19348-4_8
The secret santa problem.
Liberti, L. and Raimondi, F. 2008. The secret santa problem. Lecture Notes in Computer Science. 5034, pp. 271-279. https://doi.org/10.1007/978-3-540-68880-8_26
Efficient online monitoring of web-service SLAs
Raimondi, F., Skene, J. and Emmerich, W. 2008. Efficient online monitoring of web-service SLAs. in: Harrold, J. and Murphy, G. (ed.) Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering Association for computing machinery. pp. 170-180
Algorithms for efficient symbolic detection of faults in context-aware applications.
Sama, M., Raimondi, F., Rosenblum, D. and Emmerich, W. 2008. Algorithms for efficient symbolic detection of faults in context-aware applications. in: Automated Software Engineering - Workshops, 2008. ASE Workshops 2008. 23rd IEEE/ACM International Conference. Institute of Electrical and Electronics Engineers. pp. 1-8
Service-level agreements for electronic services
Skene, J., Raimondi, F. and Emmerich, W. 2010. Service-level agreements for electronic services. IEEE Transactions on Software Engineering. 36 (2), pp. 288-304. https://doi.org/10.1109/TSE.2009.55
PDVer, a tool to verify PDDL planning domains.
Raimondi, F., Pecheur, C. and Brat, G. 2009. PDVer, a tool to verify PDDL planning domains. ICAPS'09 Workshop on Verification and Validation of Planning and Scheduling Systems. Thessaloniki, Greece 20 Sep 2009
The Anonymous subgraph problem.
Bettinelli, A., Liberti, L., Raimondi, F. and Savourey, D. 2009. The Anonymous subgraph problem. Cologne Twente Workshop 2009: 8th Cologne-Twente Workshop on Graphs and Combinatorial Optimization. Paris 02 - 04 Jun 2009 pp. 269-274
Combinatorial optimization based recommender systems.
Roda, F., Liberti, L. and Raimondi, F. 2009. Combinatorial optimization based recommender systems. Cologne Twente Workshop 2009: 8th Cologne-Twente Workshop on Graphs and Combinatorial Optimization. Paris 02 - 04 Jun 2009 pp. 175-179
A model to design and verify context-aware adaptive service composition.
Cubo, J., Sama, M., Raimondi, F. and Rosenblum, D. 2009. A model to design and verify context-aware adaptive service composition. 6th IEEE International Conference on Services Computing (SCC 2009). Bangalore 21 - 25 Sep 2009
A formal analysis of requirements-based testing
Pecheur, C., Raimondi, F. and Brat, G. 2009. A formal analysis of requirements-based testing. in: Rothermel, G. and Dillon, L. (ed.) Proceedings of the Eighteenth International Symposium on Software Testing and Analysis Association for computing machinery. pp. 47-56
MCMAS: a model checker for the verification of multi-agent systems
Lomuscio, A., Qu, H. and Raimondi, F. 2009. MCMAS: a model checker for the verification of multi-agent systems. Lecture Notes in Computer Science. 5643, pp. 682-688. https://doi.org/10.1007/978-3-642-02658-4_55