Note: This is an archvied version of our old webpage. Some links might be broken. The current one can be found here.
I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Publications in 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