About me

Panagiotis Kouvaros
I am an Assistant Professor in Artificial Intelligence in the Department of Information Technologies at the University of Limassol.

My work primarly concerns the development of formal methods for assessing the safety and robustness of AI systems. It covers both symbolic and connectionist systems, including

  • optimisation-based approaches for the verification of adversarial robustness properties of neural networks,
  • logic-based approaches for the verification of the temporal-epistemic properties of multi-agent systems, and
  • hybrid approaches for the verification of strategic properties of neuro-symbolic systems.

Part of my research implements several core components of the verification engine of Safe Intelligence, where I partly work as a Research Consultant.

Previously I was a Research Fellow at the Verification of Autonomous Systems Group at Imperial College London and prior to that I was an Imperial College London EPSRC Doctoral Prize Fellow.

Publications

2024

Verification of Geometric Robustness of Neural Networks via Piecewise Linear Approximation and Lipschitz Optimisation. B. Batten, Y. Zheng, A. De Palma, P. Kouvaros and A. Lomuscio Proceedings of the 27th European Conference on Artificial Intelligence ( ECAI24). Santiago de Compostela, Spain. To Appear.
Formal Verification of Parameterised Neural-symbolic Multi-agent Systems. P. Kouvaros, E. Botoeva, C. Bonis-Campbel. Proceedings of the 33rd Joint International Conference on Artificial Intelligence ( IJCAI24). Jeju, South Korea.

2023

Towards Formal Verification of Neuro-symbolic Multi-agent Systems. P. Kouvaros. Proceedings of the 32nd Joint International Conference on Artificial Intelligence ( IJCAI23). Macao, S.A.R, China.
Verification of Semantic Key Point Detection for Aircraft Pose Estimation. P. Kouvaros, F. Leofante, B. Edwards, C. Chung, D. Margineantu, A. Lomuscio. Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning ( KR23). Rhodes, Greece.

2022

Formal Verification of Neural Agents in Non-determenistic Environments. Michael Akintunde, Elena Botoeva, Panagiotis Kouvaros, Alessio Lomuscio. Journal of Autonomous Agents and Multi-Agent Systems ( JAAMAS).

2021

OSIP: Tightened Bound Propagation for the Verification of ReLU Neural Networks. Vahid Hasemi, Panagiotis Kouvaros, Alessio Lomuscio. Proceedings of the 19th Interational Conference on Software Engineering and Formal Methods (SEFM21). Virtual conference.
Formal Analysis of Neural Network-based Systems in the Aircraft Domain. Panagiotis Kouvaros, Trent Kyono, Francesco Leofante, Alessio Lomuscio, Dragos Margineantu, Denis Osipychev, Yang Zheng. Proceedings of the 24th International Symposium on Formal Methods (FM21). Virtual conference.
Towards Scalable Complete Verification of ReLU Neural Networks via Dependency-based Branching. Panagiotis Kouvaros, Alessio Lomuscio. Proceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI21). Virtual conference.
Efficient Neural Network Verification via Layer-based Semidefinite Relaxations and Linear Cuts. Ben Batten, Panagiotis Kouvaros, Alessio Lomuscio, Yang Zheng. Proceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI21). Virtual conference.

2020

Verifying Strategic Abilities of Neural-symbolic Multi-agent Systems. Michael Akintunde, Elena Botoeva, Panagiotis Kouvaros, Alessio Lomuscio. Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning (KR20). Rhodes, Greece.
Formal Verification of Neural Agents in Non-determenistic Environments. Michael Akintunde, Elena Botoeva, Panagiotis Kouvaros, Alessio Lomuscio. Proceedings of the 19th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS20). Aucland, New Zealand.
Efficient Verification of ReLU-based Neural Networks via Dependency Analysis. Elena Botoeva, Panagiotis Kouvaros, Jan Kronqvist, Alessio Lomuscio, Ruth Misener. Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI20). New York City, New York.

2019

Formal Verification of Open Multi-Agent Systems. Panagiotis Kouvaros, Alessio Lomuscio, Edoardo Pirovano, Hashan Punchihewa. Proceedings of the 18th International Conference Autonomous Agents and Multi-Agent Systems (AAMAS19). Montreal, Canada. p. 179-187. IFAAMAS Press.

2018

Formal Verification of a Programmable Hypersurface. Panagiotis Kouvaros, Dimitrios Kouzapas, Anna Philippou, Julio Georgiou, Andreas Pitsillides. Proceedings of the 23rd International Conference on Formal Methods for Industrial Critical Systems (FMICS18). Maynooth, Ireland. p. 83-97. Springer.
Symbolic Synthesis of Fault-Tolerance Ratios in Parameterised Multi-Agent Systems. Panagiotis Kouvaros, Alessio Lomuscio, Edoardo Pirovano. Proceedings of the 27th International Joint Conference on Artificial Intelligence (IJCAI18). Stockholm, Sweden. p. 324-330. AAAI Press.

2017

