I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
All Publications

To appear

Loig Jezequel and Javier Esparza. Message passing algorithms for the verification of distributed protocols. In Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2014, San Diego, USA, January 2014, To appear.
Info
Markus Gulden and Stefan Kugele. A Concept for Generating Simplified RESTful Interfaces. In Proceedings of the Fourth International Workshop on RESTful Design, WS-REST 2013 at WWW2013, Rio de Janeiro, Brazil, May 14, 2013. ACM, to appear.
Info
Georg Bachmeier, Michael Luttenberger, and Maximilian Schlund. Finite Automata for the Sub- and Superword Closure of CFLs: Descriptional and Computational Complexity. In LATA, Lecture Notes in Computer Science, pages ??–??, March To appear.
PDF (382 kB)
Info
M. Luttenberger and M. Schlund. Convergence of Newton's Method over Commutative Semirings. Information and Computation, ?(?):??–??, To appear.
PDF (449 kB)
Info

2018

Stefan Kiefer. On computing the total variation distance of hidden Markov models. In Proceedings of the 45th International Colloquium on Automata, Languages, and Programming (ICALP), Leibniz International Proceedings in Informatics (LIPIcs), pages 130:1–130:13, 2018.
Info
See dx.doi.org ...
Slides 
Tech report version
Stefan Kiefer. On computing the total variation distance of hidden Markov models. Technical report, arXiv.org, 2018. Available at https://arxiv.org/abs/1804.06170.
Info
See arxiv.org ...
Conference version
Radu Grigore and Stefan Kiefer. Selective monitoring. In Proceedings of the 29th International Conference on Concurrency Theory (CONCUR), Leibniz International Proceedings in Informatics (LIPIcs), pages 20:1–20:16, 2018.
Info
See dx.doi.org ...
Slides 
Tech report version
Radu Grigore and Stefan Kiefer. Selective monitoring. Technical report, arXiv.org, 2018. Available at https://arxiv.org/abs/1806.06143.
Info
See arxiv.org ...
Conference version

2017

Dmitry Chistikov, Stefan Kiefer, Ines Marusic, Mahsa Shirmohammadi, and James Worrell. On rationality of nonnegative matrix factorization. In Proceedings of the 28th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pages 1290–1305. SIAM, 2017.
PDF (465 kB)
Info
See dx.doi.org ...
Christoph Haase, Stefan Kiefer, and Markus Lohrey. Computing quantiles in Markov chains with multi-dimensional costs. In Proceedings of the 32nd Annual Symposium on Logic in Computer Science (LICS). IEEE, 2017.
PDF (516 kB)
Info
Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Dominik Wojtczak. On strong determinacy of countable stochastic games. In Proceedings of the 32nd Annual Symposium on Logic in Computer Science (LICS). IEEE, 2017.
PDF (363 kB)
Info
Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Dominik Wojtczak. Parity objectives in countable MDPs. In Proceedings of the 32nd Annual Symposium on Logic in Computer Science (LICS). IEEE, 2017.
PDF (356 kB)
Info
Slides 
Dmitry Chistikov, Stefan Kiefer, Ines Marusic, Mahsa Shirmohammadi, and James Worrell. Nonnegative matrix factorization requires irrationality. SIAM Journal on Applied Algebra and Geometry (SIAGA), 1(1):285–307, 2017.
PDF (439 kB)
Info
See doi.org ...
Stefan Kiefer, Ines Marusic, and James Worrell. Minimisation of multiplicity tree automata. Logical Methods in Computer Science (LMCS), 13(1), 2017.
Info
See doi.org ...
Conference version
Christoph Haase, Stefan Kiefer, and Markus Lohrey. Counting problems for Parikh images. In Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017), pages 12:1–12:13, 2017.
PDF (522 kB)
Info
Slides 

2016

Javier Esparza, Pierre Ganty, Jerome Leroux, and Rupak Majumdar. Model checking population protocols. Technical report, Technical University of Munich, 2016. Submitted for publication.
PDF (502 kB)
Info
See arxiv.org ...
Eike Best and Javier Esparza. Existence of home states in petri nets is decidable. Inf. Process. Lett., 116(6):423–427, 2016.
PDF (289 kB)
Info
Javier Esparza and Philipp Hoffmann. Reduction rules for colored workflow nets. In FASE, pages 342–358. Springer, 2016.
PDF (358 kB)
Info
Jérôme Leroux Javier Esparza, Pierre Ganty and Rupak Majumdar. Verification of population protocols. Acta Informatica, 2016. To appear.
PDF (219 kB)
Info
Javier Esparza, Michael Luttenberger, and Maximilian Schlund. A brief history of Strahler numbers — with a preface. Technical report, Technical University of Munich, 2016.
PDF (424 kB)
Info
Conference version
Christoph Haase and Stefan Kiefer. The complexity of the th largest subset problem and related problems. Information Processing Letters (IPL), 116(2):111–115, 2016.
PDF (254 kB)
Info
See dx.doi.org ...
Nathanaël Fijalkow, Stefan Kiefer, and Mahsa Shirmohammadi. Trace refinement in labelled Markov decision processes. In Bart Jacobs and Christof Löding, editors, Proceedings of the 19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), volume 9634 of LNCS, pages 303–318, Eindhoven, The Netherlands, 2016. Springer.
PDF (534 kB)
Info
Tech report version
Nathanaël Fijalkow, Stefan Kiefer, and Mahsa Shirmohammadi. Minimisation of multiplicity tree automata. Technical report, arXiv.org, 2016. Available at http://arxiv.org/abs/1510.09102.
Info
See arxiv.org ...
Conference version
Stefan Kiefer and A. Prasad Sistla. Distinguishing hidden Markov chains. In Proceedings of the 31st Annual Symposium on Logic in Computer Science (LICS), pages 66–75, New York, USA, 2016. ACM.
PDF (376 kB)
Info
Slides 
Tech report version
Stefan Kiefer and A. Prasad Sistla. Distinguishing hidden Markov chains. Technical report, arXiv.org, 2016. Available at https://arxiv.org/abs/1507.02314.
Info
See arxiv.org ...
Conference version
Dmitry Chistikov, Stefan Kiefer, Ines Marusic, Mahsa Shirmohammadi, and James Worrell. On restricted nonnegative matrix factorization. In Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016), volume 55 of Leibniz International Proceedings in Informatics (LIPIcs), pages 103:1–103:14, 2016.
PDF (605 kB)
Info
See drops.dagstuhl.de ...
Tech report version
Dmitry Chistikov, Stefan Kiefer, Ines Marusic, Mahsa Shirmohammadi, and James Worrell. On restricted nonnegative matrix factorization. Technical report, arXiv.org, 2016. Available at https://arxiv.org/abs/1605.07061.
Info
See arxiv.org ...
Conference version
Maria Bruna, Radu Grigore, Stefan Kiefer, Joël Ouaknine, and James Worrell. Proving the Herman-protocol conjecture. In Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016), volume 55 of Leibniz International Proceedings in Informatics (LIPIcs), pages 104:1–104:12, 2016.
PDF (503 kB)
Info
See drops.dagstuhl.de ...
Tech report version
Maria Bruna, Radu Grigore, Stefan Kiefer, Joël Ouaknine, and James Worrell. Proving the Herman-protocol conjecture. Technical report, arXiv.org, 2016. Available at https://arxiv.org/abs/1504.01130.
Info
See arxiv.org ...
Conference version
Christel Baier, Stefan Kiefer, Joachim Klein, Sascha Klüppelholz, David Müller, and James Worrell. Markov chains and unambiguous Büchi automata. In Proceedings of the 28th International Conference on Computer Aided Verification (CAV), volume 9779 of LNCS, pages 23–42, 2016.
PDF (428 kB)
Info
See dx.doi.org ...
Tech report version
Christel Baier, Stefan Kiefer, Joachim Klein, Sascha Klüppelholz, David Müller, and James Worrell. Markov chains and unambiguous Büchi automata. Technical report, arXiv.org, 2016. Available at https://arxiv.org/abs/1605.00950.
Info
See arxiv.org ...
Conference version

2015

Salomon Sickert. Converting linear temporal logic to deterministic (generalized) rabin automata. Archive of Formal Proofs, September 2015.
Info
See afp.sf.net ...
This publication contains the formalization of LTL_to_DRA.
Tomás Brázdil, Stefan Kiefer, Antonín Kučera, and Ivana Hutarová Vareková. Runtime analysis of probabilistic programs with unbounded recursion. Journal of Computer and System Sciences, 81(1):288–310, February 2015.
PDF (587 kB)
Info
See dx.doi.org ...
Conference version
Javier Esparza, Michael Luttenberger, and Maximilian Schlund. FPSOLVE: A generic solver for fixpoint equations over semirings. Int. J. Found. Comput. Sci., 26(7):805–826, 2015.
PDF (438 kB)
Info
Jérôme Leroux Javier Esparza, Pierre Ganty and Rupak Majumdar. Verification of population protocols. In CONCUR, 2015.
PDF (462 kB)
Info
Journal version
Pierre Ganty Antoine Durand-Gasselin, Javier Esparza and Rupak Majumdar. Model checking parameterized asynchronous shared-memory systems.. In CAV, pages 192–208, 2015.
Info
Tech report version
Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, and Rupak Majumdar. Model checking parameterized asynchronous shared-memory systems. Technical report, CoRR, 2015.
PDF (333 kB)
Info
See arxiv.org ...
Javier Esparza and Jörg Desel. Negotiation programs. In PETRI NETS 2015, pages 157–178, 2015.
PDF (448 kB)
Info
Javier Esparza, Jan Kretinsky, and Salomon Sickert. From ltl to deterministic automata–a safraless compositional approach. Submitted, 2015.
PDF (690 kB)
Info
Tech report version, Conference version
This publication is a major revision of EsparzaK_CAV14, contains several corrections and new material.
Stefan Kiefer, Ines Marusic, and James Worrell. Minimisation of multiplicity tree automata. In Andrew Pitts, editor, Proceedings of the 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), volume 9034 of LNCS, pages 297–311, London, UK, 2015. Springer.
PDF (289 kB)
Info
Tech report version, Journal version
Stefan Kiefer, Ines Marusic, and James Worrell. Minimisation of multiplicity tree automata. Technical report, arXiv.org, 2015. Available at http://arxiv.org/abs/1410.5352.
Info
See arxiv.org ...
Conference version, Journal version
Tomáš Brázdil, Stefan Kiefer, Antonín Kučera, and Petr Novotný. Long-run average behaviour of probabilistic vector addition systems. In Proceedings of the 30th Annual Symposium on Logic in Computer Science (LICS), pages 44–55, Kyoto, Japan, 2015. IEEE.
PDF (321 kB)
Info
Tech report version
Tomáš Brázdil, Stefan Kiefer, Antonín Kučera, and Petr Novotný. Long-run average behaviour of probabilistic vector addition systems. Technical report, arXiv.org, 2015. Available at http://arxiv.org/abs/1505.02655.
Info
See arxiv.org ...
Conference version
Christoph Haase and Stefan Kiefer. The odds of staying on budget. In Proceedings of the 42nd International Colloquium on Automata, Languages and Programming (ICALP), part II, volume 9135 of LNCS, pages 234–246, Kyoto, Japan, 2015. Springer.
PDF (245 kB)
Info
Tech report version
Christoph Haase and Stefan Kiefer. The odds of staying on budget. Technical report, arXiv.org, 2015. Available at http://arxiv.org/abs/1409.8228.
Info
See arxiv.org ...
Conference version
Radu Grigore and Stefan Kiefer. Tree buffers. In Proceedings of the 27th International Conference on Computer Aided Verification (CAV), part I, volume 9206 of LNCS, pages 290–306, San Francisco, California, USA, 2015. Springer.
PDF (2 MB)
Info
Tech report version
Radu Grigore and Stefan Kiefer. Tree buffers. Technical report, arXiv.org, 2015. Available at http://arxiv.org/abs/1504.04757.
Info
See arxiv.org ...
Conference version
Georg Bachmeier, Michael Luttenberger, and Maximilian Schlund. Finite automata for the sub- and superword closure of cfls: Descriptional and computational complexity. In to appaear in: Language and Automata Theory and Applications - 9th International Conference, LATA 2015, 2015.
Info
Javier Esparza and Philipp J. Meyer. An SMT-based approach to coverability analysis. In FMCAD, pages 49–56, 2015.
Info
Peter Lammich and Rene Neumann. A framework for verifying depth-first search algorithms. In CPP, January 2015.
Info

