Publications HAL

2021

Preprints, Working Papers, ...

titre
Compositional Verification of Byzantine Consensus
auteur
Nathalie Bertrand, Vincent Gramoli, Igor Konnov, Marijana Lazic, Pierre Tholoniat, Josef Widder
article
2021
Accès au texte intégral et bibtex
https://hal.science/hal-03158911/file/paper.pdf BibTex

2019

Journal articles

titre
TLA+ Model Checking Made Symbolic
auteur
Igor Konnov, Jure Kukovec, Thanh-Hai Tran
article
Proceedings of the ACM on Programming Languages, 2019, 3 (OOPSLA), pp.123:1--123:30. ⟨10.1145/3360549⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02280888/file/camera.pdf BibTex
titre
Handbook of Model Checking by Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (eds), published by Springer International Publishing AG, Cham, Switzerland, 2018.
auteur
Igor Konnov
article
Formal Aspects of Computing, 2019, pp.455-456. ⟨10.1007/s00165-019-00486-z⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02398334/file/review-igor.pdf BibTex

Conference papers

titre
Verification of Randomized Consensus Algorithms under Round-Rigid Adversaries
auteur
Nathalie Bertrand, Igor Konnov, Marijana Lazic, Josef Widder
article
CONCUR 2019 - 30th International Conference on Concurrency Theory, Aug 2019, Amsterdam, Netherlands. pp.1-16, ⟨10.4230/LIPIcs.CONCUR.2019.33⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02191348/file/main.pdf BibTex
titre
Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking
auteur
Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger
article
TACAS 2019 - International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr 2019, Prague, Czech Republic. ⟨10.1007/978-3-030-17465-1_20⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01925653/file/Stoilkovska2019_Chapter_VerifyingSafetyOfSynchronousFa%20%281%29.pdf BibTex

Preprints, Working Papers, ...

titre
Verification of Randomized Distributed Algorithms under Round-Rigid Adversaries
auteur
Nathalie Bertrand, Igor Konnov, Marijana Lazic, Josef Widder
article
2019
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01925533/file/main.pdf BibTex

2018

Conference papers

titre
ByMC: Byzantine Model Checker
auteur
Igor Konnov, Josef Widder
article
ISoLA 2018 - 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Oct 2018, Limassol, Cyprus. pp.327-342, ⟨10.1007/978-3-030-03424-5_22⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01909653/file/camera.pdf BibTex
titre
Reachability in Parameterized Systems: All Flavors of Threshold Automata
auteur
Jure Kukovec, Igor Konnov, Josef Widder
article
CONCUR 2018 - 29th International Conference on Concurrency Theory, Sep 2018, Beijing, China. ⟨10.4230/LIPIcs.CONCUR.2018.19⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01871142/file/LIPIcs-CONCUR-2018-19.pdf BibTex
titre
Extracting Symbolic Transitions from $TLA+$ Specifications
auteur
Jure Kukovec, Thanh-Hai Tran, Igor Konnov
article
Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2018, Jun 2018, Southampton, United Kingdom. pp.89-104, ⟨10.1007/978-3-319-91271-4_7⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01871131/file/camera.pdf BibTex

Documents associated with scientific events

titre
BmcMT: Bounded Model Checking of TLA + Specifications with SMT
auteur
Igor Konnov, Jure Kukovec, Thanh Hai Tran
article
TLA+ Community Meeting 2018, Jul 2018, Oxford, United Kingdom
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01899719/file/kkt18-bmcmt.pdf BibTex
titre
Model Checking of Fault-Tolerant Distributed Algorithms: from Classics towards Contemporary
auteur
Igor Konnov, Stephan Merz
article
BCRB 2018 - DSN Workshop on Byzantine Consensus and Resilient Blockchains, Jun 2018, Luxembourg, Luxembourg
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01899723/file/main.pdf BibTex