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 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 archive.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 archive.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 archive.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 ...
Journal version
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 ...