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 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