To appear |
|
Stefan Kiefer, Michael Luttenberger, and Javier Esparza. On the convergence of Newton's method for monotone systems of polynomial equations. In Proceedings of the 39th ACM Symposium on Theory of Computing (STOC), San Diego, California, USA, to appear. |
|
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. An extension of Newton's method to  -continuous semirings. In Proceedings of the 11th International Conference on Developments in Language Theory (DLT), Lecture Notes in Computer Science, Turku, Finland, to appear. |
|
2007 |
|
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. On fixed point equations over commutative semirings. In Wolfgang Thomas and Pascal Weil, editors, Proceedings of the 24th International Symposium on Theoretical Aspects of Computer Science, volume 4393 of Lecture Notes in Computer Science, pages 296–307, Aachen, Germany, 2007. |
|
|
Javier Esparza, Pradeep Kanade, and Stefan Schwoon. A negative result on depth-first unfoldings. Software Tools for Technology Transfer, 2007. |
|
2006 |
|
Dejvuth Suwimonteerabuth, Stefan Schwoon, and Javier Esparza. Efficient algorithms for alternating pushdown systems with an application to the computation of certificate chains. In Susanne Graf and Wenhui Zhang, editors, 4th International Symposium on Automated Technology for Verification and Analysis (ATVA), volume 4218 of Lecture Notes in Computer Science, pages 141–153, Beijing, China, October 2006. Springer. |
|
|
J. Esparza, P. Jančar, and A. Miller. On the complexity of consistency and complete state coding. In Proceedings of the 6th International Conference on Application of Concurrency to System Design (ACSD 2006), Turku, Finland, June 2006. IEEE Computer Society. |
|
|
A. Bouajjani and J. Esparza. Rewriting models of boolean programs. In Proceedings of RTA 2006, Seattle, USA, 2006. |
|
|
G. Delzanno, J. Esparza, and J. Srba. Monotonic set-extended prefix rewriting and verification of recursive ping-pong protocols. In Proceedings of ATVA 2006, Beijing, China, 2006. |
|
|
Javier Esparza, Stefan Kiefer, and Stefan Schwoon. Abstraction refinement with Craig interpolation and symbolic pushdown systems. In Holger Hermanns and Jens Palsberg, editors, Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2006), pages 489–503, Vienna, Austria, 2006. |
|
|
Javier Esparza, Antonín Kučera, and Richard Mayr. Model checking probabilistic pushdown automata. Logical Methods in Computer Science, 2006. |
|
2005 |
|
Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, and Jan Strejček. Reachability analysis of multithreaded software with asynchronous communication. In Ramaswamy Ramanujam and Sandeep Sen, editors, Proceedings of FSTTCS 2005, volume 3821 of Lecture Notes in Computer Science. Springer, December 2005. |
|
|
Stefan Schwoon and Javier Esparza. A note on on-the-fly verification algorithms. In Nicolas Halbwachs and Lenore Zuck, editors, Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 3440 of Lecture Notes in Computer Science, pages 174–190, Edinburgh, UK, April 2005. Springer. |
|
|
Dejvuth Suwimonteerabuth, Stefan Schwoon, and Javier Esparza. jMoped: A Java bytecode checker based on Moped. In Nicolas Halbwachs and Lenore Zuck, editors, Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 3440 of Lecture Notes in Computer Science, pages 541–545, Edinburgh, UK, April 2005. Springer. Tool paper. |
|
|
Tomáš Brádzil, Antonín Kučera, and Javier Esparza. Analysis and prediction of the long-run behaviour of probabilistic sequential programs with recursion. In Proceedings of FOCS 2005, pages 521–530, 2005. |
|
|
Javier Esparza, Pierre Ganty, and Stefan Schwoon. Locality-based abstractions. In Proceedings of SAS 2005, volume 3672 of Lecture Notes in Computer Science, pages 118–134, 2005. |
|
|
Javier Esparza, Antonín Kučera, and Richard Mayr. Quantitative analysis of probabilistic pushdown automata: Expectations and variances. In LICS 2005, pages 117–126. IEEE Computer Society, 2005. |
|
|
Ahmed Bouajjani, Javier Esparza, and Tayssir Touili. Reachability analysis of synchronized PA-systems. Electronic Notes in Theoretical Computer Science, 138(3):153–178, 2005. |
|
2004 |
|
Javier Esparza and Kousha Etessami. Verifying probabilistic procedural programs. In Proceedings of FSTTCS 2004, volume 3328 of LNCS, Lecture Notes in Computer Science, pages 16–31, 2004. |
|
|
Ahmed Bouajjani, Javier Esparza, and Tayssir Touili. Reachability analysis of synchronized PA-systems. In Proceedings of Infinity 2004, 2004. |
|
|
Javier Esparza, Antonín Kučera, and Richard Mayr. Model checking probabilistic pushdown automata. In LICS 2004. IEEE Computer Society, 2004. |
|
|
J. Esparza. A polynomial-time algorithm for checking consistency of free-choice signal transition graphs. Fundamenta Informaticae, 62(2):197–220, 2004. |
|
2003 |
|
Javier Esparza, Antonín Kučera, and Stefan Schwoon. Model-checking LTL with regular valuations for pushdown systems. Information and Computation, 186(2):355–376, November 2003. |
|
|
J. Esparza. A polynomial-time algorithm for checking consistency of free-choice signal transition graphs. In Balarin J. Lilius, F and R.J. Machado, editors, Proceedings of the 3rd International Conference on Application of Concurrency to System Design (ACSD 2003), pages 61–70, Guimaraes, Portugal, June 2003. IEEE Computer Society. ISBN 0-7695-1887-7. |
|
|
Alin Ștefănescu, Javier Esparza, and Anca Muscholl. Synthesis of distributed algorithms using asynchronous automata. In Denis Lugiez Roberto Amadio, editor, CONCUR 2003-Concurrency Theory, volume 2761 of LNCS, Lecture Notes in Computer Science, pages 27–41. Springer-Verlag, 2003. ISBN 3-540-40753-7. |
|
|
A. Bouajjani, J. Esparza, and T. Touili. A generic approach to the static analysis of concurrent programs with procedures. In Proc. of the 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '03, 2003. |
|
|
A. Bouajjani, J. Esparza, and T. Touili. A generic approach to the static analysis of concurrent programs with procedures. International Journal on Foundations of Computer Science, 14(4):551–582, 2003. |
|
|
J. Esparza and M. Maidl. Simple representative instantiations for multicast protocols. In H. Garavel and J. Hatcliff, editors, Proc. of TACAS'03, number 2619 in Lecture Notes in Computer Science, pages 128–143. Springer-Verlag, 2003. |
|
|
A. Kučera and J. Esparza. A logical viewpoint on process-algebraic quotients. Journal of Logic and Computation, 13(6):863–880, 2003. |
|
2002 |
|
J. Esparza and C. Lakos, editors. Applications and theory of petri nets 2002, volume 2360 of Lecture Notes in Computer Science. Springer Verlag, 2002. |
|
|
J. Esparza. Grammars as processes. In J. karhuaki W. Brauer, H. Ehrig and A. Salomaa, editors, Formal and Natural Computing, volume 2300 of Lecture Notes in Computer Science. Springer Verlag, 2002. ISBN 3-540-43190-X. |
|
|
J. Esparza, S. Römer, and W. Vogler. An improvement of McMillan's unfolding algorithm. Formal Methods in System Design, 20:285–310, 2002. |
|
|
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. |
|
2001 |
|
J. Esparza and K. Heljanko. Implementing LTL model checking with net unfoldings. In Matthew B. Dwyer, editor, Proceedings of the 8th International SPIN Workshop on Model Checking of Software (SPIN'2001), volume 2057 of Lecture Notes in Computer Science, pages 37–56, Toronto, Canada, May 2001. Springer-Verlag. |
|
|
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. |
|
|
J. Esparza and C. Schröter. Unfolding based algorithms for the reachability problem. Fundamenta Informaticae, 47(3–4):231–245, 2001. |
|
|
J. Esparza and C. Schröter. Net reductions for LTL model-checking. In Proc. of 11th CHARME, volume 2144 of Lecture Notes in Computer Science, pages 310–324, Livingston, Scotland, 2001. |
|
|
J. Esparza, A. Kučera, 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. |
|
2000 |
|
J. Esparza, P. Rossmanith, and S. Schwoon. A uniform framework for problems on context-free grammars. EATCS Bulletin, 72:169–177, October 2000. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
J. Esparza and A. Podelski. Efficient algorithms for it pre and it post on interprocedural parallel flow graphs. In Proc. of POPL'2000, pages 1–11. ACM Press, 2000. |
|
|
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. |
|
|
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. |
|
|
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. |
|
1999 |
|
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, 1999. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
J. Esparza and S. Römer. An unfolding algorithm for synchronous products of transition systems. In Proc. of CONCUR'99, number 1664 in Lecture Notes in Computer Science, pages 2–20. Springer-Verlag, 1999. |
|
|
P. Jančar, J. Esparza, and F. Moller. Petri nets and regular behaviours. Journal of Computer and System Sciences, 59(3):476–503, 1999. |
|
|
A. Kučera and J. Esparza. A logical viewpoint on process-algebraic quotients. In Proc. of CSL'99, number 1683 in Lecture Notes in Computer Science, pages 499–514. Springer-Verlag, 1999. |
|
|
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. |
|
1998 |
|
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. |
|
J. Esparza. Reachability in live and safe free-choice Petri nets is  -complete. Theoretical Computer Science, 198(1–2):211–224, 1998. |
|
1997 |
|
O. Burkart and J. Esparza. More infinite results. Bulletin of the EATCS 62 (Concurrency Column), 1997. |
|
|
E. Best, J. Esparza, B. Grahlmann, S. Melzer, S. Römer, and F. Wallner. The PEP verification system. In FEmSys'97, 1997. Tool presentation. |
|
|
A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In Proc. of CONCUR'97, 1997. |
|
|
J. Esparza and S. Melzer. Model checking LTL using constraint programming. In Proc. of Application and Theory of Petri Nets'97, 1997. |
|
|
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. |
|
|
J. Esparza. Petri nets, commutative context-free grammars, and basic parallel processes. Fundamenta Informaticae, 31:13–26, 1997. |
|
|
J. Esparza. Decidability of model-checking for infinite-state concurrent systems. Acta Informatica, 34:85–107, 1997. |
|
1996 |
|
O. Burkart and J. Esparza. More infinite results. Electronic Notes in Theoretical Computer Science, 6, 1996. |
|
|
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. |
|
|
J. Esparza and G. Bruns. Trapping mutual exclusion in the box calculus. Theoretical Computer Science, 153(1):95–128, 1996. |
|
|
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. |
|
|
J. Esparza. More infinite results. In Proc. of INFINITY'96, Research Report MIP-9614, University of Passau, 1996. |
|
|
P. Jancar and J. Esparza. Deciding finiteness of Petri nets up to bisimulation. In F. Meyer auf der Heide and B. Monien, editors, Proc. of ICALP'96, number 1099 in Lecture Notes in Computer Science, pages 478–489. Springer-Verlag, 1996. |
|
|
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. |
|
|
S. Melzer and J. Esparza. Checking system properties via integer programming. In Proc. of ESOP'96, Lecture Notes in Computer Science. Springer-Verlag, 1996. |
|
|
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. |
|
1995 |
|
A. Cheng, J. Esparza, and J. Palsberg. Complexity results for 1-safe nets. Theoretical Computer Science, 147:117–136, 1995. |
|
|
J. Desel and J. Esparza. Shortest paths in reachability graphs. Journal of Computer and System Sciences, 51(2):314–323, 1995. |
|
|
J. Desel and J. Esparza. Free choice Petri nets, volume 40 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1995. |
|
|
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. |
|
|
J. Esparza. Petri nets, commutative context-free grammars, and basic parallel processes. In B. Reichel, editor, Proceedings of FCT '95, number 965 in Lecture Notes in Computer Science, pages 221–232, 1995. |
|
|
Allan Cheng, Javier Esparza, and Jens Palsberg. Complexity results for 1-safe nets. Theoretical Computer Science, 147(1&2):117–136, 1995. |
|
1994 |
|
J. Esparza and M. Nielsen. Decibility issues for Petri nets - a survey. Journal of Informatik Processing and Cybernetics, 30(3):143–160, 1994. |
|
|
J. Esparza. On the decidability 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. |
|
|
J. Esparza. Reduction and synthesis of live and bounded free choice Petri nets. Information and Computation, 114(1):50–87, 1994. |
|
|
J. Esparza. Model checking using net unfoldings. Science of Computer Programming, 23:151–195, 1994. |
|
|
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. |
|
1993 |
|
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. |
|
|
J. Desel and J. Esparza. Reachability in cyclic extended free-choice systems. Theoretical Computer Science, 114:93–118, 1993. |
|
|
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. |
|
1992 |
|
E. Best, J. Desel, and J. Esparza. Traps characterise home states in free choice systems. Theoretical Computer Science, 101:161–176, 1992. |
|
|
J. Esparza and M. Silva. A polynomial time algorithm to decide liveness of bounded free choice nets. Theoretical Computer Science, 102:185–205, 1992. |
|
|
J. Esparza. A solution to the covering problem for 1-bounded conflict-free petri nets using linear programming. Information Processing Letters, 41:313–319, 1992. |
|
1991 |
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
1990 |
|
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. |
|
|
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. |
|
|
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. |
|
bibdb) |
© University of Stuttgart |
legal notice