An Approach to the Verification of Symmetric Parameterized Distributed Systems. - Igor V. Konnov 001; Vladimir A. Zakharov (Program. Comput. Softw., 2005)

CheAPS: a Checker of Asynchronous Parameterized Systems. - Igor Konnov 001 (WING@ETAPS/IJCAR, 2010)

On application of weaker simulations to parameterized model checking by network invariants technique. - Igor V. Konnov 001 (Autom. Control. Comput. Sci., 2010)

An invariant-based approach to the verification of asynchronous parameterized networks. - Igor V. Konnov 001; Vladimir A. Zakharov (J. Symb. Comput., 2010)

Starting a Dialog between Model Checking and Fault-tolerant Distributed Algorithms - Annu John; Igor Konnov 001; Ulrich Schmid 001; Helmut Veith; Josef Widder (CoRR, 2012)

Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms - Annu John; Igor Konnov 001; Ulrich Schmid 001; Helmut Veith; Josef Widder (CoRR, 2012)

Parameterized model checking of fault-tolerant distributed algorithms by abstraction. - Annu John; Igor Konnov 001; Ulrich Schmid 001; Helmut Veith; Josef Widder (FMCAD, 2013)

Brief announcement: parameterized model checking of fault-tolerant distributed algorithms by abstraction. - Annu John; Igor Konnov 001; Ulrich Schmid 001; Helmut Veith; Josef Widder (PODC, 2013)

Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms. - Annu John; Igor Konnov 001; Ulrich Schmid 001; Helmut Veith; Josef Widder (SPIN, 2013)

Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms. - Annu Gmeiner; Igor Konnov 001; Ulrich Schmid 001; Helmut Veith; Josef Widder (SFM, 2014)

How to make a simple tool for verification of real-time systems. - Igor V. Konnov 001; Vladislav V. Podymov; Dmitry Yu. Volkanov; Vladimir A. Zakharov; Daniil A. Zorin (Autom. Control. Comput. Sci., 2014)

SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms. - Igor Konnov 001; Helmut Veith; Josef Widder (CAV (1), 2015)

What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms. - Igor V. Konnov 001; Helmut Veith; Josef Widder (Ershov Memorial Conference, 2015)

A combined toolset for the verification of real-time distributed systems. - Dmitry Yu. Volkanov; Vladimir A. Zakharov; Daniil A. Zorin; Vladislav V. Podymov; Igor V. Konnov 001 (Program. Comput. Softw., 2015)

Decidability of Parameterized Verification - Roderick Bloem; Swen Jacobs; Ayrat Khalimov 001; Igor Konnov 001; Sasha Rubin; Helmut Veith; Josef Widder (Morgan & Claypool Publishers, 2015)

Parameterized Systems in BIP: Design and Model Checking. - Igor V. Konnov 001; Tomer Kotek; Qiang Wang 020; Helmut Veith; Simon Bliudze; Joseph Sifakis (CONCUR, 2016)

Decidability in Parameterized Verification. - Roderick Bloem; Swen Jacobs; Ayrat Khalimov 001; Igor Konnov 001; Sasha Rubin; Helmut Veith; Josef Widder (SIGACT News, 2016)

Synthesis of Distributed Algorithms with Parameterized Threshold Guards. - Marijana Lazic; Igor Konnov 001; Josef Widder; Roderick Bloem (OPODIS, 2017)

A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. - Igor V. Konnov 001; Marijana Lazic; Helmut Veith; Josef Widder (POPL, 2017)

Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms. - Igor V. Konnov 001; Josef Widder; Francesco Spegni; Luca Spalazzi (VMCAI, 2017)

Para2: parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms. - Igor Konnov 001; Marijana Lazic; Helmut Veith; Josef Widder (Formal Methods Syst. Des., 2017)

On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability. - Igor V. Konnov 001; Helmut Veith; Josef Widder (Inf. Comput., 2017)

Reachability in Parameterized Systems: All Flavors of Threshold Automata. - Jure Kukovec; Igor Konnov 001; Josef Widder (CONCUR, 2018)

ByMC: Byzantine Model Checker. - Igor Konnov 001; Josef Widder (ISoLA (3), 2018)

Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (eds): Handbook of model checking - Springer International Publishing AG, Cham, Switzerland, 2018. - Igor Konnov 001 (Formal Aspects Comput., 2019)

TLA+ model checking made symbolic. - Igor Konnov 001; Jure Kukovec; Thanh-Hai Tran 002 (Proc. ACM Program. Lang., 2019)

Eliminating Message Counters in Threshold Automata. - Ilina Stoilkovska; Igor Konnov 001; Josef Widder; Florian Zuleger (ATVA, 2020)

Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper). - Sean Braithwaite; Ethan Buchman; Igor Konnov 001; Zarko Milosevic 001; Ilina Stoilkovska; Josef Widder; Anca Zamfir (FMBC@CAV, 2020)

Tutorial: Parameterized Verification with Byzantine Model Checker. - Igor Konnov 001; Marijana Lazic; Ilina Stoilkovska; Josef Widder (FORTE, 2020)

Tendermint Blockchain Synchronization: Formal Specification and Model Checking. - Sean Braithwaite; Ethan Buchman; Igor Konnov 001; Zarko Milosevic 001; Ilina Stoilkovska; Josef Widder; Anca Zamfir (ISoLA (1), 2020)

Cutoffs for Symmetric Point-to-Point Distributed Algorithms. - Thanh-Hai Tran 002; Igor Konnov 001; Josef Widder (NETYS, 2020)

A Tendermint Light Client. - Sean Braithwaite; Ethan Buchman; Ismail Khoffi; Igor Konnov 001; Zarko Milosevic 001; Romain Ruetschi; Josef Widder (CoRR, 2020)

Extracting symbolic transitions from TLA+ specifications. - Jure Kukovec; Thanh-Hai Tran 002; Igor Konnov 001 (Sci. Comput. Program., 2020)

Eliminating Message Counters in Synchronous Threshold Automata. - Ilina Stoilkovska; Igor Konnov 001; Josef Widder; Florian Zuleger (VMCAI, 2021)

Verification of randomized consensus algorithms under round-rigid adversaries. - Nathalie Bertrand 001; Igor Konnov 001; Marijana Lazic; Josef Widder (Int. J. Softw. Tools Technol. Transf., 2021)

Correction to: Verification of randomized consensus algorithms under round-rigid adversaries. - Nathalie Bertrand 001; Igor Konnov 001; Marijana Lazic; Josef Widder (Int. J. Softw. Tools Technol. Transf., 2021)

Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS. - Igor Konnov 001; Markus Kuppe 001; Stephan Merz (ISoLA (1), 2022)

Brief Announcement: Holistic Verification of Blockchain Consensus. - Nathalie Bertrand 001; Vincent Gramoli; Igor Konnov 001; Marijana Lazic; Pierre Tholoniat; Josef Widder (PODC, 2022)

Holistic Verification of Blockchain Consensus. - Nathalie Bertrand 001; Vincent Gramoli; Igor Konnov 001; Marijana Lazic; Pierre Tholoniat; Josef Widder (DISC, 2022)

Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS. - Igor Konnov 001; Markus Kuppe 001; Stephan Merz (CoRR, 2022)

Verifying safety of synchronous fault-tolerant algorithms by bounded model checking. - Ilina Stoilkovska; Igor Konnov 001; Josef Widder; Florian Zuleger (Int. J. Softw. Tools Technol. Transf., 2022)

Symbolic Model Checking for TLA+ Made Faster. - Rodrigo Otoni; Igor Konnov 001; Jure Kukovec; Patrick Eugster; Natasha Sharygina (TACAS (1), 2023)

Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker. - Igor Konnov 001; Marijana Lazic; Ilina Stoilkovska; Josef Widder (Log. Methods Comput. Sci., 2023)

A case study on parametric verification of failure detectors. - Thanh-Hai Tran 002; Igor Konnov 001; Josef Widder (Log. Methods Comput. Sci., 2023)

Technical Report: Exploring Automatic Model-Checking of the Ethereum specification. - Igor Konnov 001; Jure Kukovec; Thomas Pani; Roberto Saltini; Thanh-Hai Tran 002 (CoRR, 2025)

ChonkyBFT: Consensus Protocol of ZKsync. - Bruno França; Denis Kolegov; Igor Konnov 001; Grzegorz Prusak (CoRR, 2025)