Towards the Formal Verification of Correctness and Robustness of Robot Swarms (Invited Talk). Panagiotis Kouvaros, Alessio Lomuscio. Proceedings of the 18th Italian Conference on Theoretical Computer Science and the 32nd Italian Conference on Computational Logic (ICTCS17).
Verifying Fault-tolerance in Parameterised Multi-Agent Systems. Panagiotis Kouvaros, Alessio Lomuscio. Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI17). Melbourne, Australia. p.288-294. AAAI Press.
Parameterised Verification of Data-aware Multi-agent Systems. Francesco Belardinelli, Panagiotis Kouvaros, Alessio Lomuscio. Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI17). Melbourne, Australia. p. 98-104. AAAI Press.
Parameterised Verification of Infinite State Multi-Agent Systems via Predicate Abstraction. Panagiotis Kouvaros, Alessio Lomuscio. Proceedings of the 31st AAAI Conference on Artificial Intelligence (AAAI17). San Francisco (CA), USA p. 3013-3020. AAAI Press.

2016

Parameterised Model Checking for Alternating-Time Temporal Logic. Panagiotis Kouvaros, Alessio Lomuscio. Proceedings of the 22nd European Conference on Artificial Intelligence (ECAI16). The Hague, Netherlands. p. 1230-1238. IOS Press.
Parameterised Verification for Multi-Agent Systems. Panagiotis Kouvaros. PhD Thesis. Imperial College London.
Formal Verification of Opinion Formation in Swarms. Panagiotis Kouvaros, Alessio Lomuscio. Proceedings of the 15th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS16). Singapore. p. 1200-1209. IFAAMAS Press.
Verifying Security Properties in Unbounded Multi-Agent Systems. Ioana Boureanu, Panagiotis Kouvaros, Alessio Lomuscio. Proceedings of the 15th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS16). Singapore. p. 1209-1218. IFAAMAS Press.
Parameterised Verification for Multi-Agent Systems. Panagiotis Kouvaros, Alessio Lomuscio. Artificial Intelligence, 234. p. 152-189. Elsevier.

2015

Verifying Emergent Properties of Swarms.Panagiotis Kouvaros, Alessio Lomuscio. Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI15). Buenos Aires, Argentina. p. 1083-1089 AAAI Press.
A Counter Abstraction Technique for the Verification of Robot Swarms. Panagiotis Kouvaros, Alessio Lomuscio. Proceedings of the 29th AAAI Conference on Artificial Intelligence (AAAI15). Austin (TX), USA. p. 2081-2088. AAAI Press.

2013

A Cutoff Technique for the Verification of Parameterised Interpreted Systems with Parameterised Environments. Panagiotis Kouvaros, Alessio Lomuscio. Proceedings of the 23th International Joint Conference on Artificial Intelligence (IJCAI13). Bejing, China. p. 2013-2019. AAAI Press.
Automatic Verification of Parameterised Interleaved Multi-Agent Systems. Panagiotis Kouvaros, Alessio Lomuscio. Proceedings of the 12th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS13). Saint Paul, MN, USA. p. 861-868. IFAAMAS Press.

Software

VENUS

VENUS
Verification of NeUral Systems (VENUS) is a state-of-the-art sound and complete verification toolkit for Relu-based feed-forward neural networks. It can be used to check reachability and local adversarial robustness properties.

VENUS implements a MILP-based verification method whereby it leverages dependency relations between the ReLU nodes to reduce the search space that needs to be considered during branch-and-bound. It additionally implements methods based on symbolic interval propagation and input domain splitting.

VENUS is available for download from here.

MCMAS-P

MCMAS-P Input Language
MCMAS-P is a model checker for the verification of multi-agent systems composed of arbitrarily many agents. It takes as input multi-agent systems described in Parameterised Interleaved Interpreted Systems (PIIS) and implements cutoff and abstraction techniques to solve their parameterised verification problem.

MCMAS-P's main procedure is based on an incomplete counter abstraction method. Given the procedure is in exponential space, MCMAS-P additionally implements more effective cutoff-based methods for a number of fragments of PIIS.

MCMAS-P is available for download from here.

Service

  • Reviewer for Artificial Intelligence Journal, Swarm Intelligence, Theoretical Computer Science.
  • SPC Member for IJCAI 2021, AAAI 2020.
  • PC Member for IJCAI 2023, ICLR 2023, AAAI 2023, ICLR 2022, AAAI 2022, IJCAI 2022, ICML 2022, PAAMS 2022, NeurIPS 2022, WFVML 2022, TSRML 2022, NeurIPS 2021, PAAMS 2021, AAAI 2021, NeurIPS 2020, AAMAS 2020, AAMAS 2019, AAAI 2019, AAMAS 2018, AAAI 2018, IJCAI 2017, AAAI 2017, ECAI 2016.

Teaching

  • Guest Lecturer, Systems Verification, Department of Computing, Imperial College London, 2020.
  • Guest Lecturer, Model-Based Techniques for Safe and Trusted AI, Department of Computing, Imperial College London, 2020.
  • Lecturer, Data Structures and Algorithms, Department of Electrical and Computer Engineering, University of Cyprus, 2017-2018.
  • Lecturer, Computer Science and Information Systems, Department of Computer Science, University of Cyprus, 2017-2018.
  • Guest Lecturer, Systems Verification, Department of Computing, Imperial College London, 2017.
  • Tutor, Systems Verification, Department of Computing, Imperial College London, 2016-2017.
  • Tutor, Systems Verification, Department of Computing, Imperial College London, 2015-2016.
  • Tutor, Modal and Temporal Logic, Department of Computing, Imperial College London, 2015-2016.
  • Tutor, Modal and Temporal Logic, Department of Computing, Imperial College London, 2014-2015.