6 papers
Stateless Model Checking under a Reads-Value-From Equivalence
Pratyush Agarwal, Krishnendu Chatterjee, Shreya Pathak +2
Stateless model checking (SMC) is one of the standard approaches to the verification of concurrent programs. As scheduling non-determinism creates exponentially large spaces of thr…
The Reads-From Equivalence for the TSO and PSO Memory Models
Truc Lam Bui, Krishnendu Chatterjee, Tushar Gautam +2
The verification of concurrent programs remains an open challenge due to the non-determinism in inter-process communication. One algorithmic problem in this challenge is the consis…
Value-centric Dynamic Partial Order Reduction
Krishnendu Chatterjee, Andreas Pavlogiannis, Viktor Toman
The verification of concurrent programs remains an open challenge, as thread interaction has to be accounted for, which leads to state-space explosion. Stateless model checking bat…
Strategy Representation by Decision Trees with Linear Classifiers
Pranav Ashok, Tomáš Brázdil, Krishnendu Chatterjee +3
Graph games and Markov decision processes (MDPs) are standard models in reactive synthesis and verification of probabilistic systems with nondeterminism. The class of -regular w…
Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives
Krishnendu Chatterjee, Monika Henzinger, Veronika Loitzenbauer +2
Given a model and a specification, the fundamental model-checking problem asks for algorithmic verification of whether the model satisfies the specification. We consider graphs and…
Strategy Representation by Decision Trees in Reactive Synthesis
Tomáš Brázdil, Krishnendu Chatterjee, Jan Křetínský +1
Graph games played by two players over finite-state graphs are central in many problems in computer science. In particular, graph games with -regular winning conditions, specifi…