2014

Tomáš Brázdil, Stefan Kiefer, and Antonín Kučera. Efficient analysis of probabilistic programs with an unbounded counter. Journal of the ACM, 61(6):41:1–41:35, December 2014.
PDF (558 kB)
Info
See dx.doi.org ...
Conference version
Vojtěch Forejt, Petr Jančar, Stefan Kiefer, and James Worrell. Language equivalence of probabilistic pushdown automata. Information and Computation, 237:1–11, October 2014.
PDF (274 kB)
Info
Rene Neumann. Using Promela in a fully verified executable LTL model checker. In Dimitra Giannakopoulou and Daniel Kroening, editors, Verified Software: Theories, Tools and Experiments, Lecture Notes in Computer Science, pages 105–114, July 2014.
Info
M. Schlund and M. Luttenberger. Regular Expressions for Provenance. In Proceedings of the 6th USENIX Workshop on the Theory and Practice of Provenance, June 2014.
PDF (225 kB)
Info
Stefan Kiefer and Björn Wachter. Stability and complexity of minimising probabilistic automata. Technical report, arXiv.org, May 2014. Available at http://arxiv.org/abs/1404.6673.
Info
See arxiv.org ...
Conference version
Javier Esparza, Peter Lammich, Rene Neumann, Tobias Nipkow, Alexander Schimpf, and Jan-Georg Smaus. A fully verified executable LTL model checker. Archive of Formal Proofs, May 2014. Formal proof development.
Info
See afp.sf.net ...
Rene Neumann. Promela formalization. Archive of Formal Proofs, May 2014. Formal proof development.
Info
See afp.sf.net ...
M. Schlund, M. Luttenberger, and J. Esparza. Fast and Accurate Unlexicalized Parsing via Structural Annotations. In Proceedings of the 14th Conference of the European Chapter of the Association for Computational Linguistics, volume 2: Short Papers, pages 164–168, Gothenburg, Sweden, April 2014. Association for Computational Linguistics.
PDF (182 kB)
Info
See www.aclweb.org ...
Javier Esparza, Michael Luttenberger, and Maximilian Schlund. A brief history of Strahler numbers. In LATA, pages 1–13, 2014.
PDF (402 kB)
Info
Tech report version
Javier Esparza and Philipp Hoffmann. Negotiation games. CoRR, abs/1405.6820, 2014.
PDF (395 kB)
Info
Javier Esparza, Michael Luttenberger, and Maximilian Schlund. FPsolve: A generic solver for fixpoint equations over semirings. In CIAA, pages 1–15, 2014.
PDF (359 kB)
Info
Javier Esparza. Keeping a crowd safe: On the complexity of parameterized verification. In STACS, pages 1–10, 2014. The paper published in the proceedings of STACS contained a mistake. This is the corrected version, which can also be found in arXiv.
PDF (259 kB)
Info
Javier Esparza and Jan Kretínský. From LTL to deterministic automata: A safraless compositional approach. Technical report, arxiv.org, 2014.
PDF (418 kB)
Info
Conference version, Journal version
Javier Esparza and Jan Kretínský. From LTL to deterministic automata: A safraless compositional approach. In CAV, pages 192–208, 2014.
Info
Tech report version, Journal version
Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp Meyer, and Filip Niksic. An SMT-based approach to coverability analysis. In CAV, pages 603–619, 2014.
PDF (538 kB)
Info
Loïg Jezequel and Javier Esparza. Message-passing algorithms for the verification of distributed protocols. In VMCAI, pages 222–241, 2014.
PDF (396 kB)
Info
Javier Esparza and Jörg Desel. On negotiation as concurrency primitive ii: Deterministic cyclic negotiations. In FOSSACS, pages 258–273, 2014.
Info
Tech report version
Javier Esparza and Jörg Desel. On negotiation as concurrency primitive ii: Deterministic cyclic negotiations. Technical report, arXiv.org, 2014.
PDF (391 kB)
Info
Conference version
Rémi Bonnet, Stefan Kiefer, and Anthony W. Lin. Analysis of probabilistic basic parallel processes. In Anca Muscholl, editor, Proceedings of the 17th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), volume 8412 of LNCS, pages 43–57, Grenoble, France, 2014. Springer.
PDF (327 kB)
Info
Slides 
Tech report version
Rémi Bonnet, Stefan Kiefer, and Anthony W. Lin. Analysis of probabilistic basic parallel processes. Technical report, arXiv.org, January 2014. Available at http://arxiv.org/abs/1401.4130.
Info
See arxiv.org ...
Conference version
Stefan Kiefer and Björn Wachter. Stability and complexity of minimising probabilistic automata. In J. Esparza et al., editor, Proceedings of the 41st International Colloquium on Automata, Languages and Programming (ICALP), part II, volume 8573 of LNCS, pages 268–279, Copenhagen, Denmark, 2014. Springer.
PDF (262 kB)
Info
Slides 
Tech report version
Tomáš Brázdil, Stefan Kiefer, Antonín Kučera, Petr Novotný, and Joost-Pieter Katoen. Zero-reachability in probabilistic multi-counter automata. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 22:1–22:10, Vienna, Austria, 2014.
PDF (368 kB)
Info
Tech report version
Tomáš Brázdil, Stefan Kiefer, Antonín Kučera, Petr Novotný, and Joost-Pieter Katoen. Zero-reachability in probabilistic multi-counter automata. Technical report, arXiv.org, 2014. Available at http://arxiv.org/abs/1401.6840.
Info
See arxiv.org ...
Conference version
Taolue Chen and Stefan Kiefer. On the total variation distance of labelled Markov chains. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 33:1–33:10, Vienna, Austria, 2014.
PDF (334 kB)
Info
Slides 
Tech report version
Taolue Chen and Stefan Kiefer. On the total variation distance of labelled Markov chains. Technical report, arXiv.org, 2014. Available at http://arxiv.org/abs/1405.2852.
Info
See arxiv.org ...
Conference version
Javier Esparza, Michael Luttenberger, and Maximilian Schlund. Fpsolve: A generic solver for fixpoint equations over semirings. In Implementation and Application of Automata - 19th International Conference, CIAA 2014, Giessen, Germany, July 30 - August 2, 2014. Proceedings, pages 1–15, 2014.
Info
See dx.doi.org ...
Michael Luttenberger and Maximilian Schlund. Regular expressions for provenance. In 6th Workshop on the Theory and Practice of Provenance, TaPP'14, Cologne, Germany, June 12-13, 2014, 2014.
Info
Javier Esparza, Michael Luttenberger, and Maximilian Schlund. A brief history of strahler numbers. In Language and Automata Theory and Applications - 8th International Conference, LATA 2014, Madrid, Spain, March 10-14, 2014. Proceedings, pages 1–13, 2014.
Info
Maximilian Schlund, Michael Luttenberger, and Javier Esparza. Fast and accurate unlexicalized parsing via structural annotations. In Proceedings of the 14th Conference of the European Chapter of the Association for Computational Linguistics, EACL 2014, April 26-30, 2014, Gothenburg, Sweden, pages 164–168, 2014.
Info
Tewodros A. Beyene, Swarat Chaudhuri, Corneliu Popeea, and Andrey Rybalchenko. A constraint-based approach to solving games on infinite graphs. In POPL, pages 221–234, January 2014.
Info
Corneliu Popeea, Andrey Rybalchenko, and Andreas Wilhelm. Reduction for compositional verification of multi-threaded programs. In Formal Methods in Computer-Aided Design, FMCAD 2014, 2014.
Info

2013

