Research
My Areas of Interest
Currently, my main area of interest is model checking of temporal logics, including variants of ATL (Alternating-time Temporal Logic), introduced by Alur, Henzinger and Kupferman, and especially methods of handling the problem of state space explosion that arises in formal verification of both synchronous and asynchronous systems. These techniques include partial order reduction, which was recently shown to be applicable to certain fragments of ATL.
Between 2019-2022, I participated in the joint Polish-Luxembourgish project STV (Socio-Technical Verification of Information Security and Trust in Voting Systems), and since 2023 in its continuation SpaceVote (Probabilistic Verification of Complex Heterogeneous Systems: From Ballots to Ballistics), whose aim is to develop new concepts, methods and tools for the formal verification of e-voting systems and protocols in terms of desired properties such as resistance to coercion or confidentiality.