Formela

Laboratory of Formal Methods, Logic, and Algorithms

The laboratory concentrates on applications of logic, game theory, and discrete structures in computer science. Special attention is devoted to algorithms and methods for formal analysis and verification of computer systems, applications of game theory in artificial intelligence, and also to emerging topics at the frontiers of formal methods and AI.

Want to join

Research Areas

Logic and Automata

There is a tight connection between certain logics and automata which can be used, for example, to devise decision procedures for problems in software verification.

Program Analysis and Verification

We develop methods for automatic analysis and verification of selected classes of computer systems, devoting special attention to probabilistic programs and programs with unbounded data types.

Risk-Aware Decision Making

We investigate reinforcement learning methods for risk-aware agents that act to maximize their rewards while keeping their risk at an acceptable level. We consider various classes of agents/environments and evaluate our algorithms experimentally.

Security Games

Security is one of the major societal concerns. We want to protect our airports, trains or digital networks. In practice, security resources are limited and the security guards have to be deployed selectively, raising the question of how to utilize them optimally.

News

9 Dec 2023

A new paper was accepted to AAAI 2024!

A paper on local stability of invariant distributions was accepted to AAAI 2024.

November 2023

CHESS Industrial Day 2023

CHESS Industrial Day 2023: Registration Open!

27 Jul 2023

A new paper on VASS MDPs accepted to CONCUR 2023

24 Apr 2023