M. Schlund, M. Terepeta, and M. Luttenberger. Putting Newton into Practice: A Solver for Polynomial Equations over Semirings. In LPAR 2013, volume 8312 of Lecture Notes in Computer Science, pages 727–734, December 2013.
PDF (324 kB)
Info
Tewodros Beyene, Corneliu Popeea, and Andrey Rybalchenko. Solving existentially quantified Horn clauses. In CAV, July 2013.
Info
Corneliu Popeea and Wei-Ngan Chin. Dual analysis for proving safety and finding bugs. Sci. Comput. Program., 78(4):390–411, April 2013.
Info
M. Luttenberger and M. Schlund. Convergence of Newton's Method over Commutative Semirings. In LATA, volume 7810 of Lecture Notes in Computer Science, pages 407–418, April 2013.
PDF (367 kB)
Info
Corneliu Popeea and Andrey Rybalchenko. Threader: A verifier for multi-threaded programs - (competition contribution). In TACAS, pages 633–636, March 2013.
Info
Javier Esparza, Loïg Jezequel, and Stefan Schwoon. Computation of summaries using net unfoldings. In FSTTCS, pages 225–236, 2013.
PDF (740 kB)
Info
Javier Esparza and Jörg Desel. On negotiation as concurrency primitive. In CONCUR, 2013.
Info
Tech report version
Javier Esparza and Jörg Desel. On negotiation as concurrency primitive. Technical report, arXiv.org, 2013.
PDF (442 kB)
Info
Conference version
Javier Esparza, Pierre Ganty, and Rupak Majumdar. Parameterized verification of asynchronous shared-memory systems. In CAV, pages 124–140, 2013.
Info
Tech report version
Javier Esparza, Pierre Ganty, and Rupak Majumdar. Parameterized verification of asynchronous shared-memory systems. Technical report, arXiv.org, 2013.
Info
Conference version
Javier Esparza, Peter Lammich, Rene Neumann, Tobias Nipkow, Alexander Schimpf, and Jan-Georg Smaus. A fully verified executable LTL model checker. In CAV, pages 463–478, 2013.
PDF (363 kB)
Info
Javier Esparza, Andreas Gaiser, and Stefan Kiefer. A strongly polynomial algorithm for criticality of branching processes and consistency of stochastic context-free grammars. Inf. Process. Lett., 113(10-11):381–385, 2013.
PDF (170 kB)
Info
Stefan Kiefer. BPA bisimilarity is EXPTIME-hard. Information Processing Letters (IPL), 113(4):101–106, 2013.
PDF (160 kB)
Info
See dx.doi.org ...
Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, and James Worrell. On the complexity of equivalence and minimisation for Q-weighted automata. Logical Methods in Computer Science (LMCS), 9(1:8):1–22, 2013.
PDF (247 kB)
Info
See arxiv.org ...
Conference version
Javier Esparza, Andreas Gaiser, and Stefan Kiefer. A strongly polynomial algorithm for criticality of branching processes and consistency of stochastic context-free grammars. Information Processing Letters (IPL), 113(10–11):381–385, 2013.
PDF (167 kB)
Info
See dx.doi.org ...
Michael Benedikt, Stefan Göller, Stefan Kiefer, and Andrzej S. Murawski. Bisimilarity of pushdown automata is nonelementary. In Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 488–498, New Orleans, Louisiana, USA, 2013.
PDF (366 kB)
Info
See doi.ieeecomputersociety.org ...
Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, and James Worrell. Algorithmic probabilistic game semantics – playing games with automata. Formal Methods in System Design, 43(2):285–312, 2013.
PDF (1 MB)
Info
Tomáš Brázdil, Javier Esparza, Stefan Kiefer, and Antonín Kučera. Analyzing probabilistic pushdown automata. Formal Methods in System Design, 43(2):124–163, 2013.
PDF (1 MB)
Info
Tomas Brazdil, Vojtech Forejt, Jan Krcal, Jan Kretinsky, and Antonin Kucera. Continuous-time stochastic games with time-bounded reachability. Inf. Comput., 224:46–70, 2013.
Info
Krishnendu Chatterjee, Andreas Gaiser, and Jan Kretinsky. Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. In Sharygina and Veith, pages 559–575.
Info
Krishnendu Chatterjee, Andreas Gaiser, and Jan Kretinsky. Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. Technical Report abs/1304.5281, arXiv.org, 2013.
Info
Jan Kretinsky and Salomon Sickert. On refinements of Boolean and parametric modal transition systems. In Liu et al., pages 213–230.
Info
Jan Kretinsky and Salomon Sickert. On refinements of Boolean and parametric modal transition systems. Technical Report abs/1304.5278, arXiv.org, 2013.
Info
Tomas Brazdil, Lubos Korenciak, Jan Krcal, Jan Kretinsky, and Vojtech Rehak. On time-average limits in deterministic and stochastic Petri nets. In Seelam et al., pages 421–422.
Info
Nikola Benes, Benoit Delahaye, Uli Fahrenberg, Jan Kretinsky, and Axel Legay. Hennessy-Milner logic with greatest fixed points as a complete behavioural specification theory. In D'Argenio and Melgratti, pages 76–90.
Info
Nikola Benes, Benoit Delahaye, Uli Fahrenberg, Jan Kretinsky, and Axel Legay. Hennessy-Milner logic with greatest fixed points as a complete behavioural specification theory. Technical Report abs/1306.0741, arXiv.org, 2013.
Info
Holger Hermanns, Jan Krcal, and Jan Kretinsky. Compositional verification and optimization of interactive Markov chains. In D'Argenio and Melgratti, pages 364–379.
Info
Holger Hermanns, Jan Krcal, and Jan Kretinsky. Compositional verification and optimization of interactive Markov chains. Technical Report abs/1305.7332, arXiv.org, 2013.
Info
Jan Kretinsky and Salomon Sickert. MoTraS: A tool for modal transition systems and their extensions. In Hung and Ogawa, pages 487–491.
Info
Jan Kretinsky and Ruslan Ledesma-Garza. Rabinizer 2: Small deterministic automata for LTLGU. In Hung and Ogawa, pages 446–450.
Info
Maximilian Schlund, Michal Terepeta, and Michael Luttenberger. Putting newton into practice: A solver for polynomial equations over semirings. In Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings, pages 727–734, 2013.
Info
Philipp Hoffmann and Michael Luttenberger. Solving parity games on the GPU. In Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings, pages 455–459, 2013.
Info

2012

Taolue Chen, Klaus Dräger, and Stefan Kiefer. Model checking stochastic branching processes. Technical report, arXiv.org, June 2012. Available at http://arxiv.org/abs/1206.1317.
Info
See arxiv.org ...
Conference version
Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. Synthesizing software verifiers from proof rules. In PLDI, pages 405–416, June 2012.
Info
Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Proving termination of probabilistic programs using patterns. Technical report, arXiv.org, April 2012. Available at http://arxiv.org/abs/1204.2932.
Info
See arxiv.org ...
Conference version
Corneliu Popeea and Andrey Rybalchenko. Compositional termination proofs for multi-threaded programs. In TACAS, March 2012.
Info
Sergey Grebenshchikov, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. Hsf(c): A software verifier based on horn clauses - (competition contribution). In TACAS, pages 549–551, March 2012.
Info
Javier Esparza, Pierre Ganty, and Rupak Majumdar. A perfect model for bounded verification. In Twenty-Seventh Annual ACM/IEEE Symposium on Logic in Cmputer Sience (LICS 2012), pages 285–294, 2012.
PDF (350 kB)
Info
Javier Esparza, Pierre Ganty, and Rupak Majumdar. A perfect model for bounded verification. Technical report, arXiv.org, 2012.
Info
Javier Esparza and Jörg Kreiker. Three case studies on verification of infinite-state systems. In Modern Applications of Automata Theory. World Scientific Publishing, 2012.
PDF (424 kB)
Info
Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Proving termination of probabilistic programs using patterns. In Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, pages 123–138, 2012.
PDF (232 kB)
Info
Jan Kretinsky and Javier Esparza. Deterministic automata for the (F,G)-fragment of LTL. In Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, pages 7–22, 2012.
PDF (227 kB)
Info
Tech report version
Jan Kretinsky and Javier Esparza. Deterministic automata for the (F,G)-fragment of LTL. Technical Report abs/1106.1424, arXiv.org, 2012.
Info
Javier Esparza, Orna Kupferman, and Moshe Vardi. Verification. In Hanbook on Automata Theory. European Mathematical Society, 2012. To appear.
PDF (319 kB)
Info
Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Proving termination of probabilistic programs using patterns. In Proceedings of CAV 2012, Berkeley, USA, 2012.
Info
See www.model.in.tum.de ...
Tech report version
Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Proving termination of probabilistic programs using patterns. In Proceedings of CAV 2012, Berkeley, USA, 2012.
Info
See www.model.in.tum.de ...
Tech report version
Javier Esparza, Andreas Gaiser, and Jan Kretinsky. Rabinizer: Small Deterministic Automata for LTL(F,G). In 10th International Symposium on Automated Technology for Verification and Analysis (ATVA) 2012, Thiruvananthapuram, India, 2012.
Info
See www.model.in.tum.de ...
Javier Esparza and Christian Kern. Reactive and proactive diagnosis of distributed systems using net unfoldings. In ACSD, 2012. To appear.
Info
Tomáš Brázdil and Stefan Kiefer. Stabilization of branching queueing networks. In C. Dürr and T. Wilke, editors, Proceedings of the 29th International Symposium on Theoretical Aspects of Computer Science (STACS), pages 507–518, Paris, France, 2012.
PDF (675 kB)
Info
Slides 
Tech report version
Tomáš Brázdil, Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Space-efficient scheduling of stochastically generated tasks. Information and Computation, 210:87–110, January 2012.
PDF (418 kB)
Info
Conference version
Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, and James Worrell. On the complexity of the equivalence problem for probabilistic automata. Technical report, arXiv.org, January 2012. Available at http://arxiv.org/abs/1112.4644.
PDF (206 kB)
Info
See arxiv.org ...
Conference version
Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, and James Worrell. On the complexity of the equivalence problem for probabilistic automata. In Lars Birkedal, editor, Proceedings of the 15th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), volume 7213 of LNCS, pages 467–481, Tallinn, Estonia, 2012. Springer.
PDF (281 kB)
Info
Slides 
Tech report version, Journal version
Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, and James Worrell. Apex: An analyzer for open probabilistic programs. In Madhusudan Parathasarathy and Sanjit A. Seshia, editors, Proceedings of the 24th International Conference on Computer Aided Verification (CAV), volume 7358 of LNCS, pages 693–698, Berkeley, California, USA, 2012. Springer.
PDF (280 kB)
Info
Slides 
Taolue Chen, Klaus Dräger, and Stefan Kiefer. Model checking stochastic branching processes. In Vladimiro Sassone and Peter Widmayer, editors, Proceedings of the 37th International Symposium on Mathematical Foundations of Computer Science (MFCS), volume 7464 of LNCS, pages 271–282, Bratislava, Slovakia, 2012. Springer.
PDF (357 kB)
Info
Slides 
Tech report version
Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, and James Worrell. Three tokens in Herman's algorithm. Formal Aspects of Computing, 24(4):671–678, 2012.
PDF (281 kB)
Info
See dx.doi.org ...
Vojtěch Forejt, Petr Jančar, Stefan Kiefer, and James Worrell. Bisimilarity of probabilistic pushdown automata. In Deepak D'Souza, Telikepalli Kavitha, and Jaikumar Radhakrishnan, editors, Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), Leibniz International Proceedings in Informatics (LIPIcs), pages 448–460, Hyderabad, India, 2012.
PDF (565 kB)
Info
See drops.dagstuhl.de ...
Nikola Benes, Jan Kretinsky, Kim Guldstrand Larsen, Mikael H. Moller, and Jiri Srba. Dual-priced modal transition systems with time durations. In Bjørner and Voronkov, pages 122–137.
Info
Nikola Benes, Jan Kretinsky, Kim G. Larsen, Mikael H. Moller, and Jiri Srba. Dual-priced modal transition systems with time durations. Technical report FIMU-RS-2012-01, Faculty of Informatics, Masaryk University, Brno, 2012.
Info
Jan Kretinsky and Javier Esparza. Deterministic automata for the (F,G)-fragment of LTL. In Madhusudan and Seshia, pages 7–22.
Info
Jan Kretinsky and Javier Esparza. Deterministic automata for the (F,G)-fragment of LTL. Technical Report abs/1106.1424, arXiv.org, 2012.
Info
Nikola Benes and Jan Kretinsky. Modal process rewrite systems. In Roychoudhury and D'Souza, pages 120–135.
Info
Nikola Benes and Jan Kretinsky. Modal process rewrite systems. Technical report FIMU-RS-2012-02, Faculty of Informatics, Masaryk University, Brno, 2012.
Info
Andreas Gaiser, Jan Kretinsky, and Javier Esparza. Rabinizer: Small deterministic automata for LTL(F, G). In Chakraborty and Mukund, pages 72–76.
Info
Nikola Benes, Jan Kretinsky, Kim G. Larsen, and Jiri Srba. Exptime-completeness of thorough refinement on modal transition systems. Inf. Comput., 218:54–68, 2012.
Info
Tomas Brazdil, Holger Hermanns, Jan Krcal, Jan Kretinsky, and Vojtech Rehak. Verification of open interactive markov chains. In D'Souza et al., pages 474–485.
Info
Tomas Brazdil, Holger Hermanns, Jan Krcal, Jan Kretinsky, and Vojtech Rehak. Verification of open interactive markov chains. Technical report FIMU-RS-2012-04, Faculty of Informatics, Masaryk University, Brno, 2012.
Info
Visar Januzaj, Stefan Kugele, Florian Biechele, and Ralf Mauersberger. A Configuration Approach for IMA Systems. In George Eleftherakis, Mike Hinchey, and Mike Holcombe, editors, Software Engineering and Formal Methods, volume 7504 of Lecture Notes in Computer Science, pages 203–217. Springer Berlin / Heidelberg, 2012. 10.1007/978-3-642-33826-7_14.
Info
See dx.doi.org ...
Rene Neumann. A framework for verified depth-first algorithms. In Annabelle McIver and Peter Höfner, editors, Proc. of the Workshop on Automated Theory Exploration (ATX 2012), pages 36–45. EasyChair, 2012.
PDF (490 kB)
Info
See cava.in.tum.de ...

