Ilina Stoilkovska, Igor Konnov, Josef Widder, and Florian Zuleger. “Eliminating Message Counters in Threshold Automata,” To appear at ATVA 2020. Read here.

Igor Konnov, Marijana Lazic, Ilina Stoilkovska, and Josef Widder. “Tutorial: Parameterized Verification with Byzantine Model Checker,” in FORTE, pages 189–207, 2020. Source here

Daniel Collins, Rachid Guerraoui, Jovan Komatovic, Matteo Monti, Athanasios Xygkis, Matej Pavlovic, Petr Kuznetsov, Yvonne-Anne Pig- nolet, Dragos-Adrian Seredinschi, and Andrei Tonkikh. “Online Payments by Merely Broadcasting Messages,” in DSN, 2020. Source here

Nathalie Bertrand, Igor Konnov, Marijana Lazi ́c, and Josef Widder. “Verification of randomized consensus algorithms under round-rigid adver- saries,” Invited Submission to International Journal on Software Tools for Technology Transfer. Source here.

Blockchain synchronization is one of the core protocols of Tendermint blockchains. In this short paper, we discuss our recent efforts in formal specification of the protocol and its implementation, as well as some initial model checking results. We demonstrate that the protocol quality and understanding can be improved by writing specifications and model checking them. By: Sean Braithwaite, Igor Konnov, Ilina Stoilkovska, Anca Zamfir, Ethan Buchman, Zarko Milosevic, and Josef Widder.