Javier Esparza, Alexander Miller, Petr Jančar
Abstract. Signal Transition Graphs (STGs) are a popular formalism for the specification of asynchronous circuits. A necessary condition for the implementability of an STG is the existence of a...
Cheng, Chih-Hong, Buckl, Christian, Esparza, Javier, Knoll, Alois
The focus of the tool FTOS is to alleviate designers' burden by offering code generation for non-functional aspects including fault-tolerance mechanisms. One crucial aspect in this context is to...
Modeling and Verification for Timing Satisfaction of Fault-Tolerant Systems with Finiteness (2009)
Cheng, Chih-Hong, Buckl, Christian, Esparza, Javier, Knoll, Alois
The increasing use of model-based tools enables further use of formal verification techniques in the context of distributed real-time systems. To avoid state explosion, it is necessary to construct...
Abteilung Sichere, Zuverlässige Softwaresysteme, Stefan Kiefer, Examiner Prof, Dr. Javier Esparza, Supervision Dr. Stefan Schwoon
I hereby declare that this thesis was composed by myself, and that I have used no sources other than those cited in the thesis. (Stefan Kiefer) 4
On Fixed Point Equations over Commutative (2008)
Javier Esparza, Stefan Kiefer, Michael Luttenberger
Abstract. Fixed point equations x = f(x) over ω-continuous semirings can be seen as the mathematical foundation of interprocedural program analysis. The sequence 0, f(0), f 2 (0),... converges to...
Building a Software Model-Checker (2008)
Model-checking techniques are being increasingly applied to software. In this course I will start by introducing jMoped, a tool for the analysis of Java programs. I will then proceed to explain the...
Convergence Thresholds of Newton's Method for Monotone Polynomial Equations (2008)
Esparza, Javier, Kiefer, Stefan, Luttenberger, Michael
Monotone systems of polynomial equations (MSPEs) are systems of fixed-point equations $X_1 = f_1(X_1, \ldots, X_n),$ $\ldots, X_n = f_n(X_1, \ldots, X_n)$ where each $f_i$ is a polynomial with...
Convergence Thresholds of Newton's Method for Monotone Polynomial Equations (2008)
Esparza, Javier, Kiefer, Stefan, Luttenberger, Michael
Monotone systems of polynomial equations (MSPEs) are systems of fixed-point equations $X_1 = f_1(X_1, \ldots, X_n),$ $\ldots, X_n = f_n(X_1, \ldots, X_n)$ where each $f_i$ is a polynomial with...
Convergence Thresholds of Newton's Method for Monotone Polynomial Equations (2008)
Esparza, Javier, Kiefer, Stefan, Luttenberger, Michael
Monotone systems of polynomial equations (MSPEs) are systems of fixed-point equations $X_1 = f_1(X_1, ..., X_n),$ $..., X_n = f_n(X_1, ..., X_n)$ where each $f_i$ is a polynomial with positive real...
An Extension of Newton's Method to (2008)
Continuous Semirings, Javier Esparza, Stefan Kiefer, Michael Luttenberger
Abstract. Fixed point equations x = F (x) over!-continuous semirings are a natural mathematical foundation of interprocedural program analysis. Equations over the semiring of the real numbers can be...
Javier Esparza, Antonín Kučera, Richard Mayr
Probabilistic pushdown automata (pPDA) have been identified as a natural model for probabilistic programs with recursive procedure calls. Previous works considered the decidability and complexity of...
Abstract. Signal Transition Graphs (STGs) are one of the most popular models for the specification of asynchronous circuits. A STG can be implemented if it admits a so-called consistent and complete...
An Extension of Newton's Method to (2008)
Continuous Semirings, Javier Esparza, Stefan Kiefer, Michael Luttenberger
Abstract. Fixed point equations x = F (x) over!-continuous semirings are a natural mathematical foundation of interprocedural program analysis. Equations over the semiring of the real numbers can be...
On Fixed Point Equations over Commutative (2008)
Javier Esparza, Stefan Kiefer, Michael Luttenberger
Abstract. Fixed point equations x = f(x) over ω-continuous semirings can be seen as the mathematical foundation of interprocedural program analysis. The sequence 0,f(0),f 2 (0),... converges to the...
Ahmed Bouajjani, Javier Esparza, Tayssir Touili
We present a generic aproach to the static analysis of concurrent programs with procedures. We model programs as communicating pushdown systems. It is known that typical dataflow problems for this...
1 Preface Grammars as Processes (2008)
ETAPS conference and he was taking part in a meeting. The next day I was giving a talk with the title “Grammars as Processes”, and Grzegorz, who had seen it announced in the program, asked me...
Software Tools for Technology Transfer manuscript No. (will be inserted by the editor) (2008)
A Negative, Result Depth-first, Net Unfoldings, Javier Esparza, Pradeep Kanade, Stefan Schwoon
The date of receipt and acceptance will be inserted by the editor
Laboratory for Foundations of Computer Science, (2008)
The Model-checking, Kit Claus Schr"oter, Stefan Schwoon, Javier Esparza
Abstract. The Model-Checking Kit [8] is a collection of programs which allow to model finite state systems using a variety of modelling languages, and verify them using a variety of checkers,...
IOS Press Unfolding Based Algorithms for the Reachability Problem ∗ (2008)
Javier Esparza, Claus Schröter
Abstract. We study four solutions to the reachability problem for 1-safe Petri nets, all of them based on the unfolding technique. We define the problem as follows: given a set of places of the net,...
Convergence Thresholds of Newton's Method for Monotone Polynomial Equations (2008)
Esparza, Javier, Kiefer, Stefan, Luttenberger, Michael
Monotone systems of polynomial equations (MSPEs) are systems of fixed-point equations $X_1 = f_1(X_1, \ldots, X_n),$ $\ldots, X_n = f_n(X_1, \ldots, X_n)$ where each $f_i$ is a polynomial with...
Convergence Thresholds of Newton's Method for Monotone Polynomial Equations (2008)
Esparza, Javier, Kiefer, Stefan, Luttenberger, Michael
Monotone systems of polynomial equations (MSPEs) are systems of fixed-point equations $X_1 = f_1(X_1, \ldots, X_n),$ $\ldots, X_n = f_n(X_1, \ldots, X_n)$ where each $f_i$ is a polynomial with...
26. Convergence Thresholds of Newton's Method for Monotone Polynomial Equations (2008)
Esparza, Javier, Kiefer, Stefan, Luttenberger, Michael
Monotone systems of polynomial equations (MSPEs) are systems of fixed-point equations $X_1 = f_1(X_1, ldots, X_n),$ $ldots, X_n = f_n(X_1, ldots, X_n)$ where each $f_i$ is a polynomial with positive...
Efficient Algorithms for pre* and post* on Interprocedural Parallel Flow Graphs (2007)
Javier Esparza, Andreas Podelski
This paper is a contribution to the already existing series of work on the algorithmic principles of interprocedural analysis. We consider the generalization to the case of parallel programs. We give...
Antonin Kucera, Antonin Kucera, Javier Esparza, Javier Esparza, Javier Esparza, Stefan Schwoon, ...
Recent works have proposed pushdown systems as a tool for analyzing programs with (recursive) procedures. In particular, the model-checking problem for LTL has been studied. In this paper we examine...
Gordon Plotkin, Glynn Winskel Bistructures, Javier Esparza, Decidability Issues, Petri Nets, Andr Joyal, ...
Javier Esparza, Petr Jan Car, Faron Moller
We consider the following problems: (a) Given a labelled Petri net and a finite automaton, are they equivalent? (b) Given a labelled Petri net, is it equivalent to some (unspecified) finite...
Ahmed Bouajjani, Javier Esparza, Alain Finkel, Oded Maler, Peter Rossmanith, Bernard Willems
2 Institut fur Informatik, Technische Universitat Munchen, Arcisstr. 21,
Javier Esparza, Keijo Heljanko
Abstract We report on an implementation of the unfolding approach to model-checking LTL-X recently presented by the authors. Contrary to that work, we consider an state-based version of LTL-X, which...
IOS Press Petri Nets, Commutative Context-Free Grammars, and Basic Parallel Processes (2007)
Abstract. The paper provides a structural characterisation of the reachable markings of Petri nets in which every transition has exactly one input place. As a corollary, the reachability problem for...
Petri Nets and Regular Processes (2007)
Petr Jan Car, Javier Esparza, Faron Moller
SWEDEN Copyright c fl the authors We consider the following problems: (a) Given a labelled Petri net and a finite automaton, are they equivalent? (b) Given a labelled Petri net, is it equivalent to...
A NEW UNFOLDING APPROACH TO LTL MODEL CHECKING (2007)
Espoo Hut-tcs-a, Tekniska Hgskolan, Javier Esparza, Javier Esparza, Keijo Heljanko, ...
Teknillinen korkeakoulu Tietotekniikan osasto Tietojenka sittelyteorian laboratorio Distribution:
Javier Esparza, Antonn Kucera, Richard Mayr
We consider the model checking problem for probabilistic pushdown automata (pPDA) and properties expressible in various probabilistic logics. We start with properties that can be formulated as...
IOS Press Unfolding Based Algorithms for the Reachability Problem # (2007)
Javier Esparza, Claus Schr Oter
Abstract. We study four solutions to the reachability problem for 1-safe Petri nets, all of them based on the unfolding technique. We define the problem as follows: given a set of places of the net,...
Eike Best, Javier Esparza, Bernd Grahlmann, Stephan Melzer, Stefan Romer, Frank Wallner
3 This paper gives a short overview of the verification system PEP (a Programming Environment based on Petri nets). It focuses on some recent developments.
Javier Esparza, Kousha Etessami
Abstract. Monolithic nite-state probabilistic programs have been abstractly modeled by nite Markov chains, and the algorithmic veri-cation problems for them have been investigated very extensively....
Javier Esparza, Antonn Kucera, Stefan Schwoon
Recent works have proposed pushdown systems as a tool for analyzing programs with (recursive) procedures, and the model-checking problem for LTL has received special attention. However, all these...
on Interprocedural Parallel Flow Graphs (2007)
Javier Esparza, Andreas Podelski
This paper is a contribution to the already existing series of work on the algorithmic principles of interprocedural analysis. We consider the generalization to the case of parallel programs. We give...
Ahmed Bouajjani, Javier Esparza, Oded Maler
We apply the symbolic analysis principle to pushdown systems. We represent (possibly infinite) sets of configurations of such systems by means of finite-state automata. In order to reason in a...
Giorgio Delzanno, Javier Esparza, Andreas Podelski
Abstract. Broadcast protocols are systems composed of a nite but arbitrarily large number of processes that communicate by rendezvous (two processes exchange a message) or by broadcast (a process...
Stephan Melzer, Stefan Romer, Javier Esparza
Abstract. PEP is a tool for the design, analysis and the verification of parallel programs. Two approaches are presented in this paper being the underlying technique of the verification component of...
The Asynchronous Committee Meeting Problem (2007)
Javier Esparza, Bernhard Von Stengel
Abstract. The committee meeting problem consists in finding the earliest meeting time acceptable to every member of a committee. We consider an asynchronous version of the problem that does not...
More Infinite Results Olaf Burkart (2007)
Recently there has been a spurt of activity in concurrency theory centred on the analysis of infinite-state systems. The following two problems have been intensely investigated: (1) given two...
Abstract. We study the following problem: Given a transition system T and its quotient T = under an equivalence, which are the sets L, L 0
Abstract. We show that recent progress in extending the automatatheoretic approach to model-checking beyond the class of finite-state processes finds a natural application in the area of...
Ahmed Bouajjani, Javier Esparza, Tayssir Touili
Communicated by Editor's name We present a generic aproach to the static analysis of concurrent programs with procedures. We model programs as communicating pushdown systems. It is known that...
On the Mechanized Verication of Innite Systems (2007)
Observation equivalence is a well-known technique for proving that a concurrent system satises its specication. We report on our experience in the mechanization of observation equivalence proofs with...
(formerly: Elektron. Inform.verarb. Kybernet.) Decidability Issues for Petri Nets-- a survey (2007)
Javier Esparza, Mogens Nielsen
Abstract: We survey 25 years of research on decidability issues for Petri nets. We collect results on the decidability of important properties, equivalence notions, and temporal logics. 1.
On the convergence of Newton’s method for monotone systems of polynomial equations (2007)
Stefan Kiefer, Michael Luttenberger, Javier Esparza
kiefersn, luttenml, esparza o
An extension of Newton’s method to ω-continuous semirings (2007)
Javier Esparza, Stefan Kiefer, Michael Luttenberger
Abstract. Fixed point equations x = F (x) over ω-continuous semirings are a natural mathematical foundation of interprocedural program analysis. Equations over the semiring of the real numbers can...
An extension of Newton’s method to ω-continuous semirings (2007)
Javier Esparza, Stefan Kiefer, Michael Luttenberger
Abstract. Fixed point equations x = F (x) over ω-continuous semirings are a natural mathematical foundation of interprocedural program analysis. Equations over the semiring of the real numbers can...
Convergence thresholds of Newton’s method for monotone polynomial equations (2007)
Javier Esparza, Stefan Kiefer, Michael Luttenberger
Abstract. Monotone systems of polynomial equations (MSPEs) are systems of fixedpoint equations X1 = f1(X1,..., Xn),..., Xn = fn(X1,..., Xn) where each fi is a polynomial with positive real...
Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems (2006)
Esparza, Javier, Kiefer, Stefan, Schwoon, Stefan
Counterexample-guided abstraction refinement (CEGAR) has proven to be apowerful method for software model-checking. In this paper, we investigate thisconcept in the context of sequential (possibly...
Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems (2006)
Esparza, Javier, Kiefer, Stefan, Schwoon, Stefan
21 pages
Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems (2006)
Esparza, Javier, Kiefer, Stefan, Schwoon, Stefan
Counterexample-guided abstraction refinement (CEGAR) has proven to be a powerful method for software model-checking. In this paper, we investigate this concept in the context of sequential (possibly...
Suwimonteerabuth, Dejvuth, Schwoon, Stefan, Esparza, Javier
Motivated by recent applications of pushdown systems to computer security problems, we present an efficient algorithm for the reachability problem of alternating pushdown systems. Although the...
Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols (2006)
Giorgio Delzanno, Javier Esparza
Abstract. Ping-pong protocols with recursive definitions of agents, but without any active intruder, are a Turing powerful model. We show that under the environment sensitive semantics (i.e. by...
Rewriting models of Boolean programs (2006)
Ahmed Bouajjani, Javier Esparza
Abstract. We show that rewrite systems can be used to give semantics to imperative programs with boolean variables, a class of programs used in software model-checking as over- or underapproximations...
Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols (2006)
Giorgio Delzanno, Javier Esparza
Abstract. Ping-pong protocols with recursive definitions of agents, but without any active intruder, are a Turing powerful model. We show that under the environment sensitive semantics (i.e. by...
Javier Esparza, Alexander Miller, Petr Jančar
Signal Transition Graphs (STGs) are a popular formalism for the specification of asynchronous circuits. A necessary condition for the implementability of an STG is the existence of a consistent and...
Automatic Synthesis of Dis trib (2006)
Elektrotechnik Und Informationstechnik, Aus Slatina Rumänien, Vorsitzender Prüfungsausschusses, Prof Dr, Volker Diekert, ...
ut Alin S¸tefănescu
Rewriting models of Boolean programs (2006)
Ahmed Bouajjani, Javier Esparza
Abstract. We show that rewrite systems can be used to give semantics to imperative programs with boolean variables, a class of programs used in software model-checking as over- or underapproximations...
Abstraction refinement with Craig interpolation and symbolic pushdown systems (2006)
Javier Esparza, Stefan Kiefer, Stefan Schwoon
Abstract. Counterexample-guided abstraction refinement (CEGAR) has proven to be a powerful method for software model-checking. In this paper, we investigate this concept in the context of sequential...
On the Complexity of Consistency and Complete State Coding for Signal Transition Graphs (2006)
Signal Transition Graphs (STGs) are a popular formalism for the specification of asynchronous circuits. A necessary condition for the implementability of an STG is the existence of a consistent and...
Abstraction refinement with Craig interpolation and symbolic pushdown systems (2006)
Javier Esparza, Stefan Kiefer, Stefan Schwoon
Abstract. Counterexample-guided abstraction refinement (CEGAR) has proven to be a powerful method for software model-checking. In this paper, we investigate this concept in the context of sequential...
Dejvuth Suwimonteerabuth, Stefan Schwoon, Javier Esparza
Abstract. Motivated by recent applications of pushdown systems to computer security problems, we present an efficient algorithm for the reachability problem of alternating pushdown systems. Although...
Reachability analysis of multithreaded software with asynchronous communication (2006)
Bouajjani, Ahmed, Esparza, Javier, Schwoon, Stefan, Strejcek, Jan
We introduce asynchronous dynamic pushdown networks (ADPN), a new model for multithreaded programs in which pushdown systems communicate via shared memory. ADPN generalizes both CPS (concurrent...
On the complexity of consistency and complete state coding for signal transition graphs (2006)
Javier Esparza, Alexander Miller, Petr Jančar
Signal Transition Graphs (STGs) are a popular formalism for the specification of asynchronous circuits. A necessary condition for the implementability of an STG is the existence of a consistent and...
Reachability analysis of multithreaded software with asynchronous communication (2005)
Bouajjani, Ahmed, Esparza, Javier, Schwoon, Stefan, Strejcek, Jan
18 pages
Model Checking Probabilistic Pushdown Automata (2005)
Esparza, Javier, Kucera, Antonin, Mayr, Richard
We consider the model checking problem for probabilistic pushdown automata (pPDA) and properties expressible in various probabilistic logics. We start with properties that can be formulated as...
Reachability analysis of multithreaded software with asynchronous communication (2005)
Bouajjani, Ahmed, Esparza, Javier, Schwoon, Stefan, Strejcek, Jan
We introduce asynchronous dynamic pushdown networks (ADPN), a new model formultithreaded programs in which pushdown systems communicate via shared memory.ADPN generalizes both CPS (concurrent...
Reachability analysis of multithreaded software with asynchronous communication (2005)
Bouajjani, Ahmed, Esparza, Javier, Schwoon, Stefan, Strejcek, Jan
We introduce asynchronous dynamic pushdown networks (ADPN), a new model for multithreaded programs in which pushdown systems communicate via shared memory. ADPN generalizes both CPS (concurrent...
Event Multiset Lemmas Channel Contents (2005)
Tom Ridge, Javier Esparza, Ltl Simulationrelation
Why are theorem provers not more widely used?
Verifying red-black trees (2005)
Paolo Baldan, Andrea Corradini, Javier Esparza, Tobias Heindel, Barbara König, Vitali Kozioura
Abstract. We show how to verify the correctness of insertion of elements into red-black trees—a form of balanced search trees—using analysis techniques developed for graph rewriting. We first...
S.: Locality-based abstractions (2005)
Javier Esparza, Pierre Ganty, Stefan Schwoon
Abstract. We present locality-based abstractions, in which a set of states of a distributed system is abstracted to the collection of views that some observers have of the states. Special cases of...
A note on on-the-fly verification algorithms (2005)
Stefan Schwoon, Javier Esparza
Abstract. The automata-theoretic approach to verification of LTL relies on an algorithm for finding accepting cycles in the product of the system and a Büchi automaton for the negation of the...
jMoped: A Java bytecode checker based on Moped (2005)
Dejvuth Suwimonteerabuth, Stefan Schwoon, Javier Esparza
Abstract. We present a tool for finding errors in Java programs that translates Java bytecodes into symbolic pushdown systems, which are then checked by the Moped tool [1]. 1
Reachability analysis of multithreaded software with asynchronous communication (2005)
Ahmed Bouajjani, Javier Esparza, Stefan Schwoon
Abstract. We introduce asynchronous dynamic pushdown networks (ADPN), a new model for multithreaded programs in which pushdown systems communicate via shared memory. ADPN generalizes both CPS...
S.: Locality-based abstractions (2005)
Javier Esparza, Pierre Ganty, Stefan Schwoon
Abstract. We present locality-based abstractions, in which a set of states of a distributed system is abstracted to the collection of views that some observers have of the states. Special cases of...
Reachability analysis of multithreaded software with asynchronous communication (2005)
Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, Jan Strejček� Liafa
Abstract. We introduce asynchronous dynamic pushdown networks (ADPN), a new model for multithreaded programs in which pushdown systems communicate via shared memory. ADPN generalizes both CPS...
Reachability analysis of multithreaded software with asynchronous communication (2005)
Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, Jan Strejček
communication
A note on on-the-fly verification algorithms (2004)
Schwoon, Stefan, Esparza, Javier
The automata-theoretic approach to verification of LTL relies on an algorithmfor finding accepting cycles in the product of the system and a Büchi automatonfor the negation of the formula....
A note on on-the-fly verification algorithms (2004)
Schwoon, Stefan, Esparza, Javier
The automata-theoretic approach to verification of LTL relies on an algorithm for finding accepting cycles in the product of the system and a Büchi automaton for the negation of the formula....
Model checking probabilistic pushdown automata (2004)
We consider the model checking problem for probabilistic pushdown automata (pPDA) and properties expressible in various probabilistic logics. We start with properties that can be formulated as...
Model Checking Probabilistic Pushdown Automata (2004)
Fi Mu, Antonín Kucera, Javier Esparza, Javier Esparza, Richard Mayr, ...
We consider the model checking problem for probabilistic pushdown automata (pPDA) and properties expressible in various probabilistic logics. We start with properties that can be formulated as...
Implementation of a Consistency Test for Free-Choice Signal Transition Graphs (2004)
S. Mahadevan, Saravanan Mahadevan, Infotech Programme, Supervisor Prof, Dr. Javier Esparza
I would like to thank my supervisor Prof. Javier Esparza for his support and constant advices. The comments and encouragements given by him were invaluable to the completion of this thesis. I also...
A Polynomial-Time Algorithm for Checking Consistency of Free-Choice Signal Transition Graphs (2004)
Signal Transition Graphs (STGs) are one of the most popular models for the specication of asynchronous circuits. A STG can be implemented if it admits a so-called consistent and complete binary...
Reachability analysis of synchronized PA systems (2004)
Ahmed Bouajjani, Javier Esparza, Tayssir Touili
Abstract. We present a generic approach for the analysis of concurrent programs with (unbounded) dynamic creation of threads and recursive procedure calls. We define a model for such programs based...
Verifying probabilistic procedural programs (2004)
Javier Esparza, Kousha Etessami
Abstract. Monolithic finite-state probabilistic programs have been abstractly modeled by finite Markov chains, and the algorithmic verification problems for them have been investigated very...
Model checking probabilistic pushdown automata (2004)
Javier Esparza, Antonín Kučera, Richard Mayr
Abstract. We consider the model checking problem for probabilistic pushdown automata (pPDA) and properties expressible in various probabilistic logics. We start with properties that can be formulated...
Model checking probabilistic pushdown automata (2004)
Javier Esparza, Antonín Kučera, Richard Mayr
Abstract. We consider the model checking problem for probabilistic pushdown automata (pPDA) and properties expressible in various probabilistic logics. We start with properties that can be formulated...
Model checking probabilistic pushdown automata (2004)
We consider the model checking problem for probabilistic pushdown automata (pPDA) and properties expressible in various probabilistic logics. We start with properties that can be formulated as...
Claus Schröter, Stefan Schwoon, Javier Esparza
Abstract. The Model-Checking Kit [8] is a collection of programs which allow to model finite state systems using a variety of modelling languages, and verify them using a variety of checkers,...
Reachability analysis of synchronized PA systems (2004)
Ahmed Bouajjani, Javier Esparza, Tayssir Touili
We present a generic approach for the analysis of concurrent programs with (unbounded) dynamic creation of threads and recursive procedure calls. We define a model for such programs based on a set of...
Model Checking Probabilistic Pushdown Automata (2004)
Fi Mu, Javier Esparza, Antonín Kučera, Richard Mayr, Javier Esparza, Antonín Kučera, ...
We consider the model checking problem for probabilistic pushdown automata (pPDA) and properties expressible in various probabilistic logics. We start with properties that can be formulated as...
Simple representative instantiations for multicast protocols (2003)
Abstract. We present a formal model for multicast network protocols working on arbitrary tree structures. We give sucient conditions under which correctness of the protocol for all structures reduces...
A generic approach to the static analysis of concurrent programs with procedures (2003)
Ahmed Bouajjani, Javier Esparza, Tayssir Touili
We present a generic aproach to the static analysis of concurrent programs with procedures. We model programs as communicating pushdown systems. It is known that typical dataflow problems for this...
A polynomial-time algorithm for checking consistency of free-choice signal transition graphs (2003)
Signal Transition Graphs (STGs) are one of the most popular models for the specification of asynchronous circuits. A STG can be implemented if it admits a so-called consistent and complete binary...
Synthesis of Distributed Algorithms Using Asynchronous Automata (2003)
Alin Stefanescu, Javier Esparza, Anca Muscholl
We apply the theory of asynchronous automata to the synthesis problem of closed distributed systems. We use safe asynchronous automata as implementation model, and characterise the languages they...
Synthesis of Distributed Algorithms Using Asynchronous Automata (2003)
Alin Stefanescu, Javier Esparza, Anca Muscholl
We apply the theory of asynchronous automata to the synthesis problem of closed distributed systems. We use safe asynchronous automata as implementation model, and characterise the languages they...
A Generic Approach to the Static Analysis of Concurrent Programs with Procedures (2003)
Ahmed Bouajjani, Javier Esparza, Tayssir Touili
We present a generic aproach to the static analysis of concurrent programs with procedures. We model programs as communicating pushdown systems. It is known that typical dataflow problems for this...
Synthesis of distributed algorithms using asynchronous automata (2003)
Abstract. We apply the theory of asynchronous automata to the synthesis problem of closed distributed systems. We use safe asynchronous automata as implementation model, and characterise the...
A Logical Viewpoint on Process-algebraic Quotients (2003)
Kucera, Antonín, Esparza, Javier
Let ∼ be a process equivalence. A formula ϕ is preserved by ∼-quotients iff for every process s of a transition system T we have that if s satisfies ϕ, then also [s] satisfies ϕ,...
In 1999 I met Grzegorz Rozenberg in Amsterdam, while I was attending the ETAPS conference and he was taking part in a meeting. The next day I was giving a talk with the title "Grammars as...
Javier Esparza, Antonín Kučera, Stefan Schwoon
Recent works have proposed pushdown systems as a tool for analyzing programs with (recursive) procedures, and the model-checking problem for LTL has received special attention. However, all these...
Model-Checking LTL with Regular Valuations for Pushdown Systems (2001)
Stefan Schwoon, Stefan Schwoon, Antonin Kucera, Antonin Kucera, Javier Esparza, Javier Esparza, ...
by
Model-checking LTL with regular valuations for pushdown systems (2001)
Javier Esparza, Antonn Kucera, Stefan Schwoon
Abstract. Recent works have proposed pushdown systems as a tool for analyzing programs with (recursive) procedures. In particular, the model-checking problem for LTL has been studied. In this paper...
Net Reductions for LTL Model-Checking (2001)
Javier Esparza, Claus Schroter
Abstract. We present a set of reduction rules for LTL model-checking of 1-safe Petri nets. Our reduction techniques are of two kinds: (1) Linear programming techniques which are based on well-known...
A BDD-based model checker for recursive programs (2001)
Javier Esparza, Stefan Schwoon
Abstract. We present a model-checker for boolean programs with (possibly recursive) procedures and the temporal logic LTL. The checker is guaranteed to terminate even for (usually faulty) programs in...
K.: Implementing LTL model checking with net unfoldings (2001)
Ab Teknillinen Korkeakoulu, Tekniska Hgskolan, Javier Esparza, Javier Esparza, Javier Esparza, ...
Teknillinen korkeakoulu Tietotekniikan osasto Tietojenka sittelyteorian laboratorio Distribution:
K.: Implementing LTL model checking with net unfoldings (2001)
Ab Teknillinen Korkeakoulu, Tekniska Hgskolan, Javier Esparza, Javier Esparza, Javier Esparza, ...
Teknillinen korkeakoulu Tietotekniikan osasto Tietojenka sittelyteorian laboratorio Distribution:
Implementing LTL model checking with net unfoldings (2001)
Javier Esparza, Keijo Heljanko
Abstract We report on an implementation of the unfolding approach to model-checking LTL-X recently presented by the authors. Contrary to that work, we consider an state-based version of LTL-X, which...
Implementing LTL Model Checking with Net Unfoldings (2001)
Ab Teknillinen Korkeakoulu, Tekniska Hgskolan, Javier Esparza, Javier Esparza, Javier Esparza, ...
We report on an implementation of the unfolding approach to model-checking LTL-X recently presented by the authors. Contrary to that work, we consider an state-based version of LTL-X, which is more...
Implementing LTL model checking with net unfoldings (2001)
Abteknillinen Korkeakoulu, Javier Esparza, Javier Esparza, Tietotekniikan Osasto, C Javier Esparza, ...
Teknillisen korkeakoulun tietojenkäsittelyteorian laboratorion tutkimusraportti 68
Model-checking LTL with regular valuations for pushdown systems (2001)
Javier Esparza, Antonín Kučera, Stefan Schwoon
Abstract. Recent works have proposed pushdown systems as a tool for analyzing programs with (recursive) procedures. In particular, the model-checking problem for LTL has been studied. In this paper...
Net Reductions for LTL Model-Checking (2001)
Javier Esparza, Claus Schröter
Abstract. We present a set of reduction rules for LTL model-checking of 1-safe Petri nets. Our reduction techniques are of two kinds: (1) Linear programming techniques which are based on well-known...
Implementing LTL model checking with net unfoldings (2001)
Abteknillinen Korkeakoulu, Javier Esparza, Javier Esparza, Tietotekniikan Osasto, C Javier Esparza, ...
Teknillisen korkeakoulun tietojenkäsittelyteorian laboratorion tutkimusraportti 68
Verifying single and multimutator garbage collectors with Owicki/Gries in Isabelle/HOL (2000)
Leonor Prensa Nieto, Javier Esparza
Abstract. Using a formalization of the Owicki-Gries method in the theorem prover Isabelle/HOL, we obtain mechanized correctness proofs for two incremental garbage collection algorithms, the second...
Reachability Analysis Using Net Unfoldings (2000)
Abstract. We study four solutions to the reachability problem for 1safe Petri nets, all of them based on the unfolding technique. We dene the problem as follows: given a set of places of the net,...
A new Unfolding Approach to LTL Model Checking (2000)
Javier Esparza, Keijo Heljanko
Abstract A new unfolding approach to LTL model checking is presented, in which the model checking problem can be solved by direct inspection of a certain finite prefix. The techniques presented so...
A uniform framework for problems on context-free grammars (2000)
Javier Esparza, Peter Rossmanith, Stefan Schwoon
In [2], Bouajjani and others presented an automata-based approach to a number of elementary problems on context-free grammars. This approach is of pedagogical interest since it provides a uniform...
Efficient algorithms for model checking pushdown systems (2000)
Javier Esparza, David Hansel, Peter Rossmanith, Stefan Schwoon
We study model checking problems for pushdown systems and linear time logics. We show that the global model checking problem (computing the set of configurations, reachable or not, that violate the...
Verification of Infinite-state Systems (2000)
Ahmed Bouajjani, Javier Esparza
ion by Syntactic Program Transformations 9 8 Unfoldings of Innite State Systems 9 9 Provability in a Logic for Concurrent Objects is Well-structured! 10 10 On the Complexity of Bisimulation...
A New Unfolding Approach to LTL Model Checking (2000)
Javier Esparza, Keijo Heljanko
A new unfolding approach to LTL model checking is presented, in which the model checking problem can be solved by direct inspection of a certain finite prefix. The techniques presented so far...
An Efficient Automata Approach to Some Problems on Context-Free Grammars (2000)
Ahmed Bouajjani, Javier Esparza, Alain Finkel, Oded Maler, Peter Rossmanith, Bernard Willems, ...
In Chapter 4 of [2], Book and Otto solve a number of word problems for monadic string-rewriting systems using an elegant automata-based technique. In this note we observe that the technique is also...
A Logical Viewpoint on Process-Algebraic Quotients (2000)
Fi Mu, Javier Esparza, Antonín Kucera, Antonín Kučera, Javier Esparza Y
We study the following problem: Given a transition system T and its quotient T= # under an equivalence #, which are the sets L, L 0 of Hennessy-Milner formulae such that: if ' 2Land T satisfies...
A New Unfolding Approach to LTL Model Checking (2000)
Espoo Hut-tcs-a, Tekniska Hgskolan, Javier Esparza, Javier Esparza, Keijo Heljanko, ...
: A new unfolding approach to LTL model checking is presented, in which the model checking problem can be solved by direct inspection of a certain finite prefix. The techniques presented so far...
Efficient algorithms for model checking pushdown systems (2000)
Javier Esparza, David Hansel, Peter Rossmanith, Stefan Schwoon
1 Introduction Pushdown systems (PDSs) are pushdown automata seen under a different light: We are not interested in the languages they recognise, but in the transition system they generate. These are...
A new Unfolding Approach to LTL Model Checking (2000)
Javier Esparza, Javier Esparza, Keijo Heljanko, Keijo Heljanko, Teknillinen Korkeakoulu, ...
ABSTRACT: A new unfolding approach to LTL model checking is presented, in which the model checking problem can be solved by direct inspection of a certain finite prefix. The techniques presented so...
An Unfolding Algorithm for Synchronous Products of Transition Systems (1999)
Abstract. The unfolding method, initially introduced for systems modelled by Petri nets, is applied to synchronous products of transition systems, a model introduced by Arnold [2]. An unfolding...
On the Verification of Broadcast Protocols (1999)
Javier Esparza, Alain Finkel, Richard Mayr
We analyze the model-checking problems for safety and liveness properties in parameterized broadcast protocols, a model introduced in [5]. We show that the procedure suggested in [5] for safety...
On the Verification of Broadcast Protocols (1999)
Javier Esparza, Alain Finkel, Richard Mayr
We analyze the model-checking problems for safety and liveness properties in parameterized broadcast protocols, a model introduced in [5]. We show that the procedure suggested in [5] for safety...
A logical viewpoint on process-algebraic quotients (1999)
Let be a process equivalence. A formula ' is preserved by -quotients i for every process s of a transition system T we have that if s satises ', then also [s] satises ', where [s] is...
Petri nets and regular processes (1999)
Petr Jancar, Javier Esparza, Faron Moller
We consider the following problems: (a) Given a labelled Petri net and a finite automaton, are they equivalent? (b) Given a labelled Petri net, is it equivalent to some (unspecified) finite...
A Logical Viewpoint on Process-Algebraic Quotients (1999)
Antonín Kucera, Fi Mu, Javier Esparza, Javier Esparza
We study the following problem: Given a transition system T and its quotient T= under an equivalence , which are the sets L, L 0 of Hennessy-Milner formulae such that: if ' 2 L and T satisfies...
On the Verification of Broadcast Protocols (1999)
Javier Esparza, Alain Finkel, Richard Mayr
We analyze the model-checking problems for safety and liveness properties in parameterized broadcast protocols, a model introduced in [5]. We show that the procedure suggested in [5] for safety...
Proof-Checking Protocols using Bisimulations (1999)
Christine Röckl, Javier Esparza
We report on our experience in using the Isabelle/HOL theorem prover to mechanize proofs of observation equivalence for systems with in nitely many states, and for parameterized systems. We follow...
On the Verification of Broadcast Protocols (1999)
Javier Esparza, Alain Finkel, Richard Mayr
We analyze the model-checking problems for safety and liveness properties in parameterized broadcast protocols, a model introduced in [5]. We show that the procedure suggested in [5] for safety...
A logical viewpoint on process-algebraic quotients (1999)
Antonín Kučera, Javier Esparza
Abstract. We study the following problem: Given a transition system � and its quotient ���� � under an equivalence � , which are the sets � , �� � of Hennessy-Milner formulae...
An Unfolding Algorithm for Synchronous Products of Transition Systems (1999)
Abstract. The unfolding method, initially introduced for systems modelled by Petri nets, is applied to synchronous products of transition systems, a model introduced by Arnold [2]. An unfolding...
A logical viewpoint on process-algebraic quotients (1999)
Antonín Kučera, Javier Esparza
Abstract. We study the following problem: Given a transition systemTand its quotientT=under an equivalence, which are the setsL,L0of Hennessy-Milner formulae such that: if'2LandTsatisfies',...
Decidability and complexity of petri net problems - an introduction (1998)
Abstract. A collection of 10 "rules of thumb " is presented that helps to determine the decidability and complexity of a large number of Petri net problems. 1
Decidability and complexity of Petri net problems - an introduction (1998)
. A collection of 10 "rules of thumb" is presented that helps to determine the decidability and complexity of a large number of Petri net problems. 1 Introduction The topic of this paper is...
Decidability and complexity of petri net problems - an introduction (1998)
Abstract. A collection of 10 “rules of thumb ” is presented that helps to determine the decidability and complexity of a large number of Petri net problems. 1
Stephan Melzer, Frank Wallner, Javier Esparza
Partial order reduction versus Net unfoldings\Lambda
Decidability of model checking for infinite-state concurrent systems (1997)
We study the decidability of the model checking problem for linear and branching time logics, and two models of concurrent computation, namely Petri nets and Basic Parallel Processes. 1
Reachability Analysis of Pushdown Automata: Application to Model-Checking (1997)
Ahmed Bouajjani, Javier Esparza, Oded Maler
. We apply the symbolic analysis principle to pushdown systems. We represent (possibly infinite) sets of configurations of such systems by means of finite-state automata. In order to reason in a...
Model Checking LTL using Constraint Programming (1997)
Javier Esparza, Stephan Melzer
. The model-checking problem for 1-safe Petri nets and lineartime temporal logic (LTL) consists of deciding, given a 1-safe Petri net and a formula of LTL, whether the Petri net satisfies the...
Model Checking LTL using Constraint Programming (1997)
Javier Esparza, Stephan Melzer
The model-checking problem for 1-safe Petri nets and linear-time temporal logic (LTL) consists of deciding, given a 1-safe Petri net and a formula of LTL, whether the Petri net satisfies the property...
An Automata Approach to Some Problems on Context-Free Grammars (1997)
In Chapter 4 of [2], Book and Otto solve a number of word problems for monadic string-rewriting systems using an elegant automatabased technique. In this note we observe that the technique is also...
Reachability analysis of pushdown automata: application to model checking (1997)
Ahmed Bouajjani, Javier Esparza, Oded Maler
Abstract. We apply the symbolic analysis principle to pushdown systems. We represent (possibly in nite) sets of con gurations of such systems by means of nite-state automata. In order to reason in a...
Reachability in Live and Safe Free-Choice Petri Nets is NP-Complete (1996)
The complexity of the reachability problem for live and safe free-choice Petri nets has been open for several years. Several partial results seemed to indicate that the problem is polynomial. We show...
An Improvement of McMillan’s Unfolding Algorithm (1996)
Javier Esparza, Stefan Romer, Walter Vogler
ABSTRACT McMillan has recently proposed a new technique to avoid the state explosion problem in the verification of systems modelled with finite-state Petri nets. The technique requires to construct...
An Improvement of McMillan’s Unfolding Algorithm (1996)
Javier Esparza, Stefan Romer, Walter Vogler
Abstract. McMillan has recently proposed a new technique to avoid the state explosion problem in the verification of systems modelled with finite-state Petri nets. The technique requires to construct...
Andrei Kovalyov, Javier Esparza
Free-choice Signal Transition Graphs (STG) are a class of interpreted Petri nets with applications to the verification and synthesis of speed-independet circuits. Several synthesis techniques for...
Recently there has been a spurt of activity in concurrency theory centered on the analysis of infinite-state systems. The following two problems have been intensely investigated: (1) given two...
Deciding finiteness of Petri nets up to bisimulation (1996)
Petr Jancar Javier, Javier Esparza
. We study the following problems for strong and weak bisimulation equivalence: given a labelled Petri net and a finite transition system, are they equivalent?; given a labelled Petri net, is it...
Checking System Properties via Integer Programming (1996)
Stephan Melzer, Javier Esparza
. The marking equation is a well known verification method in the Petri net community. It has also be applied by Avrunin, Corbett et al. to automata models. It is a semidecision method, and it may...
Reachability in Live and Safe Free-Choice Petri Nets is NP-complete (1996)
The complexity of the reachability problem for live and safe free-choice Petri nets has been open for several years. Several partial results seemed to indicate that the problem is polynomial. We show...
Deciding finiteness of Petri nets up to bisimulation (1996)
. We study the following problems for strong and weak bisimulation equivalence: given a labelled Petri net and a finite transition system, are they equivalent?; given a labelled Petri net, is it...
Checking System Properties via Integer Programming (1996)
Anforderungen Prof, Dr. A. Bode, Stephan Melzer, Stephan Melzer, Javier Esparza, ...
Deciding finiteness of petri nets up to bisimulation (1996)
Abstract We study the following problems for strong and weak bisimulation equivalence: given a labelled Petri net and a finite transition system, are they equivalent?; given a labelled Petri net, is...
On the model checking problem for branching time logics and Basic Parallel Processes (1995)
Javier Esparza And, Javier Esparza, Astrid Kiehn
We investigate the model checking problem for branching time logics and Basic Parallel Processes. We show that the problem is undecidable for the logic 8L(O; F; U) (equivalent to CTL ) in the usual...
On the model checking problem for branching time logics and Basic Parallel Processes (1995)
We investigate the model checking problem for branching time logics and Basic Parallel Processes. We show that the problem is undecidable for the logic 8L(O; F; U) (equivalent to CTL ) in the usual...
Complexity results for 1-safe nets (1995)
Allan Cheng, Javier Esparza, Jens Palsberg
We study the complexity of several standard problems for 1-safe Petri nets and some of its subclasses. We prove that reachability, liveness, and deadlock are all PSPACE-complete for 1-safe nets. We...
Decidability issues for Petri nets (1994)
Javier Esparza, Javier Esparza, Mogens Nielsen, Mogens Nielsen
is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent publications in the BRICS Report Series. Copies...
On the decidability of model checking for several mu-calculi and Petri nets (1994)
The decidability of the model checking problem for several -calculi and Petri nets is analysed. The linear time -calculus is decidable; if simple atomic sentences are added, it becomes undecidable. A...
Decidability issues for Petri nets (1994)
Javier Esparza, Javier Esparza, Mogens Nielsen, Mogens Nielsen
Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent...
Complexity Results for 1-safe Nets (1993)
Allan Cheng, Javier Esparza, Jens Palsberg
We study the complexity of several standard problems for 1-safe Petri nets and some of its subclasses. We prove that reachability, liveness, and deadlock are all PSPACE-complete for 1-safe nets. We...
Complexity Results for 1-safe Nets (1993)
Allan Cheng, Javier Esparza, Jens Palsberg
We study the complexity of several standard problems for 1-safe Petri nets and some of its subclasses. We prove that reachability, liveness, and deadlock are all PSPACE-complete for 1-safe nets. We...
Solving Monotone Polynomial Equations (1970)
Javier Esparza, Stefan Kiefer, Michael Luttenberger
We survey some recent results on iterative methods for approximating the least solution of a system of monotone fixed-point polynomial equations. Full Text at Springer, may require registration or fee
Edwards, Claire M., Edwards, James R., Lwin, Seint T., Esparza, Javier, Oyajobi, Babatunde O., McCluskey, Brandon, ...
There is increasing evidence to suggest that the Wnt signaling pathway plays a critical role in the pathogenesis of myeloma bone disease. In the present study, we determined whether increasing Wnt...
Giorgio Delzanno, Javier Esparza, Copyright C, Giorgio Delzanno, Javier Esparza, Giorgio Delzanno, ...
Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent BRICS...