2011

Tomáš Brázdil and Stefan Kiefer. Stabilization of branching queueing networks. Technical report, arXiv.org, December 2011. Available at http://arxiv.org/abs/1112.1041.
PDF (594 kB)
Info
See arxiv.org ...
Conference version
Michael Luttenberger. An extension of Parikh's theorem beyond idempotence. Technical report, Technische Universität München, Institut für Informatik, December 2011.
Info
See arxiv.org ...
Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. Solving recursion-free horn clauses over LI+UIF. In APLAS, December 2011.
Info
Javier Esparza and Andreas Gaiser. Probabilistic abstractions with arbitrary domains. In Proceedings of the 18th International Static Analysis Symposium (SAS), Venice, Italy, September 2011.
PDF (305 kB)
Info
Slides 
Javier Esparza and Andreas Gaiser. Probabilistic abstractions with arbitrary domains. In Proceedings of the 18th International Static Analysis Symposium (SAS), Venice, Italy, September 2011.
PDF (305 kB)
Info
Slides 
Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. Threader: A constraint-based verifier for multi-threaded programs. In CAV, pages 412–417, July 2011.
Info
Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, James Worrell, and Lijun Zhang. On stabilization in Herman's algorithm. Technical report, arXiv.org, April 2011. Available at http://arxiv.org/abs/1104.3100.
PDF (253 kB)
Info
See arxiv.org ...
Conference version
Tomáš Brázdil, Stefan Kiefer, and Antonín Kučera. Efficient analysis of probabilistic programs with an unbounded counter. Technical report, arXiv.org, April 2011. Available at http://arxiv.org/abs/1102.2529.
Info
See arxiv.org ...
Conference version, Journal version
J. Esparza and P. Ganty. Complexity of pattern-based verification for multithreaded programs. In Proc. of the 38th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '11, 2011.
PDF (360 kB)
Info
Javier Esparza and Andreas Gaiser. Probabilistic abstractions with arbitrary domains. Technical report, Technische Universität München, 2011. Available via arxiv.org (arXiv:1106.1364).
Info
Javier Esparza and Andreas Gaiser. Probabilistic abstractions with arbitrary domains. Technical report, Technische Universität München, 2011. Available via arxiv.org (arXiv:1106.1364).
Info
Stefan Haar, Christian Kern, and Stefan Schwoon. Computing the reveals relation in occurrence nets. In GandALF, pages 31–44, 2011.
Info
Stefan Kiefer and Dominik Wojtczak. On probabilistic parallel programs with process creation and synchronisation. In P.A. Abdulla and K.R.M. Leino, editors, Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 6605 of LNCS, pages 296–310, Saarbrücken, Germany, 2011. Springer.
PDF (176 kB)
Info
Slides 
Tech report version
Javier Esparza, Pierre Ganty, Stefan Kiefer, and Michael Luttenberger. Parikh's theorem: A simple and direct automaton construction. Information Processing Letters (IPL), 111(12):614–619, 2011.
PDF (217 kB)
Info
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Derivation tree analysis for accelerated fixed-point computation. Theoretical Computer Science, 412(28):3226–3241, 2011.
PDF (279 kB)
Info
Conference version
Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, James Worrell, and Lijun Zhang. On stabilization in Herman's algorithm. In L. Aceto, M. Henzinger, and J. Sgall, editors, Proceedings of the 38th International Colloquium on Automata, Languages and Programming (ICALP), volume 6756 of LNCS, pages 466–477, Zürich, Switzerland, 2011. Springer.
PDF (190 kB)
Info
Slides 
Tech report version
Tomáš Brázdil, Stefan Kiefer, Antonín Kučera, and Ivana Hutařová Vařeková. Runtime analysis of probabilistic programs with unbounded recursion. In L. Aceto, M. Henzinger, and J. Sgall, editors, Proceedings of the 38th International Colloquium on Automata, Languages and Programming (ICALP), volume 6756 of LNCS, pages 319–331, Zürich, Switzerland, 2011. Springer.
PDF (157 kB)
Info
Journal version
Tomáš Brázdil, Stefan Kiefer, and Antonín Kučera. Efficient analysis of probabilistic programs with an unbounded counter. In G. Gopalakrishnan and S. Qadeer, editors, Proceedings of the 23rd International Conference on Computer Aided Verification (CAV), volume 6806 of LNCS, pages 208–224, Snowbird, Utah, USA, 2011. Springer.
PDF (177 kB)
Info
Slides 
Tech report version, Journal version
Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, and James Worrell. Language equivalence for probabilistic automata. In G. Gopalakrishnan and S. Qadeer, editors, Proceedings of the 23rd International Conference on Computer Aided Verification (CAV), volume 6806 of LNCS, pages 526–540, Snowbird, Utah, USA, 2011. Springer.
PDF (202 kB)
Info
Tomas Brazdil, Jan Krcal, Jan Kretinsky, Antonin Kucera, and Vojtech Rehak. Measuring performance of continuous-time stochastic processes using timed automata. In Caccamo et al., pages 33–42.
Info
Tomas Brazdil, Jan Krcal, Jan Kretinsky, Antonin Kucera, and Vojtech Rehak. Measuring performance of continuous-time stochastic processes using timed automata. Technical Report abs/1101.4204, arXiv.org, 2011.
Info
Jan Kretinsky. Probabilistic timed systems with non-determinism. PhD Thesis proposal, Masaryk University, Brno, Dept. of Computer Science, 2011.
Info
Tomas Brazdil, Jan Krcal, Jan Kretinsky, and Vojtech Rehak. Fixed-delay events in generalized semi-markov processes revisited. In CONCUR, pages 140–155, 2011.
Info
Tomas Brazdil, Jan Krcal, Jan Kretinsky, and Vojtech Rehak. Fixed-delay events in generalized semi-markov processes revisited. Technical Report abs/1106.1424, arXiv.org, 2011.
Info
Nikola Benes, Ivana Cerna, and Jan Kretinsky. Modal transition systems: Composition and LTL model checking. In Bultan and Hsiung, pages 228–242.
Info
Nikola Benes, Jan Kretinsky, Kim G. Larsen, Mikael H. Moller, and Jiri Srba. Parametric modal transition systems. In Bultan and Hsiung, pages 275–289.
Info
Nikola Benes, Jan Kretinsky, Kim G. Larsen, Mikael H. Moller, and Jiri Srba. Parametric modal transition systems. Technical report FIMU-RS-2011-03, Faculty of Informatics, Masaryk University, Brno, 2011.
Info
Andreas Holzer, Visar Januzaj, Stefan Kugele, Boris Langer, Christian Schallhart, Michael Tautschnig, and Helmut Veith. Seamless testing for models and code. In Dimitra Giannakopoulou and Fernando Orejas, editors, Fundamental Approaches to Software Engineering - 14th International Conference, FASE 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, volume 6603 of Lecture Notes in Computer Science, pages 278–293. Springer, 2011.
Info
Javier Esparza and Michael Luttenberger. Solving fixed-point equations by derivation tree analysis. In CALCO, pages 19–35, 2011.
Info
Chih-Hong Cheng, Alois Knoll, Michael Luttenberger, and Christian Buckl. Gavs+: An open platform for the research of algorithmic game solving. In TACAS, pages 258–261, 2011.
Info
Andrey Rybalchenko and Juan Antonio Navarro. Separation logic + Superposition calculus = Heap theorem prover. In PLDI'11: Proceedings of the 32nd ACM SIGPLAN conference on Programming language design and implementation, San Jose, CA, USA, 2011. ACM Press.
PDF (287 kB)
Info
See navarroj.com ...
Slides 
Rene Neumann. Development of a concurrent language featuring a type system based on boolean implications. Master's thesis, Technische Universität München, 2011.
PDF (709 kB)
Info
Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. Predicate abstraction and refinement for verifying multi-threaded programs. In POPL, pages 331–344, January 2011.
Info
Ruslan Ledesma-Garza. Verification of Temporal Properties of Functional Programs. Master's thesis, Saarland University, 2011.
Info
Ranjit Jhala, Rupak Majumdar, and Andrey Rybalchenko. Hmc: Verifying functional programs using abstract interpreters. In Gopalakrishnan and Qadeer, pages 470–485.
Info
Andrey Rybalchenko. Towards automatic synthesis of software verification tools. In Schneider-Kamp and Hanus, pages 3–4.
Info
Andreas Podelski and Andrey Rybalchenko. Transition invariants and transition predicate abstraction for program termination. In Abdulla and Leino, pages 3–10.
Info
Nuno P. Lopes and Andrey Rybalchenko. Distributed and predictable software model checking. In Jhala and Schmidt, pages 340–355.
Info
Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Proving program termination. Commun. ACM, 54(5):88–98, 2011.
Info
J. Esparza, M. Leucker, and M. Schlund. Learning workflow Petri nets. Fundamenta Informaticae, 113(3-4):205–228, 2011.
PDF (212 kB)
Info

2010

