Publications by Igor Konnov
| 2020 | |
| [60] | Extracting symbolic transitions from TLA+ specifications Science of Computer Programming, volume 187, pages 102361, 2020. |
| [59] | Tutorial: Parameterized Verification with Byzantine Model Checker FORTE 2020, pages 189–207, 2020. |
| 2019 | |
| [58] | Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries 30th 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 Checking Tools 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 symbolic PACMPL, volume 3, number OOPSLA, pages 123:1–123:30, 2019. |
| 2018 | |
| [55] | Verification of Randomized Distributed Algorithms under Round-Rigid Adversaries HAL, volume hal-01925533, Nov 2018. |
| [54] | Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking HAL, volume hal-01925653, Nov 2018. Note: Accepted at TACAS 2019 |
| [53] | ByMC: Byzantine Model Checker Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems, pages 327–342, 2018, Springer International Publishing. |
| [52] | Extracting Symbolic Transitions from TLA+ Specifications Abstract State Machines, Alloy, B, TLA, VDM, and Z, pages 89–104, 2018. |
| [51] | Reachability in Parameterized Systems: All Flavors of Threshold Automata 29th 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 Guards OPODIS, volume 95 of LIPIcs, pages 32:1–32:20, 2017. |
| [49] | Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms Verification, 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: Reachability Information and Computation, volume 252, pages 95–109, 2017. |
| [47] | 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, 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 Algorithms Formal Methods in System Design, volume 51, number 2, pages 270–307, 2017, Springer. |
| 2016 | |
| [45] | Decidability of Parameterized Verification ACM SIGACT News, volume 47, number 2, pages 53–64, jun 2016. |
| [44] | Parameterized Systems in BIP: Design and Model Checking 27th 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 Algorithms Perspectives 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 Algorithms arXiv/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 Systems Programming 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 Algorithms CAV (Part I), volume 9206 of LNCS, pages 85–102, 2015. |
| 2014 | |
| [38] | How to Make a Simple Tool for Verification of Real-Time Systems Automatic 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 Algorithms Formal Methods for Executable Software Models, pages 122–171, 2014, Springer. |
| 2013 | |
| [35] | Parameterized model checking of fault-tolerant distributed algorithms by abstraction FMCAD, pages 201–209, 2013. |
| [34] | Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms SPIN, 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 abstraction PODC, pages 119–121, 2013. |
| 2012 | |
| [31] | Starting a Dialog between Model Checking and Fault-tolerant Distributed Algorithms ArXiv e-prints, October 2012. |
| [30] | Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms ArXiv 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 Architecture 17th 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 Checking International 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 Checking Modelling 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 networks J. 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 VRS International 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 Systems Third 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 technique Automatic 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 Systems Trudy 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 Checking Modelling 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 Python Proc. 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 Networks International 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 checking Mathemathical 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 systems 7th International Conf. on Discrete models of control systems, 2006. |
| [4] | Computing (bi)simulation relations preserving CTL*_X for ordinary and fair Kripke structures Mathemathical 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 Programs Trudy 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 Systems Programming 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 Programs Trudy 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 |
