2 citations · 3 across the 3 of their papers we have counts for
4 papers
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…
Computing Parameterized Invariants of Parameterized Petri Nets
Javier Esparza, Mikhail Raskin, Christoph Welzel
A fundamental advantage of Petri net models is the possibility to automatically compute useful system invariants from the syntax of the net. Classical techniques used for this are…
Structural Invariants for the Verification of Systems with Parameterized Architectures
Marius Bozga, Javier Esparza, Radu Iosif +2
We consider parameterized concurrent systems consisting of a finite but unknown number of components, obtained by replicating a given set of finite state automata. Components commu…
Working with first-order proofs and provers
Michael Raskin, Christoph Welzel
Verifying software correctness has always been an important and complicated task. Recently, formal proofs of critical properties of algorithms and even implementations are becoming…