Igor Konnov

Orcid: 0000-0001-6629-3377

Affiliations:
  • Informal Systems, Vinna, Austria
  • INRIA Nancy, France (former)
  • TU Wien, Vienna, Austria (former)
  • Lomonosov Moscow State University, Russia (PhD 2008)


According to our database1, Igor Konnov authored at least 44 papers between 2005 and 2023.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2023
A case study on parametric verification of failure detectors.
Log. Methods Comput. Sci., 2023

Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker.
Log. Methods Comput. Sci., 2023

Symbolic Model Checking for TLA+ Made Faster.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

2022
Verifying safety of synchronous fault-tolerant algorithms by bounded model checking.
Int. J. Softw. Tools Technol. Transf., 2022

Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS.
CoRR, 2022

Holistic Verification of Blockchain Consensus.
Proceedings of the 36th International Symposium on Distributed Computing, 2022

Brief Announcement: Holistic Verification of Blockchain Consensus.
Proceedings of the PODC '22: ACM Symposium on Principles of Distributed Computing, Salerno, Italy, July 25, 2022

Specification and Verification with the TLA<sup>+</sup> Trifecta: TLC, Apalache, and TLAPS.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles, 2022

2021
Correction to: Verification of randomized consensus algorithms under round-rigid adversaries.
Int. J. Softw. Tools Technol. Transf., 2021

Verification of randomized consensus algorithms under round-rigid adversaries.
Int. J. Softw. Tools Technol. Transf., 2021

Eliminating Message Counters in Synchronous Threshold Automata.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2021

2020
Extracting symbolic transitions from TLA<sup>+</sup> specifications.
Sci. Comput. Program., 2020

A Tendermint Light Client.
CoRR, 2020

Cutoffs for Symmetric Point-to-Point Distributed Algorithms.
Proceedings of the Networked Systems - 8th International Conference, 2020

Tendermint Blockchain Synchronization: Formal Specification and Model Checking.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, 2020

Tutorial: Parameterized Verification with Byzantine Model Checker.
Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2020

Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper).
Proceedings of the 2nd Workshop on Formal Methods for Blockchains, 2020

Eliminating Message Counters in Threshold Automata.
Proceedings of the Automated Technology for Verification and Analysis, 2020

2019
TLA+ model checking made symbolic.
Proc. ACM Program. Lang., 2019

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., 2019

2018
ByMC: Byzantine Model Checker.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems, 2018

Reachability in Parameterized Systems: All Flavors of Threshold Automata.
Proceedings of the 29th International Conference on Concurrency Theory, 2018

2017
On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability.
Inf. Comput., 2017

Para<sup>2</sup>: parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms.
Formal Methods Syst. Des., 2017

Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2017

A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms.
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

Synthesis of Distributed Algorithms with Parameterized Threshold Guards.
Proceedings of the 21st International Conference on Principles of Distributed Systems, 2017

2016
Decidability in Parameterized Verification.
SIGACT News, 2016

Parameterized Systems in BIP: Design and Model Checking.
Proceedings of the 27th International Conference on Concurrency Theory, 2016

2015
Decidability of Parameterized Verification
Synthesis Lectures on Distributed Computing Theory, Morgan & Claypool Publishers, ISBN: 978-3-031-02011-7, 2015

A combined toolset for the verification of real-time distributed systems.
Program. Comput. Softw., 2015

What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms.
Proceedings of the Perspectives of System Informatics, 2015

SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014
How to make a simple tool for verification of real-time systems.
Autom. Control. Comput. Sci., 2014

Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms.
Proceedings of the Formal Methods for Executable Software Models, 2014

2013
Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms.
Proceedings of the Model Checking Software - 20th International Symposium, 2013

Brief announcement: parameterized model checking of fault-tolerant distributed algorithms by abstraction.
Proceedings of the ACM Symposium on Principles of Distributed Computing, 2013

Parameterized model checking of fault-tolerant distributed algorithms by abstraction.
Proceedings of the Formal Methods in Computer-Aided Design, 2013

2012
Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms
CoRR, 2012

Starting a Dialog between Model Checking and Fault-tolerant Distributed Algorithms
CoRR, 2012

2010
An invariant-based approach to the verification of asynchronous parameterized networks.
J. Symb. Comput., 2010

On application of weaker simulations to parameterized model checking by network invariants technique.
Autom. Control. Comput. Sci., 2010

CheAPS: a Checker of Asynchronous Parameterized Systems.
Proceedings of the Second International Workshop on Invariant Generation, 2010

2005
An Approach to the Verification of Symmetric Parameterized Distributed Systems.
Program. Comput. Softw., 2005


  Loading...