# Publications by Igor Konnov

2020 | |

[59] | Extracting symbolic transitions from TLA+ specificationsScience of Computer Programming, volume 187, pages 102361, 2020. |

2019 | |

[58] | Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries30th International Conference on Concurrency Theory (CONCUR 2019) (Wan Fokkink, Rob van Glabbeek, eds.), volume 140 of Leibniz International Proceedings in Informatics (LIPIcs), pages 33:1–33:15, 2019, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. |

[57] | Verifying Safety of Synchronous Fault-Tolerant Algorithms Bounded Model CheckingTools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part II, pages 357–374, 2019.Note: A pre-print including the proofs is available at: https://hal.inria.fr/hal-01925653 |

[56] | TLA+ model checking made symbolicPACMPL, volume 3, number OOPSLA, pages 123:1–123:30, 2019. |

2018 | |

[55] | Verification of Randomized Distributed Algorithms under Round-Rigid AdversariesHAL, volume hal-01925533, Nov 2018. |

[54] | Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model CheckingHAL, volume hal-01925653, Nov 2018.Note: Accepted at TACAS 2019 |

[53] | ByMC: Byzantine Model CheckerLeveraging Applications of Formal Methods, Verification and Validation. Distributed Systems, pages 327–342, 2018, Springer International Publishing. |

[52] | Extracting Symbolic Transitions from TLA+ SpecificationsAbstract State Machines, Alloy, B, TLA, VDM, and Z, pages 89–104, 2018. |

[51] | Reachability in Parameterized Systems: All Flavors of Threshold Automata29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, pages 19:1–19:17, 2018. |

2017 | |

[50] | Synthesis of Distributed Algorithms with Parameterized Threshold GuardsOPODIS, volume 95 of LIPIcs, pages 32:1–32:20, 2017. |

[49] | Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed AlgorithmsVerification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, pages 347–366, 2017. |

[48] | On the completeness of bounded model checking for threshold-based distributed algorithms: ReachabilityInformation and Computation, volume 252, pages 95–109, 2017. |

[47] | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithmsProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 719–734, 2017.Note: A pre-print including the proofs is available at http://arxiv.org/abs/1608.05327 |

[46] | Para^2: Parameterized Path Reduction, Acceleration, and SMT for Reachability in Threshold-Guarded Distributed AlgorithmsFormal Methods in System Design, volume 51, number 2, pages 270–307, 2017, Springer. |

2016 | |

[45] | Decidability of Parameterized VerificationACM SIGACT News, volume 47, number 2, pages 53–64, jun 2016. |

[44] | Parameterized Systems in BIP: Design and Model Checking27th International Conference on Concurrency Theory (CONCUR 2016) (Josée Desharnais, Radha Jagadeesan, eds.), volume 59 of Leibniz International Proceedings in Informatics (LIPIcs), pages 30:1–30:16, 2016, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. |

[43] | What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed AlgorithmsPerspectives of System Informatics: 10th International Andrei Ershov Informatics Conference, PSI 2015, in Memory of Helmut Veith, Kazan and Innopolis, Russia, August 24-27, 2015, Revised Selected Papers (Manuel Mazzara, Andrei Voronkov, eds.), volume 9609 of LNCS, pages 6–21, 2016, Springer International Publishing. |

[42] | A Short Counterexample Property for Safety and Liveness Verification of Fault-Tolerant Distributed AlgorithmsarXiv/CoRR, volume 1608.05327, 2016.Note: (accepted to POPL 2017) |

2015 | |

[41] | Decidability of Parameterized Verification pages 170, 2015. |

[40] | A Combined Toolset for the Verification of Real-Time Distributed SystemsProgramming and Computer Software, volume 41, number 6, pages 325–335, 2015. |

[39] | SMT and POR beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed AlgorithmsCAV (Part I), volume 9206 of LNCS, pages 85–102, 2015. |

2014 | |

[38] | How to Make a Simple Tool for Verification of Real-Time SystemsAutomatic Control and Computer Sciences, volume 48, number 7, pages 534–542, 2014, Allerton Press. |

[37] | On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability Chapter in CONCUR 2014 — Concurrency Theory (Paolo Baldan, Daniele Gorla, eds.), volume 8704 of Lecture Notes in Computer Science, pages 125-140, 2014. |

