Publications by Igor Konnov

2017
[49] Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms
Igor V. Konnov, Josef Widder, Francesco Spegni, Luca Spalazzi
Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, pages 347-366, 2017.
[bibtex] [pdf] [doi]
[48] On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability
Igor V. Konnov, Helmut Veith, Josef Widder
Information and Computation, volume 252, pages 95-109, 2017.
[bibtex] [pdf] [doi]
[47] A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
Igor V. Konnov, Marijana Lazic, Helmut Veith, Josef Widder
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
[bibtex] [pdf]
[46]Para^2: Parameterized Path Reduction, Acceleration, and SMT for Reachability in Threshold-Guarded Distributed Algorithms
Igor Konnov, Marijana Lazic, Helmut Veith, Josef Widder
Formal Methods in System Design, 2017, Springer.
Note: to appear
[bibtex]
2016
[45] Decidability of Parameterized Verification
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder
ACM SIGACT News, volume 47, number 2, pages 53-64, jun 2016.
[bibtex] [pdf]
[44] Parameterized Systems in BIP: Design and Model Checking
Igor Konnov, Tomer Kotek, Qiang Wang, Helmut Veith, Simon Bliudze, Joseph Sifakis
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.
[bibtex] [pdf]
[43] What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms
Igor Konnov, Helmut Veith, Josef Widder
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.
[bibtex] [pdf]
[42] A Short Counterexample Property for Safety and Liveness Verification of Fault-Tolerant Distributed Algorithms
Igor Konnov, Marijana Lazic, Helmut Veith, Josef Widder
arXiv/CoRR, volume 1608.05327, 2016.
Note: (accepted to POPL 2017)
[bibtex] [pdf]
2015
[41] Decidability of Parameterized Verification
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder
pages 170, 2015.
[bibtex] [pdf] [doi]
[40]A Combined Toolset for the Verification of Real-Time Distributed Systems
D.Yu. Volkanov, V.A. Zakharov, D.A. Zorin, V.V. Podymov, I.V. Konnov
Programming and Computer Software, volume 41, number 6, pages 325-335, 2015.
[bibtex] [doi]
[39] SMT and POR beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms
Igor Konnov, Helmut Veith, Josef Widder
CAV (Part I), volume 9206 of LNCS, pages 85-102, 2015.
[bibtex] [pdf]
2014
[38]How to Make a Simple Tool for Verification of Real-Time Systems
I.V. Konnov, V.V. Podymov, D.Yu. Volkanov, V.A. Zakharov, D.A. Zorin
Automatic Control and Computer Sciences, volume 48, number 7, pages 534-542, 2014, Allerton Press.
[bibtex] [doi]
[37] On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability
Igor Konnov, Helmut Veith, Josef Widder
Chapter in CONCUR 2014 --- Concurrency Theory (Paolo Baldan, Daniele Gorla, eds.), volume 8704 of Lecture Notes in Computer Science, pages 125-140, 2014.
[bibtex] [pdf]
[36] Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms
Annu Gmeiner, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
Formal Methods for Executable Software Models, pages 122-171, 2014, Springer.
[bibtex] [pdf]
2013
[35] Parameterized model checking of fault-tolerant distributed algorithms by abstraction
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
FMCAD, pages 201-209, 2013.
[bibtex] [pdf]
[34] Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
SPIN, volume 7976 of LNCS, pages 209-226, 2013.
[bibtex] [pdf]
[33] An experience on using simulation environment DYANA augmented with UPPAAL for verification of embedded systems defined by UML statecharts
Alevtina B. Glonina, Igor Konnov, Vladislav V. Podymov, Dmitry Yu. Volkanov, Vladimir A. Zakharov, Daniil A. Zorin
2013, CAV Workshop VES13.
[bibtex] [pdf]
[32] Brief announcement: parameterized model checking of fault-tolerant distributed algorithms by abstraction
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
PODC, pages 119-121, 2013.
[bibtex] [pdf]
2012
[31] Starting a Dialog between Model Checking and Fault-tolerant Distributed Algorithms
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
ArXiv e-prints, October 2012.
[bibtex] [pdf]
[30] Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
ArXiv e-prints, October 2012.
[bibtex] [pdf]
[29] Who is afraid of Model Checking Distributed Algorithms?
Igor Konnov, Helmut Veith, Josef Widder
2012, CAV Workshop (EC)\^2.
[bibtex] [pdf]
[28] Parameterized Model Checking by Network Invariants: the Asynchronous Case
Igor Konnov
2012, LICS Workshop AISS.
[bibtex] [pdf]
2011
[27]An Invariant-Based Approach to the Verification of Asynchronous Parameterized Networks
Igor V. Konnov
2011, Talk at Concurrency Seminar, Oxford Computing Laboratory, Oxford, February, 2011.
[bibtex]
[26]Two Techniques of Parameterized Model Checking and Symmetry Reduction
Igor V. Konnov
2011, Talk at the ARiSE seminar, April 21, 2011.
[bibtex]
[25]On the Choice of a Simulation Run-Time Infrastructure based on High-Level Architecture
Vitaly V. Antonenko, Igor V. Konnov
17th International Conference on Computational Mechanics and Contemporary Application Software Systems 2011 (VMSPPS'2011), Alushta, Ukraine, pages 36-38, 2011.
[bibtex]
2010
[24]Using Adaptive Symmetry Reduction for LTL Model Checking
Igor V. Konnov, Vladimir A. Zakharov
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
[bibtex]
[23]Using Adaptive Symmetry Reduction for LTL Model Checking
Igor V. Konnov, Vladimir A. Zakharov
Modelling and Analysis of Information Systems (Modelirovanie i analiz informacionnih system), volume 17, number 4, pages 78-87, 2010.
[bibtex]
[22]An invariant-based approach to the verification of asynchronous parameterized networks
Igor V. Konnov, Vladimir A. Zakharov
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
[bibtex]
[21]Model Checking GARP Protocol using Spin and VRS
Igor V. Konnov, Oleksandr A. Letichevsky Jr.
International Workshop on Automata, Algorithms, and Information Technologies, 2010.
Note: Available as http://lvk.cs.msu.su/ konnov/publications/kl10_garp_presentation.pdf
[bibtex]
[20]CheAPS: a Checker of Asynchronous Parameterized Systems
Igor V. Konnov
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
[bibtex]
[19]On application of weaker simulations to parameterized model checking by network invariants technique
I. V. Konnov
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
[bibtex]
2009
[18] Comparison of Spin and VRS on the model of Generic Attribute Registration Protocol
Igor V. Konnov, Oleksandr A. Letichevsky
2009, Talk at the INTAS 05-1000008-8144 meeting, Linz, February 2009.
[bibtex] [pdf]
[17]CheAPS: Parameterized Model Checking Tool
Igor V. Konnov
2009, Joint Workshop of Microsoft Research and Institute for System Programming Russian Academy of Sciences, Moscow, June 2009.
[bibtex]
[16]Application of CHEAPS System to Parameterized Model Checking of Distributed Systems
Igor V. Konnov
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
[bibtex]
2008
[15] Parameterized Model Checking of Distributed Systems
Igor V. Konnov
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)
[bibtex] [pdf]
[14]Teachable Static Analysis Workbench
Dmitry D. Kozlov, Igor V. Konnov
2008, OWASP EU Summit 3-8 November 2008, Albufeira, Portugal, 2008.
[bibtex]
[13]Using Adaptive Symmetry Reduction for LTL Model Checking
Igor V.Konnov, Vladimir A.Zakharov
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
[bibtex]
[12] On Optimizing Computation of Semi-block Simulation
Igor V. Konnov
2008, Talk at the INTAS 05-1000008-8144 meeting, Kiev, May 2008.
[bibtex] [pdf]
[11]The system for verfication of parameterized models of asynchronous distributed systems (CHEAPS)
Igor V. Konnov
Proc. 5th All-Russia Scientific and Technical Conf. Tehnologii Microsoft v teorii i praktike programmirovaniya (Microsoft technologies in theory and practice of programming), 2008.
[bibtex]
[10]Static analysis for security of web applications developed in Python
Georgy A. Klimov, Dmitry D. Kozlov, Igor V. Konnov
Proc. 5th All-Russia Scientific and Technical Conf. Tehnologii Microsoft v teorii i praktike programmirovaniya (Microsoft technologies in theory and practice of programming), 2008.
[bibtex]
2007
[9]An Invariant-based Approach to the Verification of Asynchronous Parameterized Networks
Vladimir Zakharov, Igor Konnov
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
[bibtex]
[8] Parameterized Model Checking of Resource Reservation Protocol
Igor V. Konnov
2007, Talk at the INTAS 05-1000008-8144 meeting, Moscow, August 2007.
[bibtex] [pdf]
2006
[7]On the verification of asynchronous parameterized networks of communicating processes by model checking
I.V. Konnov, V.A. Zakharov
Mathemathical Methods and Algorithms, ISP RAS, pages 37-58, 2006.
Note: Also available as http://lvk.cs.msu.su/ konnov/publications/kz07_sim.pdf
[bibtex]
[6] On Verification of Parameterized Distributed Systems
Igor V. Konnov
2006, Talk at the INTAS 05-1000008-8144 meeting, Timisoara, December 2006.
[bibtex] [pdf]
[5]Applying game theory to computing simulations on labelled transition systems
Peter E. Bulychev, Vladimir A. Zakharov, Igor V. Konnov
7th International Conf. on Discrete models of control systems, 2006.
[bibtex]
[4]Computing (bi)simulation relations preserving CTL*_X for ordinary and fair Kripke structures
P.E. Bulychev, I. V. Konnov, V. A. Zakharov
Mathemathical Methods and Algorithms, ISP RAS, pages 59-76, 2006.
Note: Also available as http://lvk.cs.msu.su/ konnov/publications/bkz07_games.pdf
[bibtex]
2005
[3]On the Verification of Asynchronous Parameterized Distributed Programs
Vladimir A. Zakharov, Igor V. Konnov
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
[bibtex]
[2]An Approach to the Verification of Symmetric Parameterized Distributed Systems
Igor V. Konnov, Vladimir A. Zakharov
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
[bibtex]
2003
[1]On the Verification of Parameterized Symmetric Distributed Programs
Igor V. Konnov, Vladimir A. Zakharov
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
[bibtex]

Latest News

Helmut Veith Stipend 2017: Deadline Extension (November 30)

The application deadline for the Helmut Veith Stipend 2017 has been extended to November 30. The stipend is dedicated to the memory of an outstanding computer scientist who worked in the fields of logic in computer science, computer-aided verification, software engineering, and computer security. We encourage all female master’s students attending (or planning to attend) […]

Continue reading

Helmut Veith Stipend 2017

Outstanding female students in the field of computer science who pursue (or plan to pursue) one of the master‘s programs in Computer Science at TU Wien taught in English are invited to apply for the Helmut Veith Stipend

Continue reading

Helmut Veith Stipend

The first recipient of the Helmut Veith Stipend for excellent female master’s students in computer science will be presented on March 14 at the following event: "More female students in computer science. Who cares?" Panel discussion with renowned scientists about diversity in STEM Studies March 14, 5:30pm, TU Wien The Helmut Veith Stipend is dedicated […]

Continue reading

WAIT 2016 in Vienna

The third WAIT workshop on induction is held between 17-18 November at the TU Wien. Details are available on the workshop page.

Continue reading

Full news archive