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.
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.