[36] | Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed AlgorithmsFormal Methods for Executable Software Models, pages 122–171, 2014, Springer. |

2013 | |

[35] | Parameterized model checking of fault-tolerant distributed algorithms by abstractionFMCAD, pages 201–209, 2013. |

[34] | Towards Modeling and Model Checking Fault-Tolerant Distributed AlgorithmsSPIN, volume 7976 of LNCS, pages 209–226, 2013. |

[33] | An experience on using simulation environment DYANA augmented with UPPAAL for verification of embedded systems defined by UML statecharts 2013, CAV Workshop VES13. |

[32] | Brief announcement: parameterized model checking of fault-tolerant distributed algorithms by abstractionPODC, pages 119–121, 2013. |

2012 | |

[31] | Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed AlgorithmsArXiv e-prints, October 2012. |

[30] | Starting a Dialog between Model Checking and Fault-tolerant Distributed AlgorithmsArXiv e-prints, October 2012. |

[29] | Who is afraid of Model Checking Distributed Algorithms? 2012, CAV Workshop (EC)\^2. |

[28] | Parameterized Model Checking by Network Invariants: the Asynchronous Case 2012, LICS Workshop AISS. |

2011 | |

[27] | An Invariant-Based Approach to the Verification of Asynchronous Parameterized Networks 2011, Talk at Concurrency Seminar, Oxford Computing Laboratory, Oxford, February, 2011. |

[26] | Two Techniques of Parameterized Model Checking and Symmetry Reduction 2011, Talk at the ARiSE seminar, April 21, 2011. |

[25] | On the Choice of a Simulation Run-Time Infrastructure based on High-Level Architecture17th International Conference on Computational Mechanics and Contemporary Application Software Systems 2011 (VMSPPS'2011), Alushta, Ukraine, pages 36-38, 2011. |

2010 | |

[24] | Using Adaptive Symmetry Reduction for LTL Model CheckingInternational Workshop on Program Semantics, Specification and Verification (PSSV 2010) affiliated with CSR 2010, pages 5-11, 2010.Note: Available as http://lvk.cs.msu.su/ konnov/publications/k10_cheaps_abstract.pdf |

[23] | Using Adaptive Symmetry Reduction for LTL Model CheckingModelling and Analysis of Information Systems (Modelirovanie i analiz informacionnih system), volume 17, number 4, pages 78-87, 2010. |

[22] | An invariant-based approach to the verification of asynchronous parameterized networksJ. Symb. Comput., volume 45, number 11, pages 1144-1162, 2010.Note: A draft is also available as http://lvk.cs.msu.su/ konnov/publications/kz09_jsc_invariant_draft.pdf |

[21] | Model Checking GARP Protocol using Spin and VRSInternational Workshop on Automata, Algorithms, and Information Technologies, 2010.Note: Available as http://lvk.cs.msu.su/ konnov/publications/kl10_garp_presentation.pdf |

[20] | CheAPS: a Checker of Asynchronous Parameterized SystemsThird International Workshop on Invariant Generation (WING 2010) affiliated with IJCAR at FLoC 2010, 2010.Note: Available as http://lvk.cs.msu.su/ konnov/publications/k10_cheaps_abstract.pdf and http://lvk.cs.msu.su/ konnov/publications/k10_cheaps_presentation.pdf |

[19] | On application of weaker simulations to parameterized model checking by network invariants techniqueAutomatic Control and Computer Sciences, volume 44, number 7, pages 378-386, 2010.Note: A draft is also available as http://lvk.cs.msu.su/ konnov/publications/k08_mais_en.pdf |

2009 | |

[18] | Comparison of Spin and VRS on the model of Generic Attribute Registration Protocol 2009, Talk at the INTAS 05-1000008-8144 meeting, Linz, February 2009. |

[17] | CheAPS: Parameterized Model Checking Tool 2009, Joint Workshop of Microsoft Research and Institute for System Programming Russian Academy of Sciences, Moscow, June 2009. |

[16] | Application of CHEAPS System to Parameterized Model Checking of Distributed SystemsTrudy 3 Vserossiiskoi Nauchnoi Konferentsii Metody i Sredstva Obrabotki Informatsii (Proc. 3rd All-Russia Conf. on Methods and Techniques of Information Processing), pages 116-122, 2009.Note: Available as http://lvk.cs.msu.su/ ashalimov/doc/MCO09_-_part1.pdf |

2008 | |

[15] | Parameterized Model Checking of Distributed Systems pages 1–198, November 2008, PhD thesis, Lomonosov Moscow State University, Faculty of Computational Mathematics and Cybernetics. Note: Candidate of Sciences in Physics and Mathematics 05.13.11 (PhD in CS) |

[14] | Teachable Static Analysis Workbench 2008, OWASP EU Summit 3-8 November 2008, Albufeira, Portugal, 2008. |

[13] | Using Adaptive Symmetry Reduction for LTL Model CheckingModelling and Analysis of Information Systems (Modelirovanie i analiz informacionnih system), volume 15, number 3, pages 3-13, 2008.Note: The English translation is available as http://dx.doi.org/10.3103/S0146411610070035 |

[12] | On Optimizing Computation of Semi-block Simulation 2008, Talk at the INTAS 05-1000008-8144 meeting, Kiev, May 2008. |

[11] | The system for verfication of parameterized models of asynchronous distributed systems (CHEAPS)Proc. 5th All-Russia Scientific and Technical Conf. Tehnologii Microsoft v teorii i praktike programmirovaniya (Microsoft technologies in theory and practice of programming), 2008. |

[10] | Static analysis for security of web applications developed in PythonProc. 5th All-Russia Scientific and Technical Conf. Tehnologii Microsoft v teorii i praktike programmirovaniya (Microsoft technologies in theory and practice of programming), 2008. |

2007 | |

[9] | An Invariant-based Approach to the Verification of Asynchronous Parameterized NetworksInternational Workshop on Invariant Generation (WING'07), pages 41-55, 2007.Note: Available as http://www.risc.uni-linz.ac.at/publications/download/risc_3128/proceedings.pdf and http://lvk.cs.msu.su/ konnov/publications/kz07_wing.pdf |

[8] | Parameterized Model Checking of Resource Reservation Protocol 2007, Talk at the INTAS 05-1000008-8144 meeting, Moscow, August 2007. |

2006 | |

[7] | On the verification of asynchronous parameterized networks of communicating processes by model checkingMathemathical Methods and Algorithms, ISP RAS, pages 37-58, 2006.Note: Also available as http://lvk.cs.msu.su/ konnov/publications/kz07_sim.pdf |

[6] | On Verification of Parameterized Distributed Systems 2006, Talk at the INTAS 05-1000008-8144 meeting, Timisoara, December 2006. |

[5] | Applying game theory to computing simulations on labelled transition systems7th International Conf. on Discrete models of control systems, 2006. |

[4] | Computing (bi)simulation relations preserving CTL*_X for ordinary and fair Kripke structuresMathemathical Methods and Algorithms, ISP RAS, pages 59-76, 2006.Note: Also available as http://lvk.cs.msu.su/ konnov/publications/bkz07_games.pdf |

2005 | |

[3] | On the Verification of Asynchronous Parameterized Distributed ProgramsTrudy 2 Vserossiiskoi Nauchnoi Konferentsii Metody i Sredstva Obrabotki Informatsii (Proc. 2nd All-Russia Conf. on Methods and Techniques of Information Processing), Moscow, pages 267-372, 2005.Note: Available as http://lvk.cs.msu.su/ konnov/publications/kz05-pmc.pdf |

[2] | An Approach to the Verification of Symmetric Parameterized Distributed SystemsProgramming and Computer Software, volume 31, number 5, pages 225-236, 2005.Note: A draft is also available as http://lvk.cs.msu.su/ konnov/publications/kz05-prog-pmc-draft.pdf |

2003 | |

[1] | On the Verification of Parameterized Symmetric Distributed ProgramsTrudy 1 Vserossiiskoi Nauchnoi Konferentsii Metody i Sredstva Obrabotki Informatsii (Proc. 1st All-Russia Conf. on Methods and Techniques of Information Processing), Moscow, pages 395-400, 2003.Note: Available as http://lvk.cs.msu.su/ konnov/publications/kz03-pmc.pdf |