activity
20092021
most citedAn Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata

11 citations · 16 across the 8 of their papers we have counts for

collaborators

20 papers

cs.DC20211 cited

Abduction of trap invariants in parameterized systems

Javier Esparza, Mikhail Raskin, Christoph Welzel

In a previous paper we have presented a CEGAR approach for the verification of parameterized systems with an arbitrary number of processes organized in an array or a ring. The tech…

cs.DC2021

Population Protocols: Beyond Runtime Analysis

Javier Esparza

I survey our recent work on the verification of population protocols and their state complexity.

cs.FL2021

Decision Power of Weak Asynchronous Models of Distributed Computing

Philipp Czerner, Roland Guttenberg, Martin Helfrich +1

Esparza and Reiter have recently conducted a systematic comparative study of models of distributed computing consisting of a network of identical finite-state automata that coopera…

cs.DC2020

Peregrine 2.0: Explaining Correctness of Population Protocols through Stage Graphs

Javier Esparza, Martin Helfrich, Stefan Jaax +1

We present a new version of Peregrine, the tool for the analysis and parameterized verification of population protocols introduced in [Blondin et al., CAV'2018]. Population protoco…

cs.FL2020

A Classification of Weak Asynchronous Models of Distributed Computing

Javier Esparza, Fabian Reiter

We conduct a systematic study of asynchronous models of distributed computing consisting of identical finite-state devices that cooperate in a network to decide if the network sati…

cs.LO2020

Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling

Michael Blondin, Javier Esparza, Martin Helfrich +2

We present a sound and complete method for the verification of qualitative liveness properties of replicated systems under stochastic scheduling. These are systems consisting of a…