Background and activities
I work in Theoretical Computer Science focusing on developing and using formal methods and tools for ensuring reliability of complex systems, including properties regarding security, safety, and concurrency. Applications of such methods are numerous, e.g., verification of safety properties of software systems (like absence of certain bugs) or of hybrid systems like the Smart Grids, ensuring security of Internet of Things, or modelling the concurrency of modern multi-core or high-performance computing. Among methods or models that I have created I can list: the Timed Distributed pi-calculus, the ST-structures, the Dynamic Structural Operational Semantics, the Synchronous Kleene Algebra, or the Higher Dimensional Modal Logic. Together with my students I have worked on developing tools, e.g., together with Manish Shrestha we made the LightSC Security Classification Method for Smart Grids and IoT and the associated usable security tool with the same name; whereas together with Bjørnar Luteberget we made the SAT modulo Discrete Event Simulation method and tool applied to railway capacity verification. A nice and long collaboration with Tore Pedersen has taken me also into the realm of modelling of human behaviour, where some of my contributions are: proposing the Behavioural Computer Science agenda, where models of human behaviour are combined with CS models of system behaviour (execution); or the probabilistic modelling of humans in security ceremonies.
I have done research in different areas of computer science, including modelling of security protocols; (object-oriented) programming languages and their formal semantics; modelling languages and verification of networked systems; models and tools for parallel programming and concurrent systems; algebras and logics as used in computer science; timed process calculi for distributed and mobile communicating systems; (legal) electronic contracts and privacy agreements (ToS -- Terms of Services). My work, more than 35 international articles, has been published in highly ranked conferences s.a. CONCUR, ATVA, LFCS, FM, POST, or CCS, and top journals s.a. JLAMP, IJCIP, FMSD, or LMCS. More recent works usually target security, privacy, trust, or access control. I finished my doctoral studies in 2010 at University of Oslo and have been involved ever since in teaching and supervisory activities, in reviewing for international conferences and journals, in the organisation of conferences and workshops, and in the writing of project proposals submitted to highly competitive calls, s.a.: EU-FP7-FET-Young-Explorers, Horison-2020, NFR-FRINATEK, UK’s EPSRC, ECSEL-JU.
Scientific, academic and artistic work
A selection of recent journal publications, artistic productions, books, including book and report excerpts. See all publications in the database
- (2020) A Methodology for Security Classification applied to Smart Grid Infrastructures. International Journal of Critical Infrastructure Protection. vol. 28.
- (2020) Generating Posets Beyond N. Lecture Notes in Computer Science (LNCS). vol. 12062.
- (2019) A stable non-interleaving early operational semantics for the pi-calculus. Journal of Logical and Algebraic Methods in Programming. vol. 104.
- (2019) Dynamic Structural Operational Semantics. Journal of Logical and Algebraic Methods in Programming. vol. 107.
- (2019) Summary of: Dynamic Structural Operational Semantics. Lecture Notes in Computer Science (LNCS). vol. 11918.
- (2019) Automated Drawing of Railway Schematics Using Numerical Optimization in SAT. Lecture Notes in Computer Science (LNCS). vol. 11918 LNCS.
- (2019) Synthesis of railway signaling layout from local capacity specifications. Lecture Notes in Computer Science (LNCS). vol. 11800 LNCS.
- (2019) Behavioural artificial intelligence: an agenda for systematic empirical studies of artificial inference. AI & Society: The Journal of Human-Centred Systems and Machine Intelligence.
- (2018) Behavioural Computer Science: an agenda for combining modelling of human and system behaviours. Human-centric Computing and Information Sciences. vol. 8:7.
- (2017) Automated verification of dynamic root of trust protocols. Lecture Notes in Computer Science (LNCS). vol. 10204 LNCS.
- (2017) A stable non-interleaving early operational semantics for the Pi-calculus. Lecture Notes in Computer Science (LNCS). vol. 10168 LNCS.
- (2017) Participatory verification of railway infrastructure by representing regulations in RailCNL. Lecture Notes in Computer Science (LNCS). vol. 10469 LNCS.
- (2017) Efficient verification of railway infrastructure designs against standard regulations. Formal methods in system design. vol. 52 (1).
- (2016) ST-structures. Journal of Logical and Algebraic Methods in Programming. vol. 85 (6).
- (2016) Towards Behavioural Computer Science. IFIP Advances in Information and Communication Technology. vol. 473.
- (2016) Rule-based incremental verification tools applied to railway designs and regulations. Lecture Notes in Computer Science (LNCS). vol. 9995 LNCS.
- (2016) Rule-based consistency checking of railway infrastructure designs. Lecture Notes in Computer Science (LNCS). vol. 9681.
- (2016) Declarative event based models of concurrency and refinement in psi-calculi. Journal of Logical and Algebraic Methods in Programming. vol. 85 (3).
- (2015) Probabilistic modelling of humans in security ceremonies. Lecture Notes in Computer Science (LNCS). vol. 8872.
- (2014) Actor network procedures as Psi-calculi for security ceremonies. Electronic Proceedings in Theoretical Computer Science. vol. 148.