Javier Esparza and Andreas Gaiser. Probabilistic abstractions with arbitrary domains. Technical report, Technische Universität München, Institut für Informatik, December 2010.
PDF (426 kB)
Info
Javier Esparza and Andreas Gaiser. Probabilistic abstractions with arbitrary domains. Technical report, Technische Universität München, Institut für Informatik, December 2010.
PDF (426 kB)
Info
Stefan Kiefer and Dominik Wojtczak. On probabilistic parallel programs with process creation and synchronisation. Technical report, arXiv.org, December 2010. Available at http://arxiv.org/abs/1012.2998.
PDF (254 kB)
Info
See arxiv.org ...
Conference version
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Newtonian program analysis. Journal of the ACM, 57(6):33:1–33:47, October 2010.
Info
Tech report version
Wolfgang Haberl, Markus Herrmannsdoerfer, Stefan Kugele, Michael Tautschnig, and Martin Wechs. Seamless model-driven development put into practice. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification, and Validation, volume 6415 of Lecture Notes in Computer Science, pages 18–32. Springer, October 2010.
Info
Andreas Holzer, Visar Januzaj, Stefan Kugele, and Michael Tautschnig. Timely time estimates. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification, and Validation, volume 6415 of Lecture Notes in Computer Science, pages 33–46. Springer, October 2010.
Info
Rene Neumann. Functional binomial queues. Archive of Formal Proofs, October 2010. Formal proof development.
Info
See afp.sf.net ...
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Newtonian program analysis. Technical report, Technische Universität München, Institut für Informatik, September 2010. This is a late draft of the article in the Journal of the ACM.
PDF (422 kB)
Info
Journal version
Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. Non-monotonic refinement of control abstraction for concurrent programs. In ATVA, pages 188–202, September 2010.
Info
Wolfgang Haberl, Stefan Kugele, and Uwe Baumgarten. Model-Based Generation of Fault-Tolerant Embedded Systems. In Hamid R. Arabnia and Ashu M. G. Solo, editors, Proceedings of the 2010 International Conference on Embedded Systems and Applications, ESA 2010, pages 136–142, Las Vegas, Nevada, USA, July 2010. CSREA Press.
Info
Tomáš Brázdil, Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Space-efficient scheduling of stochastically generated tasks. Technical report, arXiv.org, April 2010. Available at http://arxiv.org/abs/1004.4286.
PDF (278 kB)
Info
See arxiv.org ...
Conference version, Journal version
Corneliu Popeea and Wei-Ngan Chin. Dual analysis for proving safety and finding bugs. In SAC, pages 2137–2143, March 2010.
Info
B König and J. Esparza. Verification of graph transformation systems with context-free specifications. In Proc. of the 5th International Conference on Graph Transformations, 2010.
PDF (289 kB)
Info
J. Esparza, M. Leucker, and M. Schlund. Learning workflow Petri nets. In Proc. of the 31st International Conference on Applications and Theory of Petri Nets, 2010.
PDF (274 kB)
Info
J. Esparza. A false history of true concurrency: from Petri to tools. In Proc. of the 17th International SPIN Workshop, 2010.
PDF (112 kB)
Info
Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Computing least fixed points of probabilistic systems of polynomials. In Proceedings of the 27th International Symposium on Theoretical Aspects of Computer Science (STACS), Nancy, France, 2010.
PDF (247 kB)
Info
Tech report version
Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Computing least fixed points of probabilistic systems of polynomials. In Proceedings of the 27th International Symposium on Theoretical Aspects of Computer Science (STACS), Nancy, France, 2010.
PDF (247 kB)
Info
Tech report version
Christian Kern. Automatic error correction of java programs. In AlgoSyn, page 155, 2010.
Info
Christian Kern and Javier Esparza. Automatic error correction of java programs. In FMICS, pages 67–81, 2010.
Info
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Computing the least fixed point of positive polynomial systems. Technical report, arXiv.org, January 2010. Available at http://arxiv.org/abs/1001.0340.
PDF (899 kB)
Info
See arxiv.org ...
Journal version
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Computing the least fixed point of positive polynomial systems. SIAM Journal on Computing, 39(6):2282–2335, 2010.
PDF (845 kB)
Info
Tech report version
Tomáš Brázdil, Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Space-efficient scheduling of stochastically generated tasks. In Samson Abramsky et al., editor, Proceedings of the 37th International Colloquium on Automata, Languages and Programming (ICALP), part II, volume 6199 of LNCS, ARCoSS, pages 539–550, Bordeaux, France, 2010. Springer.
PDF (151 kB)
Info
Slides 
Tech report version, Journal version
Jan Kretinsky. Modal transition systems. Master's thesis, Masaryk University, Brno, Dept. of Mathematics, 2010.
Info
Tomas Brazdil, Jan Krcal, Jan Kretinsky, Antonin Kucera, and Vojtech Rehak. Stochastic real-time games with qualitative timed automata objectives. In CONCUR, pages 207–221, 2010.
Info
Tomas Brazdil, Jan Krcal, Jan Kretinsky, Antonin Kucera, and Vojtech Rehak. Stochastic real-time games with qualitative timed automata objectives. Technical report FIMU-RS-2010-05, Faculty of Informatics, Masaryk University, Brno, 2010.
Info
Nikola Benes and Jan Kretinsky. Process algebra for modal transition systemses. In MEMICS, pages 9–18, 2010.
Info
Nikola Benes and Jan Kretinsky. Process algebra for modal transition systemses. Technical report FIMU-RS-2010-11, Faculty of Informatics, Masaryk University, Brno, 2010.
Info
Nikola Benes, Ivana Cerna, and Jan Kretinsky. Disjunctive modal transition systems and generalized LTL model checking. Technical report FIMU-RS-2010-12, Faculty of Informatics, Masaryk University, Brno, 2010.
Info
Michael Luttenberger. Solving systems of polynomial equations: A generalization of newton's method. PhD thesis, Technische Universität München, 2010.
PDF (1 MB)
Info
Chih-Hong Cheng, Christian Buckl, Michael Luttenberger, and Alois Knoll. Gavs: Game arena visualization and synthesis. In ATVA, pages 347–352, 2010.
Info
See dx.doi.org ...
Javier Esparza, Pierre Ganty, Stefan Kiefer, and Michael Luttenberger. Parikh's theorem: A simple and direct construction. CoRR, abs/1006.3825, 2010.
Info
See arxiv.org ...
Andrey Rybalchenko. Constraint solving for program verification: Theory and practice by example. In Touili et al., pages 57–71.
Info
Boris Köpf and Andrey Rybalchenko. Approximation and randomization for quantitative information-flow analysis. In CSF, pages 3–14.
Info
Andrey Rybalchenko. Constraint solving for program verification: Theory and practice by example. In Dawar and Veith, page 51.
Info
Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács, and Andrey Rybalchenko. Aligators for arrays (tool paper). In Fermüller and Voronkov, pages 348–356.
Info
Alexander Malkis, Andreas Podelski, and Andrey Rybalchenko. Thread-modular counterexample-guided abstraction refinement. In Cousot and Martel, pages 356–372.
Info
Andrey Rybalchenko and Viorica Sofronie-Stokkermans. Constraint solving for interpolation. J. Symb. Comput., 45(11):1212–1233, 2010.
Info
Nuno P. Lopes, Juan Antonio Navarro Pérez, Andrey Rybalchenko, and Atul Singh. Applying prolog to develop distributed systems. TPLP, 10(4-6):691–707, 2010.
Info

2009

Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Computing least fixed points of probabilistic systems of polynomials. Technical report, Technische Universität München, Institut für Informatik, December 2009.
PDF (349 kB)
Info
Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Computing least fixed points of probabilistic systems of polynomials. Technical report, Technische Universität München, Institut für Informatik, December 2009.
PDF (349 kB)
Info
Andreas Gaiser and Stefan Schwoon. Comparison of algorithms for checking emptiness on Büchi automata. In Tomáš Vojnar, Petr Hliněný, Vashek Matyáš, and David Antoš, editors, Proceedings of the 5th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS), pages 69–77, Znojmo, Czechia, November 2009.
PDF (150 kB)
Info
Tech report version
Tomáš Brázdil, Javier Esparza, and Stefan Kiefer. On the memory consumption of probabilistic pushdown automata. Technical Report FIMU-RS-2009-07, Faculty of Informatics, Masaryk University, October 2009.
PDF (447 kB)
Info
Conference version
Andreas Holzer, Visar Januzaj, Stefan Kugele, Christian Schallhart, Michael Tautschnig, Helmut Veith, and Boris Langer. Slope testing for activity diagrams and safety critical software. Technical Report TUD-CS-2009-0184, Technische Universität Darmstadt, October 2009.
PDF (403 kB)
Info
Visar Januzaj and Stefan Kugele. Model analysis via a translation schema to coloured petri nets. In Daniel Moldt, editor, PNSE'09: Proceedings of the International Workshop on Petri Nets and Software Engineering, pages 273–292, June 2009.
PDF (563 kB)
Info
Wolfgang Haberl, Stefan Kugele, and Uwe Baumgarten. Reliable operating modes for distributed embedded systems. In Proceedings of the ICSE Workshop on Model-based Methodologies for Pervasive and Embedded Software, volume 0, pages 11–21, Los Alamitos, CA, USA, May 2009. IEEE Computer Society.
PDF (2 MB)
Info
Morten Kühnrich, Stefan Schwoon, Jiří Srba, and Stefan Kiefer. Interprocedural dataflow analysis over weight domains with infinite descending chains. In Luca de Alfaro, editor, Proceedings of the 12th International Conference on Foundations of Software Science and Computational Structures (FOSSACS), volume 5504 of Lecture Notes in Computer Science, pages 440–455, York, UK, March 2009. Springer.
PDF (211 kB)
Info
Tech report version
Tomáš Brázdil, Javier Esparza, and Stefan Kiefer. On the memory consumption of probabilistic pushdown automata. In Ravi Kannan and K. Narayan Kumar, editors, Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), Leibniz International Proceedings in Informatics, pages 49–60, Kanpur, India, 2009.
PDF (162 kB)
Info
See drops.dagstuhl.de ...
Slides 
Tech report version
Stefan Kiefer. Solving systems of positive polynomial equations. PhD thesis, Technische Universität München, 2009.
PDF (931 kB)
Info
Slides 
Jan Kretinsky. Fundamental properties of probabilistic branching-time logics. Master's thesis, Masaryk University, Brno, Dept. of Computer Science, 2009.
Info
Nikola Benes, Jan Kretinsky, Kim Guldstrand Larsen, and Jiri Srba. Checking thorough refinement on modal transition systems is exptime-complete. In ICTAC, pages 112–126, 2009.
Info
Nikola Benes, Jan Kretinsky, Kim Guldstrand Larsen, and Jiri Srba. Checking thorough refinement on modal transition systems is exptime-complete. Technical report FIMU-RS-2009-03, Faculty of Informatics, Masaryk University, Brno, 2009.
Info
Nikola Benes, Jan Kretinsky, Kim Guldstrand Larsen, and Jiri Srba. On determinism in modal transition systems. Theor. Comput. Sci., 410(41):4026–4043, 2009.
Info
Tomas Brazdil, Vojtech Forejt, Jan Krcal, Jan Kretinsky, and Antonin Kucera. Continuous-time stochastic games with time-bounded reachability. In FSTTCS, pages 61–72, 2009.
Info
Tomas Brazdil, Vojtech Forejt, Jan Krcal, Jan Kretinsky, and Antonin Kucera. Continuous-time stochastic games with time-bounded reachability. Technical report FIMU-RS-2009-09, Faculty of Informatics, Masaryk University, Brno, 2009.
Info
Wolfgang Haberl, Markus Herrmannsdoerfer, Stefan Kugele, Michael Tautschnig, and Martin Wechs. One click from model to reality, 2009. Accepted for presentation at SAASE '09: Symposium on Automotive/Avionics Systems Engineering.
Info
Andreas Holzer, Visar Januzaj, and Stefan Kugele. Towards resource consumption-aware programming. In Kenneth Boness, João M. Fernandes, Jon G. Hall, Ricardo Jorge Machado, and Roy Oberhauser, editors, The Fourth International Conference on Software Engineering Advances, ICSEA 2009, 20-25 September 2009, Porto, Portugal, pages 490–493. IEEE Computer Society, 2009.
PDF (184 kB)
Info
Morten Kühnrich, Stefan Schwoon, Jiří Srba, and Stefan Kiefer. Interprocedural dataflow analysis over weight domains with infinite descending chains. Technical Report 0901.0501, Computing Research Repository, 2009.
PDF (242 kB)
Info
Conference version
Andreas Gaiser and Stefan Schwoon. Comparison of algorithms for checking emptiness on Büchi automata. Technical Report 0910.3766, Computing Research Repository, 2009.
PDF (160 kB)
Info
Conference version
Dejvuth Suwimonteerabuth. Reachability in pushdown systems: Algorithms and applications. PhD thesis, Technische Universität München, 2009.
PDF (1002 kB)
Info

