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

12 Dec

Two new papers accepted at AAAI 2025

Researches in Formela lab discover algorithmic advances in planning for autonomous agents.

22 Jul

LGPD: A General Framework for Backpropagation through Embedded Optimization Layers

ICML 2024 Conference paper

April 2024

The PCTL satisfiability problem resolved!

The general/finite PCTL satisfiability problems are undecidable.

9 Dec 2023

A new paper was accepted to AAAI 2024!

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