Bild mit Unilogo
homeicon university sucheicon search siteicon sitemap kontakticon contact impressicon legal notice
unilogo University of Stuttgart 
Institute of Formal Methods in Computer Science

SZS - All Publications

 

To appear

Toni Jussila, Keijo Heljanko, and Ilkka Niemelä. BMC via on-the-fly determinization. STTT - International Journal on Software Tools for Technology Transfer, to appear.
Info
See www.tcs.hut.fi ...
Conference version
Volker Diekert, Tero Harju, and Dirk Nowotka. Weinbaum factorizations of primitive words. Izvestiya VUZ Matematika, to appear.
GZipped PostScript (148 kB)
PDF (186 kB)
Info
Tech report version
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.
GZipped PostScript (192 kB)
PDF (183 kB)
Info
Tero Harju and Dirk Nowotka. Periodicity and unbordered words: A proof of the extended duval conjecture. J. Assoc. Comput. Mach., to appear.
GZipped PostScript (201 kB)
PDF (229 kB)
Info
Journal version
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.
GZipped PostScript (178 kB)
PDF (167 kB)
Info
Tech report version

2007

Dejvuth Suwimonteerabuth, Felix Berger, Stefan Schwoon, and Javier Esparza. jMoped: A test environment for Java programs. In Proceedings of CAV 2007, July 2007. Tool paper. To appear.
Info
Paolo Baldan, Andrea Corradini, Barbara König, and Stefan Schwoon. McMillan's complete prefix for contextual nets. In Proceedings of UFO 2007, June 2007. To appear.
Info
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. An extension of Newton's method to -continuous semirings. Technical report, Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik, March 2007.
GZipped PostScript (196 kB)
PDF (193 kB)
Info
Conference version
Javier Esparza, Pradeep Kanade, and Stefan Schwoon. A negative result on depth-first unfoldings. Software Tools for Technology Transfer, 2007.
GZipped PostScript (80 kB)
PDF (184 kB)
Info
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 (STACS), volume 4393 of Lecture Notes in Computer Science, pages 296–307, Aachen, Germany, 2007.
GZipped PostScript (179 kB)
PDF (162 kB)
Info
Tech report version
Javier Esparza, Dirk Nowotka, and Jiri Srba. Deterministic context-free model checking. Technical report, Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik, Germany, January 2007.
GZipped PostScript (198 kB)
PDF (249 kB)
Info

2006

Javier Esparza, Stefan Kiefer, and Michael Luttenberger. On fixed point equations over commutative semirings. Technical report, Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik, December 2006.
GZipped PostScript (217 kB)
PDF (214 kB)
Info
Conference version
Prasad Naldurg, Stefan Schwoon, Sriram Rajamani, and John Lambert. NETRA: Seeing through access control. In Andrew D. Gordon and David Sands, editors, Proceedings of the 4th ACM Workshop on Formal Methods in Security Engineering (FMSE), pages 55–66, Alexandria, USA, November 2006.
PDF (794 kB)
Info
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.
PDF (243 kB)
Info
Tech report version
Hao Wang, Somesh Jha, Thomas Reps, Stefan Schwoon, and Stuart Stubblebine. Reducing the dependence of SPKI/SDSI on PKI. In Dieter Gollmann, Jan Meier, and Andrei Sabelfeld, editors, Proceedings of the 11th European Symposium on Research in Computer Security (ESORICS), volume 4189 of Lecture Notes in Computer Science, pages 156–173, Hamburg, Germany, September 2006. Springer.
PDF (281 kB)
Info
Tech report version
J. Esparza, P. Jančar, and A. Miller. On the complexity of consistency and complete state coding. Technical report, University of Stuttgart, July 2006.
GZipped PostScript (126 kB)
PDF (184 kB)
Info
Conference version
Volker Diekert, Tero Harju, and Dirk Nowotka. Weinbaum factorizations of primitive words. TUCS Tech. Rep. 780, Turku Centre of Computer Science, Finland, July 2006.
PDF (203 kB)
Info
Journal version
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.
GZipped PostScript (101 kB)
PDF (127 kB)
Info
Tech report version
Tero Harju and Dirk Nowotka. Binary words with few squares. Bull. EATCS, 89:164–166, June 2006.
GZipped PostScript (94 kB)
PDF (108 kB)
Info
Tech report version
Alin Stefanescu. Automatic synthesis of distributed transition systems. PhD thesis, Universität Stuttgart, February 2006.
PDF (2 MB)
Info
Slides 
A. Bouajjani and J. Esparza. Rewriting models of boolean programs. In Proceedings of RTA 2006, Seattle, USA, 2006.
GZipped PostScript (101 kB)
PDF (79 kB)
Info
Tech report version
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.
GZipped PostScript (180 kB)
PDF (230 kB)
Info
Tech report version
G. Delzanno, J. Esparza, and J. Srba. Monotonic set-extended prefix rewriting and verification of recursive ping-pong protocols. Technical report, BRICS, 2006.
GZipped PostScript (227 kB)
PDF (304 kB)
Info
Conference version
Javier Esparza, Antonín Kučera, and Richard Mayr. Model checking probabilistic pushdown automata. Logical Methods in Computer Science, 2006.
PDF (403 kB)
Info
Tech report version, Conference version
Javier Esparza, Stefan Kiefer, and Stefan Schwoon. Abstraction refinement with Craig interpolation and symbolic pushdown systems. Technical Report 2006/02, Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik, January 2006.
GZipped PostScript (219 kB)
PDF (219 kB)
Info
Conference version
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), volume 3920 of Lecture Notes in Computer Science, pages 489–503, Vienna, Austria, 2006.
GZipped PostScript (182 kB)
PDF (174 kB)
Info
Tech report version
Paolo Baldan, Stefan Haar, and Barbara König. Distributed unfolding of Petri nets. In Proc. of FOSSACS '06, pages 126–141. Springer, 2006. LNCS 3921.
Info
Paolo Baldan, Andrea Corradini, Tobias Heindel, Barbara König, and Paweł Sobociński. Processes for adhesive rewriting systems. In Proc. of FOSSACS '06, pages 202–216. Springer, 2006. LNCS 3921.
Info
Barbara König and Vitali Kozioura. Counterexample-guided abstraction refinement for the analysis of graph transformation systems. In Proc. of TACAS '06, pages 197–211. Springer, 2006. LNCS 3920.
Info
Barbara König and Vitali Kozioura. Augur 2—a new version of a tool for the analysis of graph transformation systems. In Proc. of GT-VMT '06 (Workshop on Graph Transformation and Visual Modeling Techniques), 2006. ENTCS. to appear.
Info
Paolo Baldan, Stefan Haar, and Barbara König. Distributed unfolding of Petri nets. Technical Report CS-2006-1, Dipartimento di Informatica, Università Ca' Foscari di Venezia, 2006.
PDF (302 kB)
Info
Barbara König and Vitali Kozioura. Counterexample-guided abstraction refinement for the analysis of graph transformation systems. Technical Report 01/2006, Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik, 2006.
PDF (282 kB)
Info
Michael Luttenberger. Reachability analysis of procedural programs with affine integer arithmetic. In Oscar H. Ibarra and Hsu-Chun Yen, editors, Proceedings of the 11th Conference on Implementation and Application of Automata, volume 4094 of LNCS, 2006.
PDF (180 kB)
Info
Tero Harju and Dirk Nowotka. On unique factorizations of primitive words. Theoret. Comput. Sci., 356(1–2):186–189, 2006.
GZipped PostScript (106 kB)
PDF (127 kB)
Info
Tech report version
Tero Harju and Dirk Nowotka. Periods in word extensions. TUCS Tech. Rep. 736, Turku Centre of Computer Science, Finland, January 2006.
GZipped PostScript (595 kB)
PDF (125 kB)
Info
Journal version
Tero Harju and Dirk Nowotka. Periods in word extensions. Acta Inform., 43(2):165–171, 2006.
GZipped PostScript (111 kB)
PDF (136 kB)
Info
Tech report version
Tero Harju and Dirk Nowotka. Binary words with few squares. TUCS Tech. Rep. 737, Turku Centre of Computer Science, Finland, January 2006.
GZipped PostScript (582 kB)
PDF (93 kB)
Info
Journal version
Claus Schröter. Halbordnungs- und Reduktionstechniken für die automatische Verifikation von verteilten Systemen. PhD thesis, Universität Stuttgart, 2006.
GZipped PostScript (712 kB)
PDF (1 MB)
Info
Somesh Jha, Stefan Schwoon, Hao Wang, and Thomas Reps. Weighted pushdown systems and trust-management 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), volume 3920 of Lecture Notes in Computer Science, pages 1–26, Vienna, Austria, 2006. Springer. Invited paper.
PDF (357 kB)
Info
Tech report version
Dejvuth Suwimonteerabuth, Stefan Schwoon, and Javier Esparza. Efficient algorithms for alternating pushdown systems: Application to certificate chain discovery with threshold subjects. Technical Report 2006/09, Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik, 2006.
GZipped PostScript (216 kB)
Info
Conference version

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, pages 348–359. Springer, December 2005.
GZipped PostScript (51 kB)
Info
Tech report version
Barbara König and Vitali Kozioura. Augur—a tool for the analysis of graph transformation systems. EATCS Bulletin, 87:125–137, November 2005. Appeared in The Formal Specification Column.
GZipped PostScript (172 kB)
PDF (256 kB)
Info
Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, and Jan Strejček. Reachability analysis of multithreaded software with asynchronous communication. Technical Report 2005/06, Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik, November 2005.
GZipped PostScript (65 kB)
PDF (183 kB)
Info
Conference version
Tero Harju and Dirk Nowotka. On unique factorizations of primitive words. TUCS Tech. Rep. 714, Turku Centre of Computer Science, Finland, October 2005.
GZipped PostScript (582 kB)
PDF (115 kB)
Info
Journal version
Thomas Reps, Stefan Schwoon, Somesh Jha, and David Melski. Weighted pushdown systems and their application to interprocedural dataflow analysis. Science of Computer Programming, 58(1–2):206–263, October 2005. Special Issue on the Static Analysis Symposium 2003.
GZipped PostScript (942 kB)
Info
Conference version, Tech report version
Stefan Schwoon, Hao Wang, Somesh Jha, and Thomas Reps. Distributed certificate-chain discovery in SPKI/SDSI. Technical Report TR-1526, Computer Sciences Department, University of Wisconsin, August 2005.
GZipped PostScript (160 kB)
Info
Conference version
Hao Wang, Somesh Jha, Thomas Reps, Stefan Schwoon, and Stuart Stubblebine. Reducing the dependence of trust-management systems on PKI. Technical Report TR-1527, Computer Sciences Department, University of Wisconsin, August 2005.
GZipped PostScript (126 kB)
Info
Conference version
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.
GZipped PostScript (89 kB)
Info
Tech report version
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.
GZipped PostScript (82 kB)
Info
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.
GZipped PostScript (171 kB)
PDF (157 kB)
Info
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.
PDF (256 kB)
Info
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.
GZipped PostScript (158 kB)
PDF (178 kB)
Info
Tech report version
Javier Esparza, Antonín Kučera, and Richard Mayr. Quantitative analysis of probabilistic pushdown automata: Expectations and variances. Technical Report FIMU-RS-2005-07, Masaryk University, 2005.
PDF (253 kB)
Info
Conference version
Ahmed Bouajjani, Javier Esparza, and Tayssir Touili. Reachability analysis of synchronized PA-systems. Electronic Notes in Theoretical Computer Science, 138(3):153–178, 2005.
GZipped PostScript (76 kB)
PDF (137 kB)
Info
Conference version
Stefan Kiefer. Abstraction refinement for pushdown systems. Master's thesis, Universität Stuttgart, 2005.
GZipped PostScript (329 kB)
PDF (557 kB)
Info
Slides 
Barbara König. Analysing input/output-capabilities of mobile processes with a generic type system. Journal of Logic and Algebraic Programming, 63(1):35–58, 2005.
Info
Barbara König, Ugo Montanari, and Philippa Gardner, editors. Abstracts Collection – Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems, Dagstuhl Seminar Proceedings 04241, 2005.
PDF (351 kB)
Info
See drops.dagstuhl.de ...
Paolo Baldan, Barbara König, and Arend Rensink. Graph grammar verification through abstraction. In Abstracts Collection – Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems, Dagstuhl Seminar Proceedings 04241, 2005.
PDF (330 kB)
Info
See drops.dagstuhl.de ...
Barbara König. A general framework for types in graph rewriting. Acta Informatica, 42(4-5):349–388, 2005.
Info
Hermann Gruber, Markus Holzer, Astrid Kiehn, and Barbara König. On timed automata with discrete time—structural and language theoretical characterization. In Proc. of DLT '05 (Developments in Language Theory), pages 272–283. Springer, 2005. LNCS 3572.
GZipped PostScript (81 kB)
PDF (144 kB)
Info
Paolo Baldan, Andrea Corradini, Javier Esparza, Tobias Heindel, Barbara König, and Vitali Kozioura. Verifying red-black trees. In Proc. of COSMICAH '05, 2005. Proceedings available as report RR-05-04 (Queen Mary, University of London).
GZipped PostScript (101 kB)
PDF (175 kB)
Info
Reiko Heckel, Barbara König, and Arend Rensink, editors. Proc. of GT-VC '05 (Graph Transformation for Verification and Concurrency), number 05–34 in CTIT Technical Reports. Centre for Telematics and Information Technology, University of Twente, 2005.
Info
See trese.cs.utwente.nl ...
Tero Harju, Arto Lepistö, and Dirk Nowotka. A characterization of periodicity of bi-infinite words. Theoret. Comput. Sci., 347(1–2):419–422, 2005.
GZipped PostScript (95 kB)
PDF (75 kB)
Info
Tech report version
Tero Harju and Dirk Nowotka. On the equation in a free semigroup. Theoret. Comput. Sci., 330(1):117–121, 2005.
GZipped PostScript (129 kB)
PDF (107 kB)
Info
Tech report version
Tero Harju and Dirk Nowotka. Counting bordered and primitive words with a fixed weight. Theoret. Comput. Sci., 340(2):273–279, 2005.
GZipped PostScript (165 kB)
PDF (112 kB)
Info
Tech report version
Keijo Heljanko and Alin Stefanescu. Complexity results for checking distributed implementability. In Proceedings of the 5th International Conference on Application of Concurrency to System Design (ACSD 2005), pages 78–87, 2005.
GZipped PostScript (119 kB)
PDF (258 kB)
Info
Slides 
Tech report version

2004

Barbara König. Analysis and verification of systems with dynamically evolving structures. Habilitation thesis, Universität Stuttgart, December 2004.
GZipped PostScript (998 kB)
PDF (1 MB)
Info
Timo Latvala, Armin Biere, Keijo Heljanko, and Tommi Junttila. Simple bounded LTL model checking. In Alan Hu and Andy Martin, editors, Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD'04), volume 3312 of Lecture Notes in Computer Science, pages 186–200. Springer, November 2004.
Info
See www.tcs.hut.fi ...
Tech report version
Tero Harju and Dirk Nowotka. Counting bordered and primitive words with a fixed weight. TUCS Tech. Rep. 630, Turku Centre of Computer Science, Finland, November 2004.
GZipped PostScript (668 kB)
PDF (142 kB)
Info
Journal version
Stefan Schwoon and Javier Esparza. A note on on-the-fly verification algorithms. Technical Report 2004/06, Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik, November 2004.
GZipped PostScript (93 kB)
PDF (179 kB)
Info
See www.fmi.uni-stuttgart.de ...
Conference version
Jussi Rintanen, Keijo Heljanko, and Ilkka Niemelä. Parallel encodings of classical planning as satisfiability. In José Júlio Alferes and João Alexandre Leite, editors, Proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA'04), volume 3229 of Lecture Notes in Computer Science, pages 307–319, Lisbon, Portugal, September 2004. Springer.
Info
See www.tcs.hut.fi ...
Tech report version
Timo Latvala, Armin Biere, Keijo Heljanko, and Tommi Junttila. Simple bounded LTL model checking. Research Report A92, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, July 2004.
Info
See www.tcs.hut.fi ...
Markus Holzer and Barbara König. Regular languages, sizes of syntactic monoids, graph colouring, state complexity results, and how these topics are related to each other. EATCS Bulletin, 83:139–155, June 2004. Appeared in The Formal Language Theory Column.
GZipped PostScript (74 kB)
PDF (140 kB)
Info
Markus Holzer and Stefan Schwoon. Reflections on Reflexion – computational complexity considerations on a puzzle game. In Paolo Ferragina and Roberto Grossi, editors, Proceedings of the Third International Conference on FUN with Algorithms, pages 90–105. Università di Pisa, May 2004.
GZipped PostScript (76 kB)
Info
Tero Harju and Dirk Nowotka. On the equation in a free semigroup. TUCS Tech. Rep. 602, Turku Centre of Computer Science, Finland, April 2004.
GZipped PostScript (150 kB)
PDF (130 kB)
Info
Journal version
Jussi Rintanen, Keijo Heljanko, and Ilkka Niemelä. Parallel encodings of classical planning as satisfiability. Technical Report 198, Institute of Computer Science, University of Freiburg, Freiburg, Germany, February 2004.
Info
See www.tcs.hut.fi ...
Markus Holzer and Stefan Schwoon. Assembling molecules in Atomix is hard. Theoretical Computer Science, 303(3):447–462, February 2004.
Info
Tech report version
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.
GZipped PostScript (92 kB)
PDF (243 kB)
Info
Ahmed Bouajjani, Javier Esparza, and Tayssir Touili. Reachability analysis of synchronized PA-systems. In Proceedings of Infinity 2004, 2004.
GZipped PostScript (71 kB)
PDF (174 kB)
Info
Journal version
Javier Esparza, Antonín Kučera, and Richard Mayr. Model checking probabilistic pushdown automata. In LICS 2004. IEEE Computer Society, 2004.
GZipped PostScript (86 kB)
PDF (204 kB)
Info
Tech report version, Journal version
Javier Esparza, Antonín Kučera, and Richard Mayr. Model checking probabilistic pushdown automata. Technical report, Faculty of Informatics, Masaryk University, Brno, 2004.
GZipped PostScript (206 kB)
PDF (738 kB)
Info
Conference version, Journal version
J. Esparza. A polynomial-time algorithm for checking consistency of free-choice signal transition graphs. Fundamenta Informaticae, 62(2):197–220, 2004.
GZipped PostScript (129 kB)
PDF (182 kB)
Info
Conference version
Tobias Heindel. Encoding the -calculus into the calculus of explicit fusions, 2004. Dagstuhl Seminar: Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems.
Info
See www.dagstuhl.de ...
Paolo Baldan, Andrea Corradini, Barbara König, and Bernhard König. Verifying a behavioural logic for graph transformation systems. In Proc. of COMETA '03, volume 104 of ENTCS, pages 5–24. Elsevier, 2004.
GZipped PostScript (183 kB)
PDF (301 kB)
Info
Hartmut Ehrig and Barbara König. Deriving bisimulation congruences in the DPO approach to graph rewriting. In Proc. of FOSSACS '04, pages 151–166. Springer, 2004. LNCS 2987.
GZipped PostScript (130 kB)
PDF (311 kB)
Info
Tech report version
Markus Holzer and Barbara König. On deterministic finite automata and syntactic monoid size. Theoretical Computer Science, 327:319–347, 2004.
Info
Conference version
Hartmut Ehrig and Barbara König. Deriving bisimulation congruences in the DPO approach to graph rewriting. Technical Report 01/2004, Universität Stuttgart, 2004.
GZipped PostScript (554 kB)
PDF (1017 kB)
Info
See inf4.informatik.uni-stuttgart.de ...
Conference version
Paolo Baldan, Andrea Corradini, and Barbara König. Verifying finite-state graph grammars: an unfolding-based approach. In Proc. of CONCUR '04, pages 83–98. Springer-Verlag, 2004. LNCS 3170.
GZipped PostScript (139 kB)
PDF (231 kB)
Info
Tech report version
Paolo Baldan, Barbara König, and Ingo Stürmer. Generating test cases for code generators by unfolding graph transformation systems. In Proc. of ICGT '04 (International Conference on Graph Transformation), pages 194–209. Springer-Verlag, 2004. LNCS 3256.
GZipped PostScript (233 kB)
PDF (225 kB)
Info
Paolo Baldan, Andrea Corradini, and Barbara König. An unfolding-based approach for the verification of finite-state graph grammars. Technical Report CS-2004-10, Dipartimento di Informatica, Università Ca' Foscari di Venezia, 2004.
GZipped PostScript (225 kB)
PDF (343 kB)
Info
See www.dsi.unive.it ...
Conference version
Fernando Luís Dotti, Barbara König, Osmar Marchi dos Santos, and Leila Ribeiro. A case study: Verifying a mutual exclusion protocol with process creation using graph transformation systems. Technical Report 08/2004, Universität Stuttgart, 2004.
GZipped PostScript (324 kB)
PDF (532 kB)
Info
See inf4.informatik.uni-stuttgart.de ...
Herrman Gruber, Markus Holzer, Astrid Kiehn, and Barbara König. On timed automata with discrete time—structural and language theoretical characterization. In 14. Theorietag der GI-Fachgruppe 0.1.5 ``Automaten und Formale Sprachen''. Universität Potsdam, 2004.
Info
Matthias Hopf, Michael Luttenberger, and Thomas Ertl. Hierarchical splatting of scattered 4d data. IEEE Computer Graphics and Applications, 24(04):64–72, 2004.
Info
Michael Luttenberger. Effiziente Berechnung optimaler Strategien für Paritätsspiele. Master's thesis, Universität Stuttgart, 2004. In German.
Info
Tero Harju and Dirk Nowotka. Periodicity and unbordered words. In STACS 2004 (Montpellier), volume 2996 of Lecture Notes in Comput. Sci., pages 294–304, Berlin, 2004. Springer-Verlag.
GZipped PostScript (67 kB)
PDF (119 kB)
Info
Tech report version
Tero Harju and Dirk Nowotka. The equation in a free semigroup. Semigroup Forum, 68(3):488–490, 2004.
GZipped PostScript (40 kB)
PDF (70 kB)
Info
Tech report version
Tero Harju and Dirk Nowotka. Minimal Duval extensions. Internat. J.,Found. Comput. Sci., 15(2):349–354, 2004.
GZipped PostScript (53 kB)
PDF (94 kB)
Info
Tech report version
Tero Harju and Dirk Nowotka. Border correlation of binary words. J. Combin. Theory, Ser A, 108(2):331–341, 2004.
GZipped PostScript (150 kB)
PDF (140 kB)
Info
Tech report version
Dirk Nowotka. Periodicity and unbordered factors of words. PhD thesis, University of Turku, 2004.
GZipped PostScript (414 kB)
PDF (545 kB)
Info
C. Schröter and V. Khomenko. Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings. In R. Alur and D. A. Peled, editors, Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04), volume 3114 of Lecture Notes in Computer Science, pages 109–121. Springer-Verlag, 2004.
GZipped PostScript (190 kB)
Info
Keijo Heljanko and Alin Stefanescu. Complexity results for checking distributed implementability. Technical Report 05/2004, Universität Stuttgart, 2004.
PDF (324 kB)
Info
Slides 
Dejvuth Suwimonteerabuth. Verifying Java bytecode with the Moped model checker. Master's thesis, Universität Stuttgart, 2004.
GZipped PostScript (227 kB)
Info
See www.fmi.uni-stuttgart.de ...

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.
GZipped PostScript (202 kB)
PDF (214 kB)
Info
Conference version
Tero Harju and Dirk Nowotka. The equation in a free semigroup. TUCS Tech. Rep. 561, Turku Centre of Computer Science, Finland, October 2003.
GZipped PostScript (91 kB)
PDF (97 kB)
Info
Journal version
Alin Stefanescu, Javier Esparza, and Anca Muscholl. Synthesis of distributed algorithms using asynchronous automata. In R. Amadio and D. Lugiez, editors, Proceedings of the 14th International Conference on Concurrency Theory (CONCUR'03), volume 2761, pages 27–41. Springer, September 2003.
PDF (242 kB)
Info
Full versionSlidesImplementation
Tero Harju and Dirk Nowotka. About Duval extensions. In T. Harju and J. Karhumäki, editors, WORDS 2003 (Turku), volume 27 of TUCS General Publications, pages 392–397, Finland, August 2003. Turku Centre of Computer Science.
GZipped PostScript (49 kB)
PDF (88 kB)
Info
Tero Harju, Arto Lepistö, and Dirk Nowotka. A characterization of periodicity of bi-infinite words. TUCS Tech. Rep. 545, Turku Centre of Computer Science, Finland, August 2003.
GZipped PostScript (88 kB)
PDF (91 kB)
Info
Journal version
Tero Harju and Dirk Nowotka. Border correlation of binary words. TUCS Tech. Rep. 546, Turku Centre of Computer Science, Finland, August 2003.
GZipped PostScript (124 kB)
PDF (150 kB)
Info
Journal version
Toni Jussila, Keijo Heljanko, and Ilkka Niemelä. BMC via on-the-fly determinization. In Ofer Strichman and Armin Biere, editors, Electronic Notes in Theoretical Computer Science, volume 89. Elsevier, July 2003.
Info
See www.tcs.hut.fi ...
Stefan Kiefer. Die Menge der virtuellen Verbindungen im Spiel Hex ist PSPACE-vollständig. Studienarbeit Nr. 1887, Universität Stuttgart, Juli 2003. In German.
GZipped PostScript (280 kB)
PDF (375 kB)
Info
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.
GZipped PostScript (66 kB)
PDF (147 kB)
Info
Tuomo Pyhälä and Keijo Heljanko. Specification coverage aided test selection. In Johan Lilius, Felice Balarin, and Ricardo J. Machado, editors, Proceeding of the 3rd International Conference on Application of Concurrency to System Design (ACSD'2003), pages 187–195, Guimaraes, Portugal, June 2003. IEEE Computer Society.
Info
See www.tcs.hut.fi ...
Thomas Reps, Stefan Schwoon, and Somesh Jha. Weighted pushdown systems and their application to interprocedural dataflow analysis. In Radhia Cousot, editor, Proceedings of the 10th International Static Analysis Symposium, volume 2694 of Lecture Notes in Computer Science, pages 189–213. Springer, June 2003.
GZipped PostScript (250 kB)
Info
See www.fmi.uni-stuttgart.de ...
Tech report version, Journal version
Stefan Schwoon, Somesh Jha, Thomas Reps, and Stuart Stubblebine. On generalized authorization problems. In Proceedings of the 16th IEEE Computer Security Foundations Workshop (CSFW), pages 202–218. IEEE Computer Society, June 2003.
GZipped PostScript (184 kB)
PDF (230 kB)
Info
See www.fmi.uni-stuttgart.de ...
Tech report version
Claus Schröter, Stefan Schwoon, and Javier Esparza. The Model-Checking Kit. In Wil van der Aalst and Eike Best, editors, Applications and Theory of Petri Nets 2003, volume 2679 of Lecture Notes in Computer Science, pages 463–472. Springer, June 2003.
GZipped PostScript (60 kB)
Info
See www.fmi.uni-stuttgart.de ...
See also SSE02
Tero Harju and Dirk Nowotka. Periodicity and unbordered words. TUCS Tech. Rep. 523, Turku Centre of Computer Science, Finland, April 2003. Submitted.
GZipped PostScript (120 kB)
PDF (179 kB)
Info
Conference version
Tero Harju and Dirk Nowotka. Minimal Duval extensions. TUCS Tech. Rep. 520, Turku Centre of Computer Science, Finland, April 2003.
GZipped PostScript (80 kB)
PDF (116 kB)
Info
Journal version
Wilfried Brauer, Markus Holzer, Barbara König, and Stefan Schwoon. The theory of finite-state adventures. EATCS Bulletin, 79:230–237, February 2003.
GZipped PostScript (111 kB)
PDF (218 kB)
Info
Tero Harjuand Dirk Nowotka. About Duval's conjecture. TUCS Tech. Rep. 514, Turku Centre of Computer Science, Finland, February 2003.
GZipped PostScript (94 kB)
PDF (138 kB)
Info
Conference version
Thomas Reps, Stefan Schwoon, and Somesh Jha. Weighted pushdown systems and their application to interprocedural dataflow analysis. Technical Report TR-1470, Computer Sciences Department, University of Wisconsin, February 2003.
GZipped PostScript (261 kB)
Info
See www.fmi.uni-stuttgart.de ...
Conference version, Journal version
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.
GZipped PostScript (174 kB)
PDF (176 kB)
Info
Journal version
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.
GZipped PostScript (141 kB)
PDF (371 kB)
Info
Conference version
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.
GZipped PostScript (133 kB)
PDF (306 kB)
Info
A. Kučera and J. Esparza. A logical viewpoint on process-algebraic quotients. Journal of Logic and Computation, 13(6):863–880, 2003.
GZipped PostScript (98 kB)
PDF (263 kB)
Info
Conference version
Tobias Heindel. Cyclic -graph reduction, call-by-need, and their process semantics. Master's thesis, Eberhard Karls Universität Tübingen, 2003.
PDF (464 kB)
Info
Keijo Heljanko and Ilkka Niemelä. Bounded LTL model checking with stable models. Theory and Practice of Logic Programming (TPLP), 3(4&5):519–550, 2003. Also available as (CoRR: arXiv:cs.LO/0305040).
Info
See www.tcs.hut.fi ...
Paolo Baldan, Andrea Corradini, and Barbara König. Unfolding-based verification for graph transformation systems. In Proc. of UniGra '03: Uniform Approaches to Graphical Specification Techniques (Warsaw), 2003.
GZipped PostScript (72 kB)
PDF (110 kB)
Info
Paolo Baldan, Barbara König, and Bernhard König. A logic for analyzing abstractions of graph transformation systems. In Proc. of SAS '03 (International Static Analysis Symposium), pages 255–272. Springer-Verlag, 2003. LNCS 2694.
GZipped PostScript (157 kB)
PDF (264 kB)
Info
Markus Holzer and Barbara König. On deterministic finite automata and syntactic monoid size, continued. In Proc. of DLT '03 (Developments in Language Theory), pages 349–360. Springer-Verlag, 2003. LNCS 2710.
GZipped PostScript (131 kB)
PDF (150 kB)
Info
Journal version
Tero Harju and Dirk Nowotka. On the independence of equations in three variables. Theoret. Comput. Sci., 307(1):139–172, 2003.
GZipped PostScript (110 kB)
PDF (241 kB)
Info
Tech report version
Tero Harju and Dirk Nowotka. Periodicity and unbordered segments of words. Bull. EATCS, 80:162–167, 2003.
GZipped PostScript (41 kB)
PDF (103 kB)
Info
Tero Harju and Dirk Nowotka. About Duval's conjecture. In Z. Esik and Z. Fülöp, editors, DLT 2003 (Szeged), volume 2710 of Lecture Notes in Comput. Sci., pages 316–324, Berlin, 2003. Springer-Verlag.
GZipped PostScript (55 kB)
PDF (99 kB)
Info
Tech report version
Stefan Schwoon, Somesh Jha, Thomas Reps, and Stuart Stubblebine. On generalized authorization problems. Technical Report TR-1469, Computer Sciences Department, University of Wisconsin, January 2003.
GZipped PostScript (168 kB)
Info
See www.fmi.uni-stuttgart.de ...
Conference version

2002

Dejvuth Suwimonteerabuth and Prabhas Chongstitvatana. Online robot learning by reward and punishment for a mobile robot. In Proceedings of the 2002 IEEE/RSJ Intl. Conference on Intelliget Robots and Systems, pages 921–926, October 2002.
PDF (287 kB)
Info
J. Esparza and C. Lakos, editors. Applications and theory of petri nets 2002, volume 2360 of Lecture Notes in Computer Science. Springer Verlag, 2002.
Info
See link.springer.de ...
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.
GZipped PostScript (183 kB)
PDF (176 kB)
Info
J. Esparza, S. Römer, and W. Vogler. An improvement of McMillan's unfolding algorithm. Formal Methods in System Design, 20:285–310, 2002.
GZipped PostScript (149 kB)
PDF (351 kB)
Info
Conference version
Kozura V.E., Nepomniaschy V.A., and Novikov R.M. Verification of distributed systems modelled by high-level petri nets. In Proc. of PARELEC 2002, pages 61–66. IEEE Computer Society, 2002.
Info
Nepomniaschy V.A., Shilov N.V., Bodin E.V., and Kozura V.E. Basic-real: Integrated approach for design, specification and verification of distributed systems. In Proc. of IFM 2002, pages 69–88. Springer, 2002. LNCS 2335.
Info
Tero Harju and Dirk Nowotka. Density of critical factorizations. Theor. Inform. Appl., 36(3):315–327, 2002.
GZipped PostScript (68 kB)
PDF (131 kB)
Info
Tech report version
Tero Harju and Dirk Nowotka. Duval's conjecture and Lyndon words. TUCS Tech. Rep. 479, Turku Centre of Computer Science, Finland, 2002. Submitted.
GZipped PostScript (91 kB)
PDF (139 kB)
Info
Stefan Schwoon. Determinization and complementation of Streett automata. In Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors, Automata, Logics, and Infinite Games, volume 2500 of Lecture Notes in Computer Science, chapter 5, pages 79–91. Springer, 2002.
Info
See estragon.ti.informatik.uni-kiel.de ...
Stefan Schwoon. Model-checking pushdown systems. PhD thesis, Technische Universität München, 2002.
GZipped PostScript (662 kB)
PDF (948 kB)
Info
See www.fmi.uni-stuttgart.de ...
Claus Schröter, Stefan Schwoon, and Javier 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 (124 kB)
Info
See www.fmi.uni-stuttgart.de ...
See also SSE03
Alin Stefanescu. Automatic synthesis of distributed systems. In Proceedings of 17th IEEE International Conference on Automated Software Engineering, page 315. IEEE Computer Society, 2002. Position paper.
GZipped PostScript (56 kB)
Info
See www.fmi.uni-stuttgart.de ...
Slides 

2001

Tero Harju and Dirk Nowotka. Density of critical factorizations. TUCS Tech. Rep. 435, Turku Centre of Computer Science, Finland, December 2001.
GZipped PostScript (99 kB)
PDF (149 kB)
Info
Journal version
Tero Harju and Dirk Nowotka. On the independence of equations in three variables. TUCS Tech. Rep. 432, Turku Centre of Computer Science, Finland, November 2001.
GZipped PostScript (148 kB)
PDF (236 kB)
Info
Journal version
Javier Esparza, Antonín Kučera, and Stefan Schwoon. Model-checking LTL with regular valuations for pushdown systems. In Naoki Kobayashi and Benjamin C. Pierce, editors, Proceedings of TACS 2001, volume 2215 of Lecture Notes in Computer Science, pages 306–339. Springer, October 2001.
GZipped PostScript (154 kB)
Info
Tech report version, Journal version
Javier Esparza, Antonín Kučera, and Stefan Schwoon. Model-checking LTL with regular valuations for pushdown systems. Informatics Research Report EDI-INF-RR-0044, University of Edinburgh, School of Informatics, August 2001.
PDF (224 kB)
Info
Conference version, Journal version
Javier Esparza and Stefan Schwoon. A BDD-based model checker for recursive programs. In Gérard Berry, Hubert Comon, and Alain Finkel, editors, Proceedings of CAV 2001, volume 2102 of Lecture Notes in Computer Science, pages 324–336. Springer, July 2001.
GZipped PostScript (61 kB)
Info
See www.fmi.uni-stuttgart.de ...
Markus Holzer and Stefan Schwoon. Assembling molecules in Atomix is hard. Technical Report TUM-I0101, Technische Universität München, May 2001.
GZipped PostScript (75 kB)
Info
Journal version
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.
GZipped PostScript (271 kB)
PDF (281 kB)
Info
Conference version
J. Esparza and C. Schröter. Unfolding based algorithms for the reachability problem. Fundamenta Informaticae, 47(3–4):231–245, 2001.
GZipped PostScript (150 kB)
PDF (177 kB)
Info
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.
GZipped PostScript (177 kB)
PDF (164 kB)
Info
Kozura V.E. Unfoldings of coloured petri nets. In Proc. of Ershov Memorial Conference 2001, pages 268–278. Springer, 2001. LNCS 2244.
Info
Kozura V.E. Unfoldings of timed coloured petri nets. In Proc. of the CS&P'2001 Workshop, Warsaw 3-5 Oktober 2001, pages 128–139, 2001.
Info

2000

Javier Esparza, Peter Rossmanith, and Stefan Schwoon. A uniform framework for problems on context-free grammars. EATCS Bulletin, 72:169–177, October 2000.
GZipped PostScript (46 kB)
Info
Javier Esparza, David Hansel, Peter Rossmanith, and Stefan Schwoon. Efficient algorithms for model checking pushdown systems. In E. Allen Emerson and A. Prasad Sistla, editors, Proceedings of CAV 2000, volume 1855 of Lecture Notes in Computer Science, pages 232–247. Springer, July 2000.
GZipped PostScript (105 kB)
Info
Tech report version
Javier Esparza, David Hansel, Peter Rossmanith, and Stefan 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 (166 kB)
Info
Conference version
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 (84 kB)
PDF (212 kB)
Info
An even more efficient approach can be found in ERS00
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 (133 kB)
PDF (331 kB)
Info
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.
GZipped PostScript (99 kB)
PDF (238 kB)
Info
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 (114 kB)
PDF (302 kB)
Info
Journal version
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 (72 kB)
PDF (224 kB)
Info
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 (127 kB)
PDF (381 kB)
Info
Marco Benini, Dirk Nowotka, and Carl Pulley. Computer arithmetic: Logic, calculation, and rewriting. In D. Gabbay and M. de Rijke, editors, FroCoS 1998 (Amsterdam), volume 7 of Studies in Logic and Computation, pages 77–93, Baldock, 2000. Research Studies Press Ltd.
GZipped PostScript (74 kB)
PDF (138 kB)
Info
Alin Stefanescu. Flownomial calculus: From theory to practice. Master's thesis, University of Bucharest, 2000. In Romanian.
GZipped PostScript (264 kB)
Info
See www.fmi.uni-stuttgart.de ...

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.
GZipped PostScript (98 kB)
PDF (271 kB)
Info
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 (90 kB)
PDF (201 kB)
Info
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 (103 kB)
PDF (278 kB)
Info
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.
Info
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.
GZipped PostScript (194 kB)
PDF (179 kB)
Info
P. Jančar, J. Esparza, and F. Moller. Petri nets and regular behaviours. Journal of Computer and System Sciences, 59(3):476–503, 1999.
GZipped PostScript (82 kB)
PDF (285 kB)
Info
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.
GZipped PostScript (63 kB)
PDF (155 kB)
Info
Journal version
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 (194 kB)
PDF (179 kB)
Info
Bodin E.V., Kozura V.E., and Shilov N.V. Experiments with model checking for mu-calculus in specification and verification project real. In Proc. of Fifth New Zealand Formal Program Development Colloquium, 22 January 1999, pages 1–18, 1999.
Info

1998

C. Schröter, T. Engel, and C. Meinel. Internetbasiertes Arztbriefsystem. Technical Report Preprint 98-07, Institut für Telematik, Trier, Juli 1998.
Info
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 (159 kB)
PDF (361 kB)
Info
J. Esparza. Reachability in live and safe free-choice Petri nets is -complete. Theoretical Computer Science, 198(1–2):211–224, 1998.
GZipped PostScript (66 kB)
PDF (222 kB)
Info
Marco Benini, Sara Kalvala, and Dirk Nowotka. Program abstraction in a higher-order logic framework. In J. Grundy and M. Newey, editors, TPHOLs 1998 (Canberra), volume 1479 of Lecture Notes in Comput. Sci., pages 33–48, Berlin, 1998. Springer-Verlag.
GZipped PostScript (79 kB)
PDF (164 kB)
Info
S. Hludov, C. Schröter, and C. Meinel. Adaptive Compression of Image Data. In S. Fischer, R. Steinmetz, H. J. Stuettgen, H. R. van As, and R. Vercelli, editors, Broadband European Networks and Multimedia Services (SYBEN'98), volume 3408 of SPIE Proceedings, pages 520–527, Zürich, 1998.
GZipped PostScript (432 kB)
Info
Stefan Schwoon. Übersetzung von SDL-Spezifikationen in Petri-Netze. Master's thesis, Universität Hildesheim, 1998. In German.
GZipped PostScript (547 kB)
Info
See theoretica.informatik.uni-oldenburg.de ...
S. Hludov, C. Schröter, and C. Meinel. Adaptive Komprimierung von DICOM-Bildern. Technical Report Preprint 98-03, Institut für Telematik, Trier, März 1998.
Info

1997

O. Burkart and J. Esparza. More infinite results. Bulletin of the EATCS 62 (Concurrency Column), 1997.
Info
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 (31 kB)
PDF (141 kB)
Info
A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In Proc. of CONCUR'97, 1997.
GZipped PostScript (154 kB)
PDF (430 kB)
Info
J. Esparza and S. Melzer. Model checking LTL using constraint programming. In Proc. of Application and Theory of Petri Nets'97, 1997.
GZipped PostScript (69 kB)
PDF (254 kB)
Info
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 (49 kB)
PDF (174 kB)
Info
J. Esparza. Petri nets, commutative context-free grammars, and basic parallel processes. Fundamenta Informaticae, 31:13–26, 1997.
GZipped PostScript (69 kB)
PDF (226 kB)
Info
Conference version
J. Esparza. Decidability of model-checking for infinite-state concurrent systems. Acta Informatica, 34:85–107, 1997.
GZipped PostScript (83 kB)
PDF (282 kB)
Info

1996

O. Burkart and J. Esparza. More infinite results. Electronic Notes in Theoretical Computer Science, 6, 1996.
GZipped PostScript (70 kB)
PDF (296 kB)
Info
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 (77 kB)
PDF (197 kB)
Info
J. Esparza and G. Bruns. Trapping mutual exclusion in the box calculus. Theoretical Computer Science, 153(1):95–128, 1996.
Info
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 (86 kB)
PDF (288 kB)
Info
Journal version
J. Esparza. More infinite results. In Proc. of INFINITY'96, Research Report MIP-9614, University of Passau, 1996.
GZipped PostScript (58 kB)
PDF (236 kB)
Info
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.
GZipped PostScript (356 kB)
PDF (826 kB)
Info
Tech report version
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 (55 kB)
PDF (205 kB)
Info
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 (84 kB)
PDF (331 kB)
Info
Journal version
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 (24 kB)
PDF (122 kB)
Info

1995

A. Cheng, J. Esparza, and J. Palsberg. Complexity results for 1-safe nets. Theoretical Computer Science, 147:117–136, 1995.
PDF (182 kB)
Info
J. Desel and J. Esparza. Shortest paths in reachability graphs. Journal of Computer and System Sciences, 51(2):314–323, 1995.
PDF (1 MB)
Info
J. Desel and J. Esparza. Free choice Petri nets, volume 40 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1995.
Info
See titles.cambridge.org ...
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 (69 kB)
PDF (232 kB)
Info
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.
GZipped PostScript (69 kB)
PDF (226 kB)
Info
Journal version
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 (356 kB)
PDF (826 kB)
Info
Conference version, Journal version
Allan Cheng, Javier Esparza, and Jens Palsberg. Complexity results for 1-safe nets. Theoretical Computer Science, 147(1&2):117–136, 1995.
PDF (182 kB)
Info

1994

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 (59 kB)
PDF (243 kB)
Info
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.
PDF (1 MB)
Info
J. Esparza. Reduction and synthesis of live and bounded free choice Petri nets. Information and Computation, 114(1):50–87, 1994.
PDF (3 MB)
Info
J. Esparza. Model checking using net unfoldings. Science of Computer Programming, 23:151–195, 1994.
Info
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.
Info

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.
Info
J. Desel and J. Esparza. Reachability in cyclic extended free-choice systems. Theoretical Computer Science, 114:93–118, 1993.
PDF (2 MB)
Info
Conference version
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 (43 kB)
PDF (179 kB)
Info

1992

E. Best, J. Desel, and J. Esparza. Traps characterise home states in free choice systems. Theoretical Computer Science, 101:161–176, 1992.
PDF (1 MB)
Info
Conference version
J. Esparza and M. Silva. A polynomial time algorithm to decide liveness of bounded free choice nets. Theoretical Computer Science, 102:185–205, 1992.
PDF (1 MB)
Info
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.
PDF (947 kB)
Info

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.
Info
Journal version
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.
PDF (1 MB)
Info
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.
Info
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.
PDF (1 MB)
Info
Journal version
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.
PDF (2 MB)
Info
Journal version
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.
PDF (1 MB)
Info

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.
PDF (4 MB)
Info
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.
PDF (4 MB)
Info
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.
PDF (1 MB)
Info