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.