BCDE91
E. Best, L. Cherkasova, J. Desel, and J. Esparza.
Traps, free choice und home states (extended abstract).
In W. Thomas M. Kwiatowska, M. Shields, editor, Semantics for Concurrency, Leicester 1990, Workshops in Computing, pages 16-21. Springer-Verlag, 1991.

BDE92
E. Best, J. Desel, and J. Esparza.
Traps characterise home states in free choice systems.
Theoretical Computer Science, 101:161-176, 1992. [Abstract]

BDE93
E. Best, R. Devillers, and J. Esparza.
General refinement and recursion operators for the Petri box calculus.
In Patrice Enjalbert et al., editor, 10th Annual Symposium on Theoretical Aspects of Computer Science 1993 (10th STACS '93), number 665 in Lecture Notes in Computer Science, pages 130-140, 1993. [Abstract]

BE91
E. Best and J. Esparza.
Model checking of persistent Petri nets.
In G. Jäger E. Börger, H. Kleine Büning, and M. M. Richter, editors, Proceedings of Computer Science Logic, number 626 in Lecture Notes in Computer Science, pages 35-52, 1991. [Abstract]

BEGMRW97
E. Best, J. Esparza, B. Grahlmann, S. Melzer, S. Römer, and F. Wallner.
The PEP verification system.
In FEmSys'97, 1997.
Tool presentation. [gzipped Postscript ] [Abstract]

BEFMRWW00
A. Bouajjani, J. Esparza, A. Finkel, O. Maler, P. Rossmanith, B. Willems, and P. Wolper.
An efficient automata approach to some problems on context-free grammars.
Information Processing Letters, 74(5-6):221-227, 2000. [gzipped Postscript ] [Abstract]

BEM97
A. Bouajjani, J. Esparza, and O. Maler.
Reachability analysis of pushdown automata: Application to model-checking.
In Proc. of CONCUR'97, 1997. [gzipped Postscript ] [Abstract]

BEM96
J. Bradfield, J. Esparza, and A. Mader.
An effective tableau system for the linear time mu-calculus.
In F. Meyer auf der Heide and B. Monien, editors, Proc. of ICALP'96, number 1099 in Lecture Notes in Computer Science, pages 98-109. Springer-Verlag, 1996. [gzipped Postscript ] [Abstract]

BE96
O. Burkart and J. Esparza.
More infinite results.
Electronic Notes in Theoretical Computer Science, 6, 1996. [gzipped Postscript ] [Abstract]

BE97
O. Burkart and J. Esparza.
More infinite results.
Bulletin of the EATCS 62 (Concurrency Column), 1997.

CEP95
A. Cheng, J. Esparza, and J. Palsberg.
Complexity results for 1-safe nets.
Theoretical Computer Science, 147:117-136, 1995. [Abstract]

CES91
A. Cruz, J. Esparza, and J. Sesma.
Zeros of the hankel function of real order out of the principal riemann sheet.
Journal of Computational und Applied Mathematics, 37:89-99, 1991.

DEP99
G. Delzanno, J. Esparza, and A. Podelski.
Constraint-based analysis of broadcast protocols.
In Proceedings of CSL '99, number 1683 in Lecture Notes in Computer Science, pages 50-66. [gzipped Postscript ] [Abstract]

DE91
J. Desel and J. Esparza.
Reachability in reversible free choice systems.
In G.Choffrut und M. Jantzen, editor, Proceedings of STACS '91, number 480 in Lecture Notes in Computer Science, pages 384-397, 1991.

DE93
J. Desel and J. Esparza.
Reachability in cyclic extended free-choice systems.
Theoretical Computer Science, 114:93-118, 1993. [Abstract]

DE95a
J. Desel and J. Esparza.
Free Choice Petri Nets.
Cambridge University Press. 1995.

DE95b
J. Desel and J. Esparza.
Free Choice Petri Nets, volume 40 of Cambridge Tracts in Theoretical Computer Science.
Cambridge University Press, 1995.

DE95
J. Desel and J. Esparza.
Shortest paths in reachability graphs.
Journal of Computer and System Sciences, 51(2):314-323, 1995. [Abstract]

Esp90
J. Esparza.
Synthesis rules for Petri nets, und how they lead to new results.
In J.C.M. Baeten und J.W. Klop, editor, Proceedings of CONCUR '90, number 458 in Lecture Notes in Computer Science, pages 182-198, 1990.

Esp92
J. Esparza.
A solution to the covering problem for 1-bounded conflict-free petrinets using linear programming.
Information Processing Letters, 41:313-319, 1992. [Abstract]

Esp94b
J. Esparza.
Model checking using net unfoldings.
Science of Computer Programming, 23:151-195, 1994. [Abstract]

Esp94
J. Esparza.
On the decidabilty of model checking for several mu-calculi and petri nets.
In S. Tison, editor, Proceedings of Trees in Algebra and Programming - CAAP '94, 19th International Colloquium 1994, number 787 in Lecture Notes in Computer Science, pages 115-129, 1994. [Abstract]

Esp94a
J. Esparza.
Reduction and synthesis of live and bounded free choice Petri nets.
Information and Computation, 114(1):50-87, 1994. [Abstract]

Esp96
J. Esparza.
More infinite results.
In Proc. of INFINITY'96, Research Report MIP-9614, University of Passau, 1996. [gzipped Postscript ] [Abstract]

Esp97b
J. Esparza.
Decidability of model-checking for infinite-state concurrent systems.
Acta Informatica, 34:85-107, 1997. [gzipped Postscript ] [Abstract]

Esp97a
J. Esparza.
Petri nets, commutative context-free grammars, and basic parallel processes.
Fundamenta Informaticae, 31:13-26, 1997. [gzipped Postscript ] [Abstract]

Esp98a
J. Esparza.
Decidability and complexity of Petri net problems - an introduction.
In G. Rozenberg and W. Reisig, editors, Lectures on Petri Nets I: Basic Models. Advances in Petri Nets, number 1491 in Lecture Notes in Computer Science, pages 374-428, 1998. [gzipped Postscript ]

Esp98b
J. Esparza.
Reachability in live and safe free-choice Petri nets is NP -complete.
Theoretical Computer Science, 198(1-2):211-224, 1998. [gzipped Postscript ] [Abstract]

EB96
J. Esparza and G. Bruns.
Trapping mutual exclusion in the box calculus.
Theoretical Computer Science, 153(1):95-128, 1996.

EFM99
J. Esparza, A. Finkel, and R. Mayr.
On the verification of broadcast protocols.
In Proceedings of LICS '99, pages 352-359. IEEE Computer Society, 1999. [gzipped Postscript ] [Abstract]

EHRS00a
J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon.
Efficient algorithms for model checking pushdown systems.
Technical Report TUM-I0002, SFB-Bericht 342/1/00 A, Technische Universität München, Institut für Informatik, February 2000. [gzipped Postscript ] [Abstract]

EHRS00b
J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon.
Efficient algorithms for model checking pushdown systems.
In Proc. of CAV'2000, number 1855 in Lecture Notes in Computer Science, pages 232-247. Springer-Verlag, 2000. [gzipped Postscript ] [Abstract]

EH00
J. Esparza and K. Heljanko.
A new unfolding approach to LTL model checking.
In U. Montanari, J. D. P. Rolim, and E. Welzl, editors, Proceedings of the 27th International Conference on Automata, Languages, and Programming, number 1853 in Lecture Notes in Computer Science, pages 475-486. Springer-Verlag, July 2000. [gzipped Postscript ]

EH01
J. Esparza and K. Heljanko.
Implementing LTL model checking with net unfoldings.
Research Report A68, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, March 2001.
To appear in the Proceedings of the SPIN Workshop 2001. [gzipped Postscript ] [Abstract]

EK95
J. Esparza and A. Kiehn.
On the model checking problem for branching time logics and basic parallel processes.
In Proc. of CAV'95, number 939 in Lecture Notes in Computer Science, pages 353-366. Springer-Verlag, 1995. [gzipped Postscript ] [Abstract]

EK99
J. Esparza and J. Knoop.
An automata-theoretic approach to interprocedural dataflow analysis.
In W. Thomas, editor, Proceedings von FOSSACS'99, number 1578 in Lecture Notes in Computer Science, pages 14-30, 1999. [gzipped Postscript ] [Abstract]

EKS01
J. Esparza, A. Kucera, and S. Schwoon.
Model-checking LTL with regular valuations for pushdown systems.
In Proc. of TACS'2001, number 2215 in Lecture Notes in Computer Science, pages 306-339, 2001. [gzipped Postscript ] [Abstract]

ELS99
J. Esparza, J.L. Lopez, and J. Sesma.
Zeros of the Whittaker function associated to Coulomb waves.
IMA Journal of Applied Mathematics, 63(1):71-88, 1999. [Abstract]

EM97
J. Esparza and S. Melzer.
Model checking LTL using constraint programming.
In Proc. of Application and Theory of Petri Nets'97, 1997. [gzipped Postscript ] [Abstract]

EM00
J. Esparza and S. Melzer.
Verification of safety properties using integer programming: Beyond the state equation.
Formal Methods in System Design, 16:159-189, 2000. [gzipped Postscript ] [Abstract]

EN94
J. Esparza and M. Nielsen.
Decibility issues for Petri nets - a survey.
Journal of Informatik Processing and Cybernetics, 30(3):143-160, 1994. [gzipped Postscript ] [Abstract]

EP00
J. Esparza and A. Podelski.
Efficient algorithms for pre * and post * on interprocedural parallel flow graphs.
In Proc. of POPL'2000, pages 1-11. ACM Press, 2000. [gzipped Postscript ]

ER99
J. Esparza and S. Römer.
An unfolding algorithm for synchronous products of transition systems.
In Proc. of CONCUR'99, number 1664, pages 2-20. Springer-Verlag, 1999. [gzipped Postscript ] [Abstract]

ERV96
J. Esparza, S. Römer, and W. Vogler.
An improvement of McMillan's unfolding algorithm.
In T. Margaria and B. Steffen, editors, Proc. of TACAS'96, number 1055 in Lecture Notes in Computer Science, pages 87-106. Springer-Verlag, 1996. [gzipped Postscript ] [Abstract]

ERV01
J. Esparza, S. Römer, and W. Vogler.
An improvement of McMillan's unfolding algorithm.
Formal Methods in System Design, 2001.
To appear. [gzipped Postscript ] [Abstract]

ER97
J. Esparza and P. Rossmanith.
An automata approach to some problems on context-free grammars.
In R. Valk C. Freksa, M. Jantzen, editor, Foundations of Computer Science, Potential - Theory - Cognition, number 1337 in Lecture Notes in Computer Science, pages 143-152, 1997. [gzipped Postscript ] [Abstract]

ERS00
J. Esparza, P. Rossmanith, and S. Schwoon.
A uniform framework for problems on context-free grammars.
EATCS Bulletin, 72:169-177, October 2000. [gzipped Postscript ]

ES00
J. Esparza and C. Schröter.
Reachability Analysis Using Net Unfoldings.
In H. D. Burkhard, L. Czaja, A. Skowron, and P. Starke, editors, Workshop of Concurrency, Specification & Programming, volume II of Informatik-Bericht 140, pages 255-270. Humboldt-Universität zu Berlin, 2000. [gzipped Postscript ]

ES01a
J. Esparza and C. Schröter.
Net reductions for LTL model-checking.
In Proc. of 11th CHARME, Livingston, Scotland, 2001. [gzipped Postscript ]

ES02
J. Esparza and C. Schröter.
Fundamenta Informaticae, 2002. [gzipped Postscript ]

ES01
J. Esparza and S. Schwoon.
A BDD-based model checker for recursive programs.
In Proc. of CAV'01, number 2102 in Lecture Notes in Computer Science, pages 324-336. Springer-Verlag, 2001. [gzipped Postscript ]

ES90b
J. Esparza and M. Silva.
Circuits, handles, bridges and nets.
In G. Rozenberg, editor, Advances in Petri Nets 1990, number 483 in Lecture Notes in Computer Science, pages 210-242, 1990.

ES90a
J. Esparza and M. Silva.
On the analysis und synthesis of free choice systems.
In G Rozenberg., editor, Advances in Petri Nets 1990, number 483 in Lecture Notes in Computer Science, pages 243-286, 1990.

ES91b
J. Esparza and M. Silva.
Compositional synthesis of live und bounded free choice nets.
In J.C.M. Baeten und J.F. Groote, editor, Proceedings of CONCUR '91, number 527 in Lecture Notes in Computer Science, pages 172-187, 1991.

ES91a
J. Esparza and M. Silva.
Top-down synthesis of free choice nets.
In G. Rozenberg, editor, Advances in Petri Nets 1991, number 524 in Lecture Notes in Computer Science, pages 118-139, 1991.

ES92
J. Esparza and M. Silva.
A polynomial time algorithm to decide liveness of bounded free choice nets.
Theoretical Computer Science, 102:185-205, 1992. [Abstract]

ES93
J. Esparza and B. von Stengel:.
The asynchronous committee meeting problem.
In Jan van Leuween, editor, Proceedings of WG '93, Graph-Theoretic in Computer Science, 19th International Workshop, number 790 in Lecture Notes in Computer Science, pages 276-287, 1993. [gzipped Postscript ] [Abstract]

JE95
P. Jancar and J. Esparza.
Deciding finiteness of Petri nets up to bisimulation.
SFB-Bericht Nr. 342/23/95A, TU München, 1995. [gzipped Postscript ] [Abstract]

JE96
P. Jancar and J. Esparza.
Deciding finiteness of Petri nets up to bisimulation.
In F. Meyer, der Heider, and B. Monien, editors, Proc. of ICALP'96, number 1099 in Lecture Notes in Computer Science, pages 478-489. Springer-Verlag, 1996. [gzipped Postscript ] [Abstract]

JEM99
P. Jancar, J. Esparza, and F. Moller.
Petri nets and regular behaviours.
Journal of Computer and System Sciences, 59(3):476-503, 1999. [gzipped Postscript ] [Abstract]

KEB94
M. Koutny, J. Esparza, and E. Best.
Operational semantics for the Petri box calculus.
In B. Jonsson and J. Parrow, editors, Proceedings of CONCUR '94, number 836 in Lecture Notes in Computer Science, pages 210-225, 1994. [Abstract]

KE96
A. Kovalyov and J. Esparza.
A polynomial algorithm to compute the concurrency relation of free-choice signal transition graphs.
In Prof. of the International Workshop on Discrete Event Systems, WODES'96, pages 1-6, Edinburgh, 1996. The Institution of Electrical Engineers. [gzipped Postscript ] [Abstract]

ME96
S. Melzer and J. Esparza.
Checking system properties via integer programming.
In Proc. of ESOP'96, Lecture Notes in Computer Science. Springer-Verlag, 1996. [gzipped Postscript ] [Abstract]

MRE96
S. Melzer, S. Römer, and J. Esparza.
Verification using PEP (tool presentation).
In M. Wirsing and M. Nivat, editors, Proc. of AMAST'96, number 1101 in Lecture Notes in Computer Science, pages 591-594. Springer-Verlag, 1996. [gzipped Postscript ] [Abstract]

PE00
L. Prensa Nieto and J. Esparza.
Verifying single and multi-mutator garbage collectors with Owicki-Gries in Isabelle/HOL.
In M. Nielsen and B. Rovan, editors, Proceedings of the 25th Conference on Mathematical Foundations of Computer Science, number 1893 in Lecture Notes in Computer Science, pages 619-628. Springer-Verlag, 2000. [gzipped Postscript ] [Abstract]

RE99
C. Röckl and J. Esparza.
Proof-checking protocols using bisimulations.
In J. C. M. Baeten and S. Mauw, editors, Proc. of CONCUR'99, number 1664 in Lecture Notes in Computer Science, pages 525-540. Springer-Verlag, 1999. [gzipped Postscript ] [Abstract]

RE00
C. Röckl and J. Esparza.
On the mechanized verification of infinite systems.
In A. Bode and T. Ludwig, editors, Proc. SFB 342 Final Colloquium, pages 31-52. Technische Universität München, 2000.
Published as Technical Report. [gzipped Postscript ]

SSE02
C. Schröter, S. Schwoon, and J. Esparza.
The Model-Checking Kit.
In Proceedings of Toolsday-Workshop (satellite event of CONCUR'02), Report Series FIMU-RS-2002-05, pages 22-31, Masaryk University, Brno, 2002. [gzipped Postscript ]

KE99
A. Kucera und J. Esparza.
A logical viewpoint on process-algebraic quotients.
In Proc. of CSL'99, number 1683, pages 499-514. Springer-Verlag, 1999. [gzipped Postscript ] [Abstract]