| 2026 | CAV | The TLA+ Model Checker Apalache. | Rodrigo Otoni, Shon Feder, Jure Kukovec, Andrey Kupriyanov, Gabriela Moreira, Philip Offtermatt, Thomas Pani, Thanh-Hai Tran, Igor Konnov |
| 2023 | TACAS | Symbolic Model Checking for TLA+ Made Faster. | Rodrigo Otoni, Igor Konnov, Jure Kukovec, Patrick Eugster, Natasha Sharygina |
| 2022 | ISoLA | Specification and Verification with the TLA | Igor Konnov, Markus Kuppe, Stephan Merz |
| 2022 | PODC | Brief Announcement: Holistic Verification of Blockchain Consensus. | Nathalie Bertrand, Vincent Gramoli, Igor Konnov, Marijana Lazic, Pierre Tholoniat, Josef Widder |
| 2021 | FORTE | A Case Study on Parametric Verification of Failure Detectors. | Thanh-Hai Tran, Igor Konnov, Josef Widder |
| 2021 | VMCAI | Eliminating Message Counters in Synchronous Threshold Automata. | Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger |
| 2020 | ATVA | Eliminating Message Counters in Threshold Automata. | Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger |
| 2020 | CAV | Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper). | Sean Braithwaite, Ethan Buchman, Igor Konnov, Zarko Milosevic, Ilina Stoilkovska, Josef Widder, Anca Zamfir |
| 2020 | FORTE | Tutorial: Parameterized Verification with Byzantine Model Checker. | Igor Konnov, Marijana Lazic, Ilina Stoilkovska, Josef Widder |
| 2020 | ISoLA | Tendermint Blockchain Synchronization: Formal Specification and Model Checking. | Sean Braithwaite, Ethan Buchman, Igor Konnov, Zarko Milosevic, Ilina Stoilkovska, Josef Widder, Anca Zamfir |
| 2019 | CONCUR | Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries. | Nathalie Bertrand, Igor Konnov, Marijana Lazic, Josef Widder |
| 2019 | TACAS | Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking. | Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger |
| 2018 | CONCUR | Reachability in Parameterized Systems: All Flavors of Threshold Automata. | Jure Kukovec, Igor Konnov, Josef Widder |
| 2018 | ISoLA | ByMC: Byzantine Model Checker. | Igor Konnov, Josef Widder |
| 2017 | OPODIS | Synthesis of Distributed Algorithms with Parameterized Threshold Guards. | Marijana Lazic, Igor Konnov, Josef Widder, Roderick Bloem |
| 2015 | CAV | SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms. | Igor Konnov, Helmut Veith, Josef Widder |
| 2014 | CONCUR | On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability. | Igor Konnov, Helmut Veith, Josef Widder |
| 2013 | FMCAD | Parameterized model checking of fault-tolerant distributed algorithms by abstraction. | Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder |
| 2013 | PODC | Brief announcement: parameterized model checking of fault-tolerant distributed algorithms by abstraction. | Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder |
| 2010 | CADE | CheAPS: a Checker of Asynchronous Parameterized Systems. | Igor Konnov |