2008

Paolo Baldan, Andrea Corradini, Barbara König, and Stefan Schwoon. McMillan's complete prefix for contextual nets. Transactions on Petri Nets and Other Models of Concurrency, 1:199–220, November 2008. Volume 5100 of Lecture Notes in Computer Science.
GZipped PostScript (127 kB)
Info
Conference version
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Derivation tree analysis for accelerated fixed-point computation. Technical report, Technische Universität München, Institut für Informatik, September 2008.
GZipped PostScript (174 kB)
PDF (220 kB)
Info
Conference version
Martin Sachenbacher and Stefan Schwoon. Model-based test generation using quantified CSPs. In Alban Grastien, Wolfgang Mayer, and Markus Stumptner, editors, Proceedings of the 19th International Workshop on Principles of Diagnosis (DX), pages 159–165, Blue Mountains, Australia, September 2008.
Info
See also SS08a.
Dejvuth Suwimonteerabuth, Javier Esparza, and Stefan Schwoon. Symbolic context-bounded analysis of multithreaded java programs. In Klaus Havelund and Rupak Majumdar, editors, Proceedings of SPIN 2008, volume 5156 of Lecture Notes in Computer Science, pages 270–287, Los Angeles, USA, August 2008. Springer.
PDF (214 kB)
Info
Stefan Kugele and Wolfgang Haberl. Mapping Data-Flow Dependencies onto Distributed Embedded Systems. In Hamid R. Arabnia and Hassan Reza, editors, Proceedings of the 2008 International Conference on Software Engineering Research & Practice, SERP 2008, volume 1, pages 272–278. CSREA Press, July 2008.
PDF (158 kB)
Info
Martin Sachenbacher and Stefan Schwoon. Model-based test generation using quantified CSPs: A map. In Bernhard Peischl, Neal Snooke, Gerald Steinbauer, and Cees Witteveen, editors, Proceedings of the ECAI 2008 Workshop on Model-Based Systems, pages 37–41, Patras, Greece, July 2008.
Info
See also SS08b.
Zhonglei Wang, Wolfgang Haberl, Stefan Kugele, and Michael Tautschnig. Automatic Generation of SystemC Models from Component-based Designs for Early Design Validation and Performance Analysis. In Proceedings of the 7th International Workshop on Software and Performance, WOSP 2008, pages 23–26, Princeton, NJ, USA, June 2008. ACM.
PDF (224 kB)
Info
Javier Esparza, Stefan Kiefer, and Stefan Schwoon. Abstraction refinement with Craig interpolation and symbolic pushdown systems. Journal on Satisfiability, Boolean Modeling and Computation, 5:27–56, June 2008. Special Issue on Constraints to Formal Verification.
PDF (322 kB)
Info
Tech report version, Conference version
Achim Rettinger, Matthias Nickles, and Volker Tresp. A statistical relational model for trust learning. In Proceedings of the 7th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2008), May 2008.
PDF (982 kB)
Info
Michael Luttenberger. Strategy iteration using non-deterministic strategies for solving parity games. Technical report, Technische Universität München, Institut für Informatik, April 2008.
PDF (190 kB)
Info
Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, and Dejvuth Suwimonteerabuth. SDSIrep: A reputation system based on SDSI. In C.R. Ramakrishnan and Jakob Rehof, editors, Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 4963 of Lecture Notes in Computer Science, pages 501–516, Budapest, Hungary, April 2008. Springer.
GZipped PostScript (76 kB)
Info
Sven Bünte and Michael Tautschnig. A Benchmarking Suite for Measurement-Based WCET Analysis Tools. In First International Conference on Software Testing, Verification and Validation (ICST), Lillehammer, Norway, April 2008. IEEE Computer Society Press.
PDF (135 kB)
Info
Wolfgang Haberl, Michael Tautschnig, and Uwe Baumgarten. Running COLA on Embedded Systems. In Proceedings of The International MultiConference of Engineers and Computer Scientists 2008, Hongkong, China, March 2008.
PDF (179 kB)
Info
Javier Esparza, Thomas Gawlitza, Stefan Kiefer, and Helmut Seidl. Approximative methods for monotone systems of min-max-polynomial equations. Technical report, Technische Universität München, Institut für Informatik, February 2008.
GZipped PostScript (181 kB)
PDF (267 kB)
Info
Conference version
Javier Esparza and Keijo Heljanko. Unfoldings - a partial-order approach to model checking. EATCS Monographs in Theoretical Computer Science. Springer-Verlag, 2008.
PDF (961 kB)
Info
See www.springer.com ...
Author created final book draft made available through our publishing agreement with Springer. Can not be made available on any other Web sites than the author homepages. The book can be purchased from the publisher. If you are interested, follow the link above.
J. Esparza, P. Jančar, and A. Miller. On the complexity of consistency and complete state coding for signal transition graphs. Fundamenta Informaticae, 86(3):227–253, 2008.
PDF (189 kB)
Info
Conference version, Tech report version
J. Bauer, Iovka Boneva, Arend Rensink, and Marcos E. Kurban. A modal-logic based graph abstraction. In Reiko Heckel and Gabriele Taentzer, editors, International Conference of Graph Transformation. Springer, 2008.
PDF (338 kB)
Info
J. Bauer, Flemming Nielson, Hanne Riis Nielson, and Henrik Pilegaard. Relational analysis of correlation. In 15th International Static Analysis Symposium, volume tba of Lecture Notes in Computer Science. Springer, 2008.
PDF (278 kB)
Info
Björn Schuller, Matthias Wimmer, Lorenz Moesenlechner, Christian Kern, Dejan Arsic, and Gerhard Rigoll. Brute-forcing hierarchical functionals for paralinguistics: A waste of feature space?. In ICASSP, pages 4501–4504, 2008.
Info
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Convergence thresholds of Newton's method for monotone polynomial equations. In Pascal Weil and Susanne Albers, editors, Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science (STACS), pages 289–300, Bordeaux, France, 2008. Available at http://arxiv.org/abs/0802.2856.
GZipped PostScript (210 kB)
PDF (199 kB)
Info
See arxiv.org ...
Tech report version
Javier Esparza, Thomas Gawlitza, Stefan Kiefer, and Helmut Seidl. Approximative methods for monotone systems of min-max-polynomial equations. In Luca Aceto et al., editor, Proceedings of the 35th International Colloquium on Automata, Languages and Programming (ICALP), part I, volume 5125 of LNCS, pages 698–710, Reykjavik, Iceland, 2008. Springer.
GZipped PostScript (115 kB)
PDF (147 kB)
Info
Tech report version
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Solving monotone polynomial equations. In Fifth IFIP International Conference On Theoretical Computer Science (TCS), volume 273 of IFIP International Federation for Information Processing, pages 285–298, Milano, Italy, 2008. Springer. Invited paper.
GZipped PostScript (67 kB)
PDF (107 kB)
Info
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Newton's method for -continuous semirings. In Luca Aceto et al., editor, Proceedings of the 35th International Colloquium on Automata, Languages and Programming (ICALP), part II, volume 5126 of LNCS, pages 14–26, Reykjavik, Iceland, 2008. Springer. Invited paper.
GZipped PostScript (113 kB)
PDF (140 kB)
Info
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Derivation tree analysis for accelerated fixed-point computation. In Masami Ito and Masafumi Toyama, editors, Proceedings of the 12th International Conference on Developments in Language Theory (DLT), volume 5257 of LNCS, pages 301–313, Kyoto, Japan, 2008. Springer.
GZipped PostScript (127 kB)
PDF (147 kB)
Info
Tech report version, Journal version
Tomas Brazdil, Vojtech Forejt, Jan Kretinsky, and Antonin Kucera. The satisfiability problem for probabilistic CTL. In LICS, pages 391–402, 2008.
Info
Tomas Brazdil, Vojtech Forejt, Jan Kretinsky, and Antonin Kucera. The satisfiability problem for probabilistic CTL. Technical report FIMU-RS-2008-03, Faculty of Informatics, Masaryk University, Brno, 2008.
Info
Stefan Kugele, Wolfgang Haberl, Michael Tautschnig, and Martin Wechs. Optimizing automatic deployment using non-functional requirement annotations. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation, volume 17 of CCIS, pages 400–414. Springer, 2008.
PDF (221 kB)
Info
Javier Esparza, Pradeep Kanade, and Stefan Schwoon. A negative result on depth-first unfoldings. Software Tools for Technology Transfer, 10(2):161–166, 2008.
GZipped PostScript (80 kB)
Info

2007

