Igor Konnov

46 papers A* 2A 1B 8C 3Journal 20Unranked 11
YearRankTypeTitle / Venue / Authors
2025 J jnl
ChonkyBFT: Consensus Protocol of ZKsync.
CoRR
Bruno França, Denis Kolegov, Igor Konnov, Grzegorz Prusak
2025 J jnl
Technical Report: Exploring Automatic Model-Checking of the Ethereum specification.
CoRR
Igor Konnov, Jure Kukovec, Thomas Pani, Roberto Saltini, Thanh-Hai Tran
2023 J jnl
A case study on parametric verification of failure detectors.
Log. Methods Comput. Sci.
Thanh-Hai Tran, Igor Konnov, Josef Widder
2023 J jnl
Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker.
Log. Methods Comput. Sci.
Igor Konnov, Marijana Lazic, Ilina Stoilkovska, Josef Widder
2023 — conf
Symbolic Model Checking for TLA+ Made Faster.
TACAS (1)
Rodrigo Otoni, Igor Konnov, Jure Kukovec, Patrick Eugster, Natasha Sharygina
2022 A* conf
Brief Announcement: Holistic Verification of Blockchain Consensus.
PODC
Nathalie Bertrand, Vincent Gramoli, Igor Konnov, Marijana Lazic, Pierre Tholoniat, Josef Widder
2022 A conf
Holistic Verification of Blockchain Consensus.
DISC
Nathalie Bertrand, Vincent Gramoli, Igor Konnov, Marijana Lazic, Pierre Tholoniat, Josef Widder
2022 J jnl
Holistic Verification of Blockchain Consensus.
CoRR
Nathalie Bertrand, Vincent Gramoli, Igor Konnov, Marijana Lazic, Pierre Tholoniat, Josef Widder
2022 — conf
Specification and Verification with the TLA
ISoLA (1)
Igor Konnov, Markus Kuppe, Stephan Merz
2022 J jnl
Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS.
CoRR
Igor Konnov, Markus Kuppe, Stephan Merz
2022 J jnl
Verifying safety of synchronous fault-tolerant algorithms by bounded model checking.
Int. J. Softw. Tools Technol. Transf.
Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger
2021 C conf
A Case Study on Parametric Verification of Failure Detectors.
FORTE
Thanh-Hai Tran, Igor Konnov, Josef Widder
2021 J jnl
A case study on parametric verification of failure detectors.
CoRR
Thanh-Hai Tran, Igor Konnov, Josef Widder
2021 J jnl
Correction to: Verification of randomized consensus algorithms under round-rigid adversaries.
Int. J. Softw. Tools Technol. Transf.
Nathalie Bertrand, Igor Konnov, Marijana Lazic, Josef Widder
2021 B conf
Eliminating Message Counters in Synchronous Threshold Automata.
VMCAI
Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger
2021 J jnl
Verification of randomized consensus algorithms under round-rigid adversaries.
Int. J. Softw. Tools Technol. Transf.
Nathalie Bertrand, Igor Konnov, Marijana Lazic, Josef Widder
2020 B ed.
31st International Conference on Concurrency Theory, CONCUR 2020, Vienna, Austria (Virtual Conference), September 1-4, 2020
CONCUR
Igor Konnov, Laura Kovács
2020 J jnl
A Tendermint Light Client.
CoRR
Sean Braithwaite, Ethan Buchman, Ismail Khoffi, Igor Konnov, Zarko Milosevic, Romain Ruetschi, Josef Widder
2020 — conf
Cutoffs for Symmetric Point-to-Point Distributed Algorithms.
NETYS
Thanh-Hai Tran, Igor Konnov, Josef Widder
2020 B conf
Eliminating Message Counters in Threshold Automata.
ATVA
Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger
2020 J jnl
Extracting symbolic transitions from TLA
Sci. Comput. Program.
Jure Kukovec, Thanh-Hai Tran, Igor Konnov
2020 — conf
Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper).
FMBC@CAV
Sean Braithwaite, Ethan Buchman, Igor Konnov, Zarko Milosevic, Ilina Stoilkovska, Josef Widder, Anca Zamfir
2020 J jnl
Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker.
CoRR
Igor Konnov, Marijana Lazic, Ilina Stoilkovska, Josef Widder
2020 — conf
Tendermint Blockchain Synchronization: Formal Specification and Model Checking.
ISoLA (1)
Sean Braithwaite, Ethan Buchman, Igor Konnov, Zarko Milosevic, Ilina Stoilkovska, Josef Widder, Anca Zamfir
2020 C conf
Tutorial: Parameterized Verification with Byzantine Model Checker.
FORTE
Igor Konnov, Marijana Lazic, Ilina Stoilkovska, Josef Widder
2019 J jnl
Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (eds): Handbook of model checking - Springer International Publishing AG, Cham, Switzerland, 2018.
Formal Aspects Comput.
Igor Konnov
2019 J jnl
TLA+ model checking made symbolic.
Proc. ACM Program. Lang.
Igor Konnov, Jure Kukovec, Thanh-Hai Tran
2019 B conf
Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries.
CONCUR
Nathalie Bertrand, Igor Konnov, Marijana Lazic, Josef Widder
2019 — conf
Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking.
TACAS (2)
Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger
2018 — conf
ByMC: Byzantine Model Checker.
ISoLA (3)
Igor Konnov, Josef Widder
2018 C conf
Extracting Symbolic Transitions from TLA
ABZ
Jure Kukovec, Thanh-Hai Tran, Igor Konnov
2018 B conf
Reachability in Parameterized Systems: All Flavors of Threshold Automata.
CONCUR
Jure Kukovec, Igor Konnov, Josef Widder
2017 J jnl
Para
Formal Methods Syst. Des.
Igor Konnov, Marijana Lazic, Helmut Veith, Josef Widder
2017 B conf
Synthesis of Distributed Algorithms with Parameterized Threshold Guards.
OPODIS
Marijana Lazic, Igor Konnov, Josef Widder, Roderick Bloem
2016 J jnl
A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms.
CoRR
Igor Konnov, Marijana Lazic, Helmut Veith, Josef Widder
2016 J jnl
Decidability in Parameterized Verification.
SIGACT News
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder
2015 — book
Decidability of Parameterized Verification
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder
2015 — conf
SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms.
CAV (1)
Igor Konnov, Helmut Veith, Josef Widder
2014 B conf
On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability.
CONCUR
Igor Konnov, Helmut Veith, Josef Widder
2014 — conf
Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms.
SFM
Annu Gmeiner, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
2013 A* conf
Brief announcement: parameterized model checking of fault-tolerant distributed algorithms by abstraction.
PODC
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
2013 B conf
Parameterized model checking of fault-tolerant distributed algorithms by abstraction.
FMCAD
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
2013 — conf
Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms.
SPIN
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
2012 J jnl
Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms
CoRR
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
2012 J jnl
Starting a Dialog between Model Checking and Fault-tolerant Distributed Algorithms
CoRR
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
2010 — conf
CheAPS: a Checker of Asynchronous Parameterized Systems.
WING@ETAPS/IJCAR
Igor Konnov