32 citations · 85 across the 18 of their papers we have counts for
20 papers
Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS
Igor Konnov, Markus Kuppe, Stephan Merz
Using an algorithm due to Safra for distributed termination detection as a running example, we present the main tools for verifying specifications written in TLA+. Examining their…
Holistic Verification of Blockchain Consensus
Nathalie Bertrand, Vincent Gramoli, Igor Konnov +3
Blockchain has recently attracted the attention of the industry due, in part, to its ability to automate asset transfers. It requires distributed participants to reach a consensus…
Primal-Dual Method for Optimization Problems with Changing Constraints
Igor Konnov
We propose a modified primal-dual method for general convex optimization problems with changing constraints. We obtain properties of Lagrangian saddle points for these problems whi…
A case study on parametric verification of failure detectors
Thanh-Hai Tran, Igor Konnov, Josef Widder
Partial synchrony is a model of computation in many distributed algorithms and modern blockchains. These algorithms are typically parameterized in the number of participants, and t…
Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
Igor Konnov, Marijana Lazić, Ilina Stoilkovska +1
Threshold guards are a basic primitive of many fault-tolerant algorithms that solve classical problems in distributed computing, such as reliable broadcast, two-phase commit, and c…
A Tendermint Light Client
Sean Braithwaite, Ethan Buchman, Ismail Khoffi +4
In Tendermint blockchains, the proof-of-stake mechanism and the underlying consensus algorithm entail a dynamic fault model that implies that the active validators (nodes that sign…
Exact Penalties for Decomposable Optimization Problems
Igor V. Konnov
We consider a general decomposable convex optimization problem. By using right-hand side allocation technique, it can be transformed into a collection of small dimensional optimiza…
Decentralized Multi-Agent Optimization Based on a Penalty Method
Igor Konnov
We propose a decentralized penalty method for general convex constrained multi-agent optimization problems. Each auxiliary penalized problem is solved approximately with a special…
Variational Inequality Type Formulations of General Market Equilibrium Problems with Local Information
Igor Konnov
We suggest a new approach to creation of general market equilibrium models involving economic agents with local and partial knowledge about the system and under different restricti…
A little about models
I. V. Konnov
We discuss several aspects of creation of adequate mathematical models in other sciences. In particular, many difficulties stem from great complexity of the source systems and the…
A General Class of Relative Optimization Problems
I. V. Konnov
We consider relative or subjective optimization problems where the goal function and feasible set are dependent of the current state of the system under consideration. In general,…
A Non-Monotone Conjugate Subgradient Type Method for Minimization of Convex Functions
Igor Konnov
We suggest a conjugate subgradient type method without any line-search for minimization of convex non differentiable functions. Unlike the custom methods of this class, it does not…
A Simple Adaptive Step-size Choice for Iterative Optimization Methods
Igor Konnov
We suggest a simple adaptive step-size procedure, which does not require any line-search, for a general class of nonlinear optimization methods and prove convergence of a general m…
Application of Market Models to Network Equilibrium Problems
Igor Konnov
We present a general two-side market model with divisible commodities and price functions of participants. A general existence result on unbounded sets is obtained from its variati…
The Method of Pairwise Variations with Tolerances for Linearly Constrained Optimization Problems
I. V. Konnov
We consider a method of pairwise variations for smooth optimization problems, which involve polyhedral constraints. It consists in making steps with respect to the difference of tw…
A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms
Igor Konnov, Marijana Lazic, Helmut Veith +1
Distributed algorithms have many mission-critical applications ranging from embedded systems and replicated databases to cloud computing. Due to asynchronous communication, process…
An Adaptive Partial Linearization Method for Optimization Problems on Product Sets
I. V. Konnov
We suggest an adaptive version of a partial linearization method for composite optimization problems. The goal function is the sum of a smooth function and a non necessary smooth c…
Selective Bi-coordinate Method for Non-Stationary and Non-Smooth Resource Allocation Type Problems
I. V. Konnov
We propose a method of bi-coordinate variations for non-stationary and non-smooth optimization problems, which involve a single linear equality and box constraints. Here only appro…
Starting a Dialog between Model Checking and Fault-tolerant Distributed Algorithms
Annu John, Igor Konnov, Ulrich Schmid +2
Fault-tolerant distributed algorithms are central for building reliable spatially distributed systems. Unfortunately, the lack of a canonical precise framework for fault-tolerant a…
Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms
Annu John, Igor Konnov, Ulrich Schmid +2
We introduce an automated parameterized verification method for fault-tolerant distributed algorithms (FTDA). FTDAs are parameterized by both the number of processes and the assume…