|
|
|
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. |
|
|
Tewodros Beyene, Corneliu Popeea, and Andrey Rybalchenko. Solving existentially quantified Horn clauses. In CAV, July 2013. |
|
|
Corneliu Popeea and Wei-Ngan Chin. Dual analysis for proving safety and finding bugs. Sci. Comput. Program., 78(4):390–411, April 2013. |
|
|
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. |
|
|
Corneliu Popeea and Andrey Rybalchenko. Threader: A verifier for multi-threaded programs - (competition contribution). In TACAS, pages 633–636, March 2013. |
|
|
Javier Esparza, Loïg Jezequel, and Stefan Schwoon. Computation of summaries using net unfoldings. In FSTTCS, pages 225–236, 2013. |
|
|
Javier Esparza and Jörg Desel. On negotiation as concurrency primitive. In CONCUR, 2013. |
|
|
Javier Esparza and Jörg Desel. On negotiation as concurrency primitive. Technical report, arXiv.org, 2013. |
|
|
Javier Esparza, Pierre Ganty, and Rupak Majumdar. Parameterized verification of asynchronous shared-memory systems. In CAV, pages 124–140, 2013. |
|
|
Javier Esparza, Pierre Ganty, and Rupak Majumdar. Parameterized verification of asynchronous shared-memory systems. Technical report, arXiv.org, 2013. |
|
|
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. |
|
|
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. |
|
|
Stefan Kiefer. BPA bisimilarity is EXPTIME-hard. Information Processing Letters (IPL), 113(4):101–106, 2013. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
Jan Kretinsky and Salomon Sickert. On refinements of Boolean and parametric modal transition systems. In Liu et al., pages 213–230. |
|
|
Jan Kretinsky and Salomon Sickert. On refinements of Boolean and parametric modal transition systems. Technical Report abs/1304.5278, arXiv.org, 2013. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
Holger Hermanns, Jan Krcal, and Jan Kretinsky. Compositional verification and optimization of interactive Markov chains. In D'Argenio and Melgratti, pages 364–379. |
|
|
Holger Hermanns, Jan Krcal, and Jan Kretinsky. Compositional verification and optimization of interactive Markov chains. Technical Report abs/1305.7332, arXiv.org, 2013. |
|
|
Jan Kretinsky and Salomon Sickert. MoTraS: A tool for modal transition systems and their extensions. In Hung and Ogawa, pages 487–491. |
|
Jan Kretinsky and Ruslan Ledesma-Garza. Rabinizer 2: Small deterministic automata for LTL GU. In Hung and Ogawa, pages 446–450. |
|
|
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. |
|
|
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. |
|
|
|
Contact