Andreas Bauer, Martin Leucker, Christian Schallhart, and Michael Tautschnig. Don't care in SMT—building flexible yet efficient abstraction/refinement solvers. In Proceedings of the 2007 ISoLA Workshop On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), pages 135–146, Poitiers, France, December 2007.
PDF (138 kB)
Info
Mihai Christodorescu, Johannes Kinder, Somesh Jha, Stefan Katzenbeisser, and Helmut Veith. Software transformations to improve malware detection. Journal in Computer Virology, 3(4):253–265, November 2007.
PDF (306 kB)
Info
Tech report version
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Convergence thresholds of Newton's method for monotone polynomial equations. Technical report, Technische Universität München, Institut für Informatik, October 2007.
GZipped PostScript (206 kB)
PDF (287 kB)
Info
Conference version
Achim Rettinger, Matthias Nickles, and Volker Tresp. Learning initial trust among interacting agents. In Eleventh International Workshop CIA 2007 on Cooperative Information Agents. Springer 2007, September 2007.
PDF (315 kB)
Info
Stefan Kugele, Michael Tautschnig, Andreas Bauer, Christian Schallhart, Stefano Merenda, Wolfgang Haberl, Christian Kühnel, Florian Müller, Zhonglei Wang, Doris Wild, Sabine Rittmann, and Martin Wechs. COLA – The component language. Technical Report TUM-I0714, Institut für Informatik, Technische Universität München, September 2007.
PDF (427 kB)
Info
Christian Kühnel, Andreas Bauer, and Michael Tautschnig. Compatibility and reuse in component-based systems via type and unit inference. In Proceedings of the 33rd EUROMICRO Conference on Software Engineering and Advanced Applications (SEAA), pages 101–108, Lübeck, Germany, August 2007. IEEE Computer Society Press.
PDF (157 kB)
Info
Tech report version
Dejvuth Suwimonteerabuth, Felix Berger, Stefan Schwoon, and Javier Esparza. jMoped: A test environment for Java programs. In Werner Damm and Holger Hermanns, editors, Proceedings of the 19th International Conference on Computer Aided Verification (CAV), volume 4590 of Lecture Notes in Computer Science, pages 164–167, Berlin, Germany, July 2007. Springer.
GZipped PostScript (104 kB)
Info
Paolo Baldan, Andrea Corradini, Barbara König, and Stefan Schwoon. McMillan's complete prefix for contextual nets. In Eric Fabre and Victor Khomenko, editors, Proceedings of UFO 2007, pages 32–49, Siedlce, Poland, June 2007.
GZipped PostScript (114 kB)
Info
Journal version
Christian Kühnel, Andreas Bauer, and Michael Tautschnig. Compatibility and reuse in component-based systems via type and unit inference. Technical Report TUM-I0716, Institut für Informatik, Technische Universität München, May 2007.
PDF (225 kB)
Info
Andreas Bauer, Markus Pister, and Michael Tautschnig. Tool-support for the analysis of hybrid systems and models. In Proceedings of the 2007 Conference on Design, Automation and Test in Europe (DATE), pages 924–929, Nice, France, April 2007. European Design and Automation Association.
PDF (213 kB)
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
J. Bauer, Werner Damm, Tobe Toben, and Bernd Westphal. Verification and Synthesis of Ocl Constraints via Topology Analysis: A Case Study. In Applications of Graph Transformations with Industrial Relevance Third International Symposium. Springer, 2007.
PDF (196 kB)
Info
J. Bauer, Tobe Toben, and Bernd Westphal. Mind the shapes: Abstraction refinement via topology invariants. In Kedar S. Namjoshi, Tomohiro Yoneda, Teruo Higashino, and Yoshio Okamura, editors, Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, Tokyo, Japan, October 22-25, 2007, Proceedings, volume 4762, pages 35–50. Springer, 2007.
PDF (707 kB)
Info
Flemming Nielson, Hanne Riis Nielson, J. Bauer, Christoffer Rosenkilde Nielsen, and Henrik Pilegaard. Relational analysis for delivery of services. In Trustworthy Global Computing, volume 4912, pages 73–89. Springer, 2007.
PDF (256 kB)
Info
J. Bauer and Reinhard Wilhelm. Static Analysis of Dynamic Communication Systems. In 14th International Static Analysis Symposium, volume 4634. Springer, 2007.
PDF (273 kB)
Info
Thomas Reps, Mooly Sagiv, and J. Bauer, editors. Program analysis and compilation, theory and practice, essays dedicated to reinhard wilhelm on the occasion of his 60th birthday, volume 4444 of Lecture Notes in Computer Science. Springer, 2007.
Info
Thomas Reps, Mooly Sagiv, and J. Bauer. An appreciation of the work of reinhard wilhelm. In Festschrift, pages 1–11.
PDF (38 kB)
Info
Christian Kern, Mohammad Khaleghi, Stefan Kugele, Christian Schallhart, Michael Tautschnig, and Andreas Weis. Sat7 engineering a modular sat-solver, 2007.
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 LNCS, pages 296–307, Aachen, Germany, 2007. Springer.
GZipped PostScript (179 kB)
PDF (162 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), pages 217–226, San Diego, California, USA, 2007. ACM.
GZipped PostScript (192 kB)
PDF (183 kB)
Info
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. An extension of Newton's method to -continuous semirings. In Tero Harju, Juhani Karhumäki, and Arto Lepistö, editors, Proceedings of the 11th International Conference on Developments in Language Theory (DLT), volume 4588 of LNCS, pages 157–168, Turku, Finland, 2007. Springer.
GZipped PostScript (178 kB)
PDF (167 kB)
Info
Tech report version
Andreas Holzer, Johannes Kinder, and Helmut Veith. Using verification technology to specify and detect malware. In 11th International Conference on Computer Aided Systems Theory (EUROCAST 2007), volume 4739 of Lecture Notes in Computer Science, pages 497–504. Springer, 2007.
PDF (80 kB)
Info
M. Nickles. Social acquisition of ontologies from communication processes. Journal of Applied Ontology, special issue "Formal Ontologies for Communicating Agents", 2007.
Info
M. Nickles, M. Rovatsos, M. Schmitt, W. Brauer, F. Fischer, Th. Malsch, K. Paetow, and G. Weiß. The Empirical Semantics Approach to Communication Structure Learning and Usage: Individuals- vs. System-Views. Journal of Artificial Societies and Social Simulation (JASSS), Issue on Socionics, 2007.
Info
M. Nickles. Towards a logic of graded normativity and norm adherence. In G. Boella, L. van der Torre, and H. Verhagen, editors, Proceedings of the Dagstuhl Seminar on Normative Multiagent Systems (NORMAS-07). Dagstuhl, 2007.
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
Andreas Holzer. Description Languages for Malicious Software. Master's thesis, Technische Universität München, November 2006.
Info
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
Stefan Kugele. Efficient Solving of Combinatorial Problems using SAT-Solvers. Master's thesis, Technische Universität München, October 2006.
PDF (2 MB)
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, Journal version
Achim Rettinger, Martin Zinkevich, and Michael Bowling. Boosting expert ensembles for rapid concept recall. In AAAI'06 Proceedings, The Twenty-First National Conference on Artificial Intelligence and the Eighteenth Innovative Applications of Artificial Intelligence Conference. AAAI Press 2006, July 2006.
PDF (241 kB)
Info
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, Journal version
J. Bauer and R. Wilhelm. Analysis of Dynamic Communicating Systems by Hierarchical Abstraction. Seminar proceedings 06081, Dagstuhl, Feb 2006.
PDF (579 kB)
Info
Michael Tautschnig. Development of a tool to solve mixed logical/linear constraint problems. Master's thesis, Technische Universität München, February 2006.
PDF (344 kB)
Info
A. Bouajjani and J. Esparza. Rewriting models of boolean programs. In Proceedings of RTA 2006, Seattle, USA, 2006.
GZipped PostScript (44 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
J. Bauer, Ina Schaefer, Tobe Toben, and Bernd Westphal. Specification and Verification of Dynamic Communication Systems. In Application of Concurrency to System Design, 2006. ACSD 2006. Sixth International Conference on. IEEE Computer Society Press, 2006.
PDF (163 kB)
Info
J. Bauer. Analysis of Communication Topologies by Partner Abstraction. PhD thesis, Universität des Saarlandes, 2006.
PDF (1 MB)
Info
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, Journal 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 LNCS, pages 489–503, Vienna, Austria, 2006. Springer.
GZipped PostScript (182 kB)
PDF (174 kB)
Info
Tech report version, Journal version
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
B. Gaudou, A. Herzig, D. Longin, and M. Nickles. A new semantics for the fipa agent communication language based on social attitudes.. In Proceedings ECAI 2006, 17th European Conference on Artificial Intelligence, August 29 - September 1, 2006, Riva del Garda, Italy, pages 245–249, 2006.
Info
F. A. Fischer and M. Nickles. Computational opinions.. In Proceedings ECAI 2006, 17th European Conference on Artificial Intelligence, August 29 - September 1, 2006, Riva del Garda, Italy, pages 240–244, 2006.
Info
M. Nickles. Modeling social attitudes on the web.. In Proceedings ISWC 2006, 5th International Semantic Web Conference, ISWC 2006, Athens, GA, USA, November 5-9, 2006, pages 529–543, 2006.
Info
M. Nickles. Communication structures of open multiagent systems. PhD thesis, Department of Informatics, Technical University of Munich, 2006.
Info
M. Nickles and R. Cobos. Social contexts and the probabilistic fusion and ranking of opinions: Towards a social semantics for the semantic web. In Proceedings of the Second Workshop on Uncertainty Reasoning for the Semantic Web (URSW-06). CEUR-WS, 2006.
Info
M. Nickles, A. Pease, A. C. Schalley, and D. Zaefferer. Ontologies across the disciplines. In A. C. Schalley and D. Zaefferer, editors, Ontolinguistics. How Ontological Status Shapes the Linguistic Coding of Concepts. Mouton de Gruyter, 2006.
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
Mihai Christodorescu, Johannes Kinder, Somesh Jha, Stefan Katzenbeisser, and Helmut Veith. Malware normalization. Technical Report 1539, University of Wisconsin, Madison, Wisconsin, USA, November 2005.
PDF (312 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
Achim Rettinger. Opponent-adaptive online multiagent learning - concept-recall with expert ensembles for simulated-soccer-agents. Master's thesis, University of Koblenz, Germany, October 2005.
Info
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
Johannes Kinder, Stefan Katzenbeisser, Christian Schallhart, and Helmut Veith. Detecting malicious code by model checking. In GI SIG SIDAR Conference on Detection of Intrusions and Malware & Vulnerability Assessment (DIMVA'05), volume 3548 of Lecture Notes in Computer Science, pages 174–187. Springer, July 2005.
GZipped PostScript (174 kB)
PDF (150 kB)
Info
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
N. Rinetzky, J. Bauer, T. Reps, M. Sagiv, and R. Wilhelm. A Semantics for Procedure Local Heaps and its Abstractions. In 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'05), 2005.
PDF (467 kB)
Info
Stefan Kiefer. Abstraction refinement for pushdown systems. Master's thesis, Universität Stuttgart, 2005.
GZipped PostScript (329 kB)
PDF (557 kB)
Info
Johannes Kinder. Model checking malicious code. Master's thesis, Technische Universität München, 2005.
GZipped PostScript (359 kB)
PDF (472 kB)
Info
M. Nickles and F. Fischer. Communication attitudes: A formal account of ostensible beliefs and intentions. In Third European Workshop on Multi-Agent Systems (EUMAS 2005), Brussel, Belgium, 2005.
Info
G. Weiß, M. Nickles, M. Rovatsos, and F. Fischer. Specifying the intertwining of coordination and autonomy in agent-based systems. International Journal of Network and Computer Applications, Vol.28, 2005.
Info
M. Nickles, T. Froehner, R. Cobos, and G. Weiß. Multi-source knowledge bases and ontologies with multiple individual and social viewpoints. In Proceedings of The 2005 IEEE/WIC/ACM International Conference on Web Intelligence (WI'05). IEEE Computer Society Press, 2005.
Info
F. Fischer and M. Nickles. Towards a notion of generalised statement-level trust. Technical Report FKI-249-05, Institut für Informatik, Technical University of Munich, 2005.
Info
G. Weiß, F. A. Fischer, M. Nickles, and M. Rovatsos. Operational modelling of agent autonomy: Theoretical aspects and a formal language.. In Agent-Oriented Software Engineering VI, 6th International Workshop, AOSE 2005, Utrecht, The Netherlands, July 25, 2005. Revised and Invited Papers, pages 1–15, 2005.
Info
T. Froehner, M. Nickles, G. Weiß, W. Brauer, and R. Franken. Integration of ontologies and knowledge from autonomous sources. Künstliche Intelligenz, 1/05, 2005.
Info
M. Nickles, M. Rovatsos, W. Brauer, and G. Weiß. Communication systems: A unified model of socially intelligent systems. In K. Fischer and M. Florian, editors, Socionics, Lecture Notes in Artificial Intelligence. Springer-Verlag, 2005. Invited paper.
Info
M. Nickles and G. Weiß. Multiagent systems without agents: Mirror-holons for the compilation and enactment of communication structures. In K. Fischer and M. Florian, editors, Socionics, Lecture Notes in Artificial Intelligence. Springer-Verlag, 2005. Invited paper.
Info
M. Nickles, F. Fischer, and G. Weiß. Communication attitudes: A formal approach to ostensible intentions, and individual and group opinions. In Wiebe van der Hoek and Mike Wooldridge, editors, Proceedings of the Third International Workshop on Logic and Communication in Multiagent Systems (LCMAS 2005), 2005.
Info
M. Nickles, M. Rovatsos, and G. Weiß. Formulating agent communication semantics and pragmatics as behavioral expectations. In F. Dignum, R. van Eijk, and M.-P. Huget, editors, Agent Communication Languages II, Lecture Notes in Artificial Intelligence. Springer, 2005. Invited paper.
Info
M. Nickles, M. Rovatsos, and G. Weiß. Expectation-oriented modeling. Engineering Applications of Artificial Intelligence (EAAI), 18, 2005.
Info
Heni Ben Amor and Achim Rettinger. Intelligent exploration for genetic algorithms: Using self-organizing maps in evolutionary computation. In GECCO'05: Proceedings of the 2005 Conference on Genetic and Evolutionary Computation, pages 1531–1538. ACM Press, 2005.
PDF (380 kB)
Info

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.
GZipped PostScript (93 kB)
PDF (179 kB)
Info
See www.fmi.uni-stuttgart.de ...
Conference version
N. Rinetzky, J. Bauer, T. Reps, M. Sagiv, and R. Wilhelm. A Semantics for Procedure Local Heaps and its Abstractions. Tech. Rep. 1, AVACS, Sep 2004.
PDF (443 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
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
Michael Luttenberger. Effiziente Berechnung optimaler Strategien für Paritätsspiele. Master's thesis, Universität Stuttgart, 2004. In German.
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
T. Froehner, M. Nickles, and G. Weiß. Open ontologies – The need for modeling heterogeneous knowledge. In Proceedings of the International Conference on Information and Knowledge Engineering (IKE-2004), 2004.
Info
T. Froehner, M. Nickles, and G. Weiß. Towards modeling the social layer of emergent knowledge using open ontologies. In ECAI Workshop on Agent-Mediated Knowledge Management (AMKM), pages 10–19, 2004.
Info
M. Nickles, T. Froehner, and G. Weiß. Social annotation of semantically heterogeneous knowledge. In Proceedings of the 4th International Workshop on Knowledge Markup and Semantic Annotation (SemAnnot), 2004.
Info
M. Nickles, T. Froehner, and G. Weiß. Open ontologies and open knowledge bases for modeling the social layer of the Semantic Web (poster). In The Third International Semantic Web Conference (ISCW), 2004.
Info
M. Nickles and M. Rovatsos. Towards a unified model of sociality in multiagent systems. International Journal of Computer and Information Science, 5(2):73–88, 2004.
Info
M. Nickles, M. Rovatsos, and G. Weiß, editors. Agents and Computational Autonomy. Potential, Risks, and Solutions, volume 2969 (Hot Topics) of Lecture Notes in Computer Science. Springer-Verlag, 2004.
Info
M. Nickles, M. Rovatsos, and G. Weiß. Empirical-rational semantics of agent communication. In Proceedings of the Third International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2004), pages 94–101, 2004.
Info
M. Rovatsos, M. Nickles, and G. Weiß. An empirical model of communication in multiagent systems. In F. Dignum, editor, Agent communication languages, Lecture Notes in Computer Science, Vol. 2922, pages 18–36. Springer-Verlag, 2004. Invited paper.
Info
G. Weiß, J. Duscher, M. Rovatsos, and M. Nickles. Spezifikation von Softwareautonomie. Künstliche Intelligenz (KI), 4/04, 2004.
Info
Achim Rettinger. Learning from recorded games: A scoring policy for simulated soccer agents. In Ubbo Visser, Hans-Dieter Burkhard, Patrick Doherty, and Gerhard Lakemeyer, editors, Proceedings of the ECAI 2004, 16th European Conference on Artificial Intelligence, Workshop 8: Agents in Dynamic and Real-Time Environments, pages 43–48, 2004.
Info
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
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
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
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
January 2011: Michal Terepeta and Flemming Nielson have found a mistake in the paper: Lemma 1.2 (numbering of the journal version) does not hold as stated. We will try to repair it as soon as possible.
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
January 2011: Michal Terepeta and Flemming Nielson have found a mistake in the paper: Lemma 1.2 does not hold as stated. We will try to repair it as soon as possible.
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
M. Nickles and G. Weiß. Agent-based social assessment of shared resources.. In Second International Workshop on Agents and Peer-to-Peer Computing (AP2PC-2003), pages 35–40, 2003.
Info
M. Nickles and G. Weiß. Empirical semantics of agent communication in open systems. In Proceedings of the Second International Workshop on Challenges in Open Agent Environments (Challenge), 2003.
Info
M. Nickles and G. Weiß. A framework for the social description of resources in open environments. In M. Klusch, S. Ossowski, A. Omicini, and H. Laamanen, editors, Proceedings of the 7th International Workshop on Cooperative Information Agents (CIA-2003), volume 2782 of Lecture Notes in Artificial Intelligence, pages 206–221. Springer-Verlag, 2003.
Info
M. Rovatsos, M. Nickles, and G. Weiß. Interaction is meaning: A new model for communication in open systems. In Proceedings of the Second International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2003), pages 536–543, 2003.
Info
M. Nickles, M. Rovatsos, W. Brauer, and G. Weiß. Towards a unified model of sociality in multiagent systems. In W. Dosch and R. Y. Lee, editors, Proceedings of the ACIS Fourth International Conference on Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing (SNPD'03), October 16-18, 2003, Lübeck, Germany. ACIS, 2003.
Info
G. Weiß, M. Rovatsos, and M. Nickles. Capturing Agent Autonomy in Roles and XML. In J. S. Rosenschein, T. Sandholm, M. Wooldridge, and M. Yokoo, editors, Proceedings of the Second International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS'03), Melbourne, Australia, 2003.
Info
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
M. Nickles, M. Rovatsos, and G. Weiß. A Schema for Specifying Computational Autonomy. In P. Petta, R. Tolksdorf, and F. Zambonelli, editors, Engineering Societies in the Agents World III, Third International Workshop (ESAW-2002), Revised Papers, volume 2577 of LNAI. Springer-Verlag, September 16-17 2002.
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
W. Brauer, M. Nickles, M. Rovatsos, G. Weiß, and K.F. Lorentzen. Expectation-oriented analysis and design. In M.J. Wooldridge, G. Weiß, and P. Ciancarini, editors, Agent-oriented software engineering. Proceedings of the Second International Workshop (AOSE-2001), Lecture Notes in Artificial Intelligence, Vol. 2222, pages 226–244. Springer-Verlag, 2002.
Info
K.F. Lorentzen and M. Nickles. Ordnung aus Chaos - Prolegomena zu einer Luhmann'schen Modellierung deentropisierender Strukturbildung in Multiagentensystemen. In T. Kron, editor, Luhmann modelliert. Ans"atze zur Simulation von Kommunikationssystemen. Leske & Budrich, 2002.
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
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

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.
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
J. Bauer. A Control-Flow-Analysis for Multi-Threaded Java with Security Applications. Master's thesis, Saarland University, 2001.
GZipped PostScript (216 kB)
Info
M. Nickles. SYSTEMATICS - Ein XML-basiertes Internet-Datenbanksystem für klassifikationsgestützte Sprachbeschreibungen. Technical Report CIS-Report 01-129, Centre for Information and Language Processing (CIS), University of Munich, 2001.
Info
M. Nickles. Towards a multiagent system for competitive website ratings. Technical Report FKI-243-01, Institut für Informatik, Technische Universität München, 2001.
Info
M. Nickles. Multiagent Systems for the Social Competition Among Website Ratings. In Who's Who in Recommender Systems, Proceedings of the 2001 ACM SIGIR Workshop on Recommender Systems, 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

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

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. Section 8 presents a logic for Petri nets, due to Yen, having an EXPSPACE model-checking problem. Unfortunately, Yen's paper has a mistake. For a description of the mistake and a partial correction see "On Yen's Path Logic for Petri Nets" by Faouzi and Habermehl, Workshop on Reachability Problems 2009.
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
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 ...

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

Jörg Desel and Javier Esparza. Free choice Petri nets, volume 40 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, New York, NY, USA, 1995.
PDF (11 MB)
Info
See www.cambridge.org ...
The copyright of this book lies by Cambridge University Press (CUP). I have got a verbal authorization from CUP to deposit a copy here. I have repeateadly mailed CUP to obtain an official, written permission, so far without answer. Please print only one copy of the book for your personal (noncommercial) use, and do not distribute the file further. The book can be purchased from the publisher in soft-cover. If you are interested, follow the link above.
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. 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