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. |
|
Volker Diekert, Tero Harju, and Dirk Nowotka. Weinbaum factorizations of primitive words. Izvestiya VUZ Matematika, 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. |
|
Tero Harju and Dirk Nowotka. Periodicity and unbordered words: A proof of the extended duval conjecture. J. Assoc. Comput. Mach., 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 |
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. |
|
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. |
|
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. |
|
Javier Esparza, Pradeep Kanade, and Stefan Schwoon. A negative result on depth-first unfoldings. Software Tools for Technology Transfer, 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 (STACS), volume 4393 of Lecture Notes in Computer Science, pages 296–307, Aachen, Germany, 2007. |
|
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. |
|
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. |
|
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. |
|
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. |
|
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. |
|
J. Esparza, P. Jančar, and A. Miller. On the complexity of consistency and complete state coding. Technical report, University of Stuttgart, July 2006. |
|
Volker Diekert, Tero Harju, and Dirk Nowotka. Weinbaum factorizations of primitive words. TUCS Tech. Rep. 780, Turku Centre of Computer Science, Finland, July 2006. |
|
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. |
|
Tero Harju and Dirk Nowotka. Binary words with few squares. Bull. EATCS, 89:164–166, June 2006. |
|
Alin Stefanescu. Automatic synthesis of distributed transition systems. PhD thesis, Universität Stuttgart, February 2006. |
|
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. |
|
G. Delzanno, J. Esparza, and J. Srba. Monotonic set-extended prefix rewriting and verification of recursive ping-pong protocols. Technical report, BRICS, 2006. |
|
Javier Esparza, Antonín Kučera, and Richard Mayr. Model checking probabilistic pushdown automata. Logical Methods in Computer Science, 2006. |
|
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. |
|
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. |
|
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. |
|
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. |
|
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. |
|
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. |
|
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. |
|
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. |
|
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. |
|
Tero Harju and Dirk Nowotka. On unique factorizations of primitive words. Theoret. Comput. Sci., 356(1–2):186–189, 2006. |
|
Tero Harju and Dirk Nowotka. Periods in word extensions. TUCS Tech. Rep. 736, Turku Centre of Computer Science, Finland, January 2006. |
|
Tero Harju and Dirk Nowotka. Periods in word extensions. Acta Inform., 43(2):165–171, 2006. |
|
Tero Harju and Dirk Nowotka. Binary words with few squares. TUCS Tech. Rep. 737, Turku Centre of Computer Science, Finland, January 2006. |
|
Claus Schröter. Halbordnungs- und Reduktionstechniken für die automatische Verifikation von verteilten Systemen. PhD thesis, Universität Stuttgart, 2006. |
|
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. |
|
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. |
|
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. |
|
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. |
|
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. |
|
Tero Harju and Dirk Nowotka. On unique factorizations of primitive words. TUCS Tech. Rep. 714, Turku Centre of Computer Science, Finland, October 2005. |
|
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. |
|
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. |
|
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. |
|
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. |
|
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. |
|
Ahmed Bouajjani, Javier Esparza, and Tayssir Touili. Reachability analysis of synchronized PA-systems. Electronic Notes in Theoretical Computer Science, 138(3):153–178, 2005. |
|
Stefan Kiefer. Abstraction refinement for pushdown systems. Master's thesis, Universität Stuttgart, 2005. |
|
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. |
|
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. |
|
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. |
|
Barbara König. A general framework for types in graph rewriting. Acta Informatica, 42(4-5):349–388, 2005. |
|
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. |
|
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). |
|
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. |
|
Tero Harju, Arto Lepistö, and Dirk Nowotka. A characterization of periodicity of bi-infinite words. Theoret. Comput. Sci., 347(1–2):419–422, 2005. |
|
Tero Harju and Dirk Nowotka. On the equation in a free semigroup. Theoret. Comput. Sci., 330(1):117–121, 2005. |
|
Tero Harju and Dirk Nowotka. Counting bordered and primitive words with a fixed weight. Theoret. Comput. Sci., 340(2):273–279, 2005. |
|
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. |
|
2004 |
Barbara König. Analysis and verification of systems with dynamically evolving structures. Habilitation thesis, Universität Stuttgart, December 2004. |
|
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. |
|
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. |
|
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. |
|
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. |
|
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. |
|
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. |
|
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. |
|
Tero Harju and Dirk Nowotka. On the equation in a free semigroup. TUCS Tech. Rep. 602, Turku Centre of Computer Science, Finland, April 2004. |
|
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. |
|
Markus Holzer and Stefan Schwoon. Assembling molecules in Atomix is hard. Theoretical Computer Science, 303(3):447–462, February 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. |
|
Javier Esparza, Antonín Kučera, and Richard Mayr. Model checking probabilistic pushdown automata. Technical report, Faculty of Informatics, Masaryk University, Brno, 2004. |
|
J. Esparza. A polynomial-time algorithm for checking consistency of free-choice signal transition graphs. Fundamenta Informaticae, 62(2):197–220, 2004. |
|
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. |
|
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. |
|
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. |
|
Markus Holzer and Barbara König. On deterministic finite automata and syntactic monoid size. Theoretical Computer Science, 327:319–347, 2004. |
|
Hartmut Ehrig and Barbara König. Deriving bisimulation congruences in the DPO approach to graph rewriting. Technical Report 01/2004, Universität Stuttgart, 2004. |
|
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. |
|
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. |
|
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. |
|
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. |
|
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. |
|
Matthias Hopf, Michael Luttenberger, and Thomas Ertl. Hierarchical splatting of scattered 4d data. IEEE Computer Graphics and Applications, 24(04):64–72, 2004. |
|
Michael Luttenberger. Effiziente Berechnung optimaler Strategien für Paritätsspiele. Master's thesis, Universität Stuttgart, 2004. In German. |
|
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. |
|
Tero Harju and Dirk Nowotka. The equation in a free semigroup. Semigroup Forum, 68(3):488–490, 2004. |
|
Tero Harju and Dirk Nowotka. Minimal Duval extensions. Internat. J.,Found. Comput. Sci., 15(2):349–354, 2004. |
|
Tero Harju and Dirk Nowotka. Border correlation of binary words. J. Combin. Theory, Ser A, 108(2):331–341, 2004. |
|
Dirk Nowotka. Periodicity and unbordered factors of words. PhD thesis, University of Turku, 2004. |
|
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. |
|
Keijo Heljanko and Alin Stefanescu. Complexity results for checking distributed implementability. Technical Report 05/2004, Universität Stuttgart, 2004. |
|
Dejvuth Suwimonteerabuth. Verifying Java bytecode with the Moped model checker. Master's thesis, Universität Stuttgart, 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. |
|
Tero Harju and Dirk Nowotka. The equation in a free semigroup. TUCS Tech. Rep. 561, Turku Centre of Computer Science, Finland, October 2003. |
|
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. |
|
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. |
|
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. |
|
Tero Harju and Dirk Nowotka. Border correlation of binary words. TUCS Tech. Rep. 546, Turku Centre of Computer Science, Finland, August 2003. |
|
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. |
|
Stefan Kiefer. Die Menge der virtuellen Verbindungen im Spiel Hex ist PSPACE-vollständig. Studienarbeit Nr. 1887, Universität Stuttgart, Juli 2003. In German. |
|
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. |
|
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. |
|
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. |
|
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. |
|
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. |
|
Tero Harju and Dirk Nowotka. Periodicity and unbordered words. TUCS Tech. Rep. 523, Turku Centre of Computer Science, Finland, April 2003. Submitted. |
|
Tero Harju and Dirk Nowotka. Minimal Duval extensions. TUCS Tech. Rep. 520, Turku Centre of Computer Science, Finland, April 2003. |
|
Wilfried Brauer, Markus Holzer, Barbara König, and Stefan Schwoon. The theory of finite-state adventures. EATCS Bulletin, 79:230–237, February 2003. |
|
Tero Harjuand Dirk Nowotka. About Duval's conjecture. TUCS Tech. Rep. 514, Turku Centre of Computer Science, Finland, February 2003. |
|
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. |
|
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. |
|
Tobias Heindel. Cyclic -graph reduction, call-by-need, and their process semantics. Master's thesis, Eberhard Karls Universität Tübingen, 2003. |
|
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). |
|
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. |
|
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. |
|
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. |
|
Tero Harju and Dirk Nowotka. On the independence of equations in three variables. Theoret. Comput. Sci., 307(1):139–172, 2003. |
|
Tero Harju and Dirk Nowotka. Periodicity and unbordered segments of words. Bull. EATCS, 80:162–167, 2003. |
|
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. |
|
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. |
|
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. |
|
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. |
|
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. |
|
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. |
|
Tero Harju and Dirk Nowotka. Density of critical factorizations. Theor. Inform. Appl., 36(3):315–327, 2002. |
|
Tero Harju and Dirk Nowotka. Duval's conjecture and Lyndon words. TUCS Tech. Rep. 479, Turku Centre of Computer Science, Finland, 2002. Submitted. |
|
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. |
|
Stefan Schwoon. Model-checking pushdown systems. PhD thesis, Technische Universität München, 2002. |
|
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. |
|
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. |
|
2001 |
Tero Harju and Dirk Nowotka. Density of critical factorizations. TUCS Tech. Rep. 435, Turku Centre of Computer Science, Finland, December 2001. |
|
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. |
|
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. |
|
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. |
|
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. |
|
Markus Holzer and Stefan Schwoon. Assembling molecules in Atomix is hard. Technical Report TUM-I0101, Technische Universität München, May 2001. |
|
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. |
|
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. |
|
Kozura V.E. Unfoldings of coloured petri nets. In Proc. of Ershov Memorial Conference 2001, pages 268–278. Springer, 2001. LNCS 2244. |
|
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. |
|
2000 |
Javier Esparza, Peter Rossmanith, and Stefan Schwoon. A uniform framework for problems on context-free grammars. EATCS Bulletin, 72:169–177, October 2000. |
|
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. |
|
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. |
|
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 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. |
|
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. |
|
Alin Stefanescu. Flownomial calculus: From theory to practice. Master's thesis, University of Bucharest, 2000. In Romanian. |
|
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. |
|
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. |
|
1998 |
C. Schröter, T. Engel, and C. Meinel. Internetbasiertes Arztbriefsystem. Technical Report Preprint 98-07, Institut für Telematik, Trier, Juli 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. |
|
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. |
|
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. |
|
Stefan Schwoon. Übersetzung von SDL-Spezifikationen in Petri-Netze. Master's thesis, Universität Hildesheim, 1998. In German. |
|
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. |
|
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. |
|
P. Jancar and J. Esparza. Deciding finiteness of Petri nets up to bisimulation. SFB-Bericht Nr. 342/23/95A, TU München, 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. |
|