|
|
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. |
|
|
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. |
|
|
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. |
|
|
M. Luttenberger and M. Schlund. Convergence of Newton's Method over Commutative Semirings. Information and Computation, ?(?):??–??, To appear. |
|
2020 | |
Nathanaël Fijalkow, Stefan Kiefer, and Mahsa Shirmohammadi. Trace refinement in labelled Markov decision processes. Logical Methods in Computer Science, Volume 16, Issue 2, 2020. |
|
|
Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, Patrick Totzke, and Dominik Wojtczak. How to play in infinite MDPs (invited talk). In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, July 8-11, 2020, Saarbrücken, Germany (Virtual Conference), volume 168 of LIPIcs, pages 3:1–3:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. |
|
|
Georgina Bumpus, Christoph Haase, Stefan Kiefer, Paul-Ioan Stoienescu, and Jonathan Tanner. On the size of finite rational matrix semigroups. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, July 8-11, 2020, Saarbrücken, Germany (Virtual Conference), volume 168 of LIPIcs, pages 115:1–115:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. |
|
|
Stefan Jaax and Stefan Kiefer. On affine reachability problems. In Javier Esparza and Daniel Král', editors, 45th International Symposium on Mathematical Foundations of Computer Science, MFCS 2020, August 24-28, 2020, Prague, Czech Republic, volume 170 of LIPIcs, pages 48:1–48:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. |
|
|
Dmitry Chistikov, Stefan Kiefer, Andrzej S. Murawski, and David Purser. The big-O problem for labelled Markov chains and weighted automata. In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), volume 171 of LIPIcs, pages 41:1–41:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. |
|
|
Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Patrick Totzke. Strategy complexity of parity objectives in countable MDPs. In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), volume 171 of LIPIcs, pages 39:1–39:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. |
|
2019 | |
Stefan Kiefer and Corto Mascle. On finite monoids over nonnegative integer matrices and short killing words. In Proceedings of the 36th International Symposium on Theoretical Aspects of Computer Science (STACS), Leibniz International Proceedings in Informatics (LIPIcs), pages 43:1–43:13, 2019. |
|
|
Nikhil Balaji, Stefan Kiefer, Petr Novotný, Guillermo A. Pérez, and Mahsa Shirmohammadi. On the complexity of value iteration. In Proceedings of the 46th International Colloquium on Automata, Languages, and Programming (ICALP), Leibniz International Proceedings in Informatics (LIPIcs), pages 102:1–102:15, 2019. |
|
|
Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Patrick Totzke. Büchi objectives in countable MDPs. In Proceedings of the 46th International Colloquium on Automata, Languages, and Programming (ICALP), Leibniz International Proceedings in Informatics (LIPIcs), pages 119:1–119:14, 2019. |
|
|
Stefan Kiefer and Cas Widdershoven. Efficient analysis of unambiguous automata using matrix semigroup techniques. In Proceedings of the 44th International Symposium on Mathematical Foundations of Computer Science (MFCS), Leibniz International Proceedings in Informatics (LIPIcs), pages 82:1–82:13, 2019. |
|
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. |
|
|
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. |
|
|
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. |
|
|
Radu Grigore and Stefan Kiefer. Selective monitoring. Technical report, arXiv.org, 2018. Available at https://arxiv.org/abs/1806.06143. |
|
|
Vojtěch Forejt, Petr Jančar, Stefan Kiefer, and James Worrell. Game characterization of probabilistic bisimilarity, and applications to pushdown automata. Logical Methods in Computer Science (LMCS), 14(4), 2018. |
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
Stefan Kiefer, Ines Marusic, and James Worrell. Minimisation of multiplicity tree automata. Logical Methods in Computer Science (LMCS), 13(1), 2017. |
|
|
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. |
|
2016 | |
Javier Esparza, Pierre Ganty, Jerome Leroux, and Rupak Majumdar. Model checking population protocols. Technical report, Technical University of Munich, 2016. Submitted for publication. |
|
|
Eike Best and Javier Esparza. Existence of home states in petri nets is decidable. Inf. Process. Lett., 116(6):423–427, 2016. |
|
|
Javier Esparza and Philipp Hoffmann. Reduction rules for colored workflow nets. In FASE, pages 342–358. Springer, 2016. |
|
|
Jérôme Leroux Javier Esparza, Pierre Ganty and Rupak Majumdar. Verification of population protocols. Acta Informatica, 2016. To appear. |
|
|
Javier Esparza, Michael Luttenberger, and Maximilian Schlund. A brief history of Strahler numbers — with a preface. Technical report, Technical University of Munich, 2016. |
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
Stefan Kiefer and A. Prasad Sistla. Distinguishing hidden Markov chains. Technical report, arXiv.org, 2016. Available at https://arxiv.org/abs/1507.02314. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
2015 | |
Salomon Sickert. Converting linear temporal logic to deterministic (generalized) rabin automata. Archive of Formal Proofs, September 2015. |
|
|
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. |
|
|
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. |
|
|
Jérôme Leroux Javier Esparza, Pierre Ganty and Rupak Majumdar. Verification of population protocols. In CONCUR, 2015. |
|
|
Pierre Ganty Antoine Durand-Gasselin, Javier Esparza and Rupak Majumdar. Model checking parameterized asynchronous shared-memory systems.. In CAV, pages 192–208, 2015. |
|
|
Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, and Rupak Majumdar. Model checking parameterized asynchronous shared-memory systems. Technical report, CoRR, 2015. |
|
|
Javier Esparza and Jörg Desel. Negotiation programs. In PETRI NETS 2015, pages 157–178, 2015. |
|
|
Javier Esparza, Jan Kretinsky, and Salomon Sickert. From ltl to deterministic automata–a safraless compositional approach. Submitted, 2015. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
Christoph Haase and Stefan Kiefer. The odds of staying on budget. Technical report, arXiv.org, 2015. Available at http://arxiv.org/abs/1409.8228. |
|
|
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. |
|
|
Radu Grigore and Stefan Kiefer. Tree buffers. Technical report, arXiv.org, 2015. Available at http://arxiv.org/abs/1504.04757. |
|
|
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. |
|
|
Javier Esparza and Philipp J. Meyer. An SMT-based approach to coverability analysis. In FMCAD, pages 49–56, 2015. |
|
|
Peter Lammich and Rene Neumann. A framework for verifying depth-first search algorithms. In CPP, January 2015. |
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
Rene Neumann. Promela formalization. Archive of Formal Proofs, May 2014. Formal proof development. |
|
|
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. |
|
|
Javier Esparza, Michael Luttenberger, and Maximilian Schlund. A brief history of Strahler numbers. In LATA, pages 1–13, 2014. |
|
|
Javier Esparza and Philipp Hoffmann. Negotiation games. CoRR, abs/1405.6820, 2014. |
|
|
Javier Esparza, Michael Luttenberger, and Maximilian Schlund. FPsolve: A generic solver for fixpoint equations over semirings. In CIAA, pages 1–15, 2014. |
|
|
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. |
|
|
Javier Esparza and Jan Kretínský. From LTL to deterministic automata: A safraless compositional approach. Technical report, arxiv.org, 2014. |
|
|
Javier Esparza and Jan Kretínský. From LTL to deterministic automata: A safraless compositional approach. In CAV, pages 192–208, 2014. |
|
|
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. |
|
|
Loïg Jezequel and Javier Esparza. Message-passing algorithms for the verification of distributed protocols. In VMCAI, pages 222–241, 2014. |
|
|
Javier Esparza and Jörg Desel. On negotiation as concurrency primitive ii: Deterministic cyclic negotiations. In FOSSACS, pages 258–273, 2014. |
|
|
Javier Esparza and Jörg Desel. On negotiation as concurrency primitive ii: Deterministic cyclic negotiations. Technical report, arXiv.org, 2014. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
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. |
|
|
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. |
|
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. |
|
|
Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. Synthesizing software verifiers from proof rules. In PLDI, pages 405–416, June 2012. |
|
|
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. |
|
|
Corneliu Popeea and Andrey Rybalchenko. Compositional termination proofs for multi-threaded programs. In TACAS, March 2012. |
|
|
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. |
|
|
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. |
|
|
Javier Esparza, Pierre Ganty, and Rupak Majumdar. A perfect model for bounded verification. Technical report, arXiv.org, 2012. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
Jan Kretinsky and Javier Esparza. Deterministic automata for the (F,G)-fragment of LTL. Technical Report abs/1106.1424, arXiv.org, 2012. |
|
|
Javier Esparza, Orna Kupferman, and Moshe Vardi. Verification. In Hanbook on Automata Theory. European Mathematical Society, 2012. To appear. |
|
|
Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Proving termination of probabilistic programs using patterns. In Proceedings of CAV 2012, Berkeley, USA, 2012. |
|
|
Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Proving termination of probabilistic programs using patterns. In Proceedings of CAV 2012, Berkeley, USA, 2012. |
|
|
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. |
|
|
Javier Esparza and Christian Kern. Reactive and proactive diagnosis of distributed systems using net unfoldings. In ACSD, 2012. To appear. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
Jan Kretinsky and Javier Esparza. Deterministic automata for the (F,G)-fragment of LTL. In Madhusudan and Seshia, pages 7–22. |
|
|
Jan Kretinsky and Javier Esparza. Deterministic automata for the (F,G)-fragment of LTL. Technical Report abs/1106.1424, arXiv.org, 2012. |
|
|
Nikola Benes and Jan Kretinsky. Modal process rewrite systems. In Roychoudhury and D'Souza, pages 120–135. |
|
|
Nikola Benes and Jan Kretinsky. Modal process rewrite systems. Technical report FIMU-RS-2012-02, Faculty of Informatics, Masaryk University, Brno, 2012. |
|
|
Andreas Gaiser, Jan Kretinsky, and Javier Esparza. Rabinizer: Small deterministic automata for LTL(F, G). In Chakraborty and Mukund, pages 72–76. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
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. |
|
|
Michael Luttenberger. An extension of Parikh's theorem beyond idempotence. Technical report, Technische Universität München, Institut für Informatik, December 2011. |
|
|
Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. Solving recursion-free horn clauses over LI+UIF. In APLAS, December 2011. |
|
|
Javier Esparza and Andreas Gaiser. Probabilistic abstractions with arbitrary domains. In Proceedings of the 18th International Static Analysis Symposium (SAS), Venice, Italy, September 2011. |
|
|
Javier Esparza and Andreas Gaiser. Probabilistic abstractions with arbitrary domains. In Proceedings of the 18th International Static Analysis Symposium (SAS), Venice, Italy, September 2011. |
|
|
Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. Threader: A constraint-based verifier for multi-threaded programs. In CAV, pages 412–417, July 2011. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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). |
|
|
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). |
|
|
Stefan Haar, Christian Kern, and Stefan Schwoon. Computing the reveals relation in occurrence nets. In GandALF, pages 31–44, 2011. |
|
|
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. |
|
|
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. |
|
|
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Derivation tree analysis for accelerated fixed-point computation. Theoretical Computer Science, 412(28):3226–3241, 2011. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
Jan Kretinsky. Probabilistic timed systems with non-determinism. PhD Thesis proposal, Masaryk University, Brno, Dept. of Computer Science, 2011. |
|
|
Tomas Brazdil, Jan Krcal, Jan Kretinsky, and Vojtech Rehak. Fixed-delay events in generalized semi-markov processes revisited. In CONCUR, pages 140–155, 2011. |
|
|
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. |
|
|
Nikola Benes, Ivana Cerna, and Jan Kretinsky. Modal transition systems: Composition and LTL model checking. In Bultan and Hsiung, pages 228–242. |
|
|
Nikola Benes, Jan Kretinsky, Kim G. Larsen, Mikael H. Moller, and Jiri Srba. Parametric modal transition systems. In Bultan and Hsiung, pages 275–289. |
|
|
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. |
|
|
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. |
|
|
Javier Esparza and Michael Luttenberger. Solving fixed-point equations by derivation tree analysis. In CALCO, pages 19–35, 2011. |
|
|
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. |
|
|
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. |
|
|
Rene Neumann. Development of a concurrent language featuring a type system based on boolean implications. Master's thesis, Technische Universität München, 2011. |
|
|
Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. Predicate abstraction and refinement for verifying multi-threaded programs. In POPL, pages 331–344, January 2011. |
|
|
Ruslan Ledesma-Garza. Verification of Temporal Properties of Functional Programs. Master's thesis, Saarland University, 2011. |
|
|
Ranjit Jhala, Rupak Majumdar, and Andrey Rybalchenko. Hmc: Verifying functional programs using abstract interpreters. In Gopalakrishnan and Qadeer, pages 470–485. |
|
|
Andrey Rybalchenko. Towards automatic synthesis of software verification tools. In Schneider-Kamp and Hanus, pages 3–4. |
|
|
Andreas Podelski and Andrey Rybalchenko. Transition invariants and transition predicate abstraction for program termination. In Abdulla and Leino, pages 3–10. |
|
|
Nuno P. Lopes and Andrey Rybalchenko. Distributed and predictable software model checking. In Jhala and Schmidt, pages 340–355. |
|
|
Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Proving program termination. Commun. ACM, 54(5):88–98, 2011. |
|
|
J. Esparza, M. Leucker, and M. Schlund. Learning workflow Petri nets. Fundamenta Informaticae, 113(3-4):205–228, 2011. |
|
2010 | |
Javier Esparza and Andreas Gaiser. Probabilistic abstractions with arbitrary domains. Technical report, Technische Universität München, Institut für Informatik, December 2010. |
|
|
Javier Esparza and Andreas Gaiser. Probabilistic abstractions with arbitrary domains. Technical report, Technische Universität München, Institut für Informatik, December 2010. |
|
|
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. |
|
|
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Newtonian program analysis. Journal of the ACM, 57(6):33:1–33:47, October 2010. |
|
|
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. |
|
|
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. |
|
|
Rene Neumann. Functional binomial queues. Archive of Formal Proofs, October 2010. Formal proof development. |
|
|
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. |
|
|
Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. Non-monotonic refinement of control abstraction for concurrent programs. In ATVA, pages 188–202, September 2010. |
|
|
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. |
|
|
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. |
|
|
Corneliu Popeea and Wei-Ngan Chin. Dual analysis for proving safety and finding bugs. In SAC, pages 2137–2143, March 2010. |
|
|
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. |
|
|
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. |
|
|
J. Esparza. A false history of true concurrency: from Petri to tools. In Proc. of the 17th International SPIN Workshop, 2010. |
|
|
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. |
|
|
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. |
|
|
Christian Kern. Automatic error correction of java programs. In AlgoSyn, page 155, 2010. |
|
|
Christian Kern and Javier Esparza. Automatic error correction of java programs. In FMICS, pages 67–81, 2010. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
Jan Kretinsky. Modal transition systems. Master's thesis, Masaryk University, Brno, Dept. of Mathematics, 2010. |
|
|
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. |
|
|
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. |
|
|
Nikola Benes and Jan Kretinsky. Process algebra for modal transition systemses. In MEMICS, pages 9–18, 2010. |
|
|
Nikola Benes and Jan Kretinsky. Process algebra for modal transition systemses. Technical report FIMU-RS-2010-11, Faculty of Informatics, Masaryk University, Brno, 2010. |
|
|
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. |
|
|
Michael Luttenberger. Solving systems of polynomial equations: A generalization of newton's method. PhD thesis, Technische Universität München, 2010. |
|
|
Chih-Hong Cheng, Christian Buckl, Michael Luttenberger, and Alois Knoll. Gavs: Game arena visualization and synthesis. In ATVA, pages 347–352, 2010. |
|
|
Javier Esparza, Pierre Ganty, Stefan Kiefer, and Michael Luttenberger. Parikh's theorem: A simple and direct construction. CoRR, abs/1006.3825, 2010. |
|
|
Andrey Rybalchenko. Constraint solving for program verification: Theory and practice by example. In Touili et al., pages 57–71. |
|
|
Boris Köpf and Andrey Rybalchenko. Approximation and randomization for quantitative information-flow analysis. In CSF, pages 3–14. |
|
|
Andrey Rybalchenko. Constraint solving for program verification: Theory and practice by example. In Dawar and Veith, page 51. |
|
|
Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács, and Andrey Rybalchenko. Aligators for arrays (tool paper). In Fermüller and Voronkov, pages 348–356. |
|
|
Alexander Malkis, Andreas Podelski, and Andrey Rybalchenko. Thread-modular counterexample-guided abstraction refinement. In Cousot and Martel, pages 356–372. |
|
|
Andrey Rybalchenko and Viorica Sofronie-Stokkermans. Constraint solving for interpolation. J. Symb. Comput., 45(11):1212–1233, 2010. |
|
|
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. |
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
Stefan Kiefer. Solving systems of positive polynomial equations. PhD thesis, Technische Universität München, 2009. |
|
|
Jan Kretinsky. Fundamental properties of probabilistic branching-time logics. Master's thesis, Masaryk University, Brno, Dept. of Computer Science, 2009. |
|
|
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. |
|
|
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. |
|
|
Nikola Benes, Jan Kretinsky, Kim Guldstrand Larsen, and Jiri Srba. On determinism in modal transition systems. Theor. Comput. Sci., 410(41):4026–4043, 2009. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
Andreas Gaiser and Stefan Schwoon. Comparison of algorithms for checking emptiness on Büchi automata. Technical Report 0910.3766, Computing Research Repository, 2009. |
|
|
Dejvuth Suwimonteerabuth. Reachability in pushdown systems: Algorithms and applications. PhD thesis, Technische Universität München, 2009. |
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
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. |
|
|
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. |
|
|
Tomas Brazdil, Vojtech Forejt, Jan Kretinsky, and Antonin Kucera. The satisfiability problem for probabilistic CTL. In LICS, pages 391–402, 2008. |
|
|
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. |
|
|
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. |
|
|
Javier Esparza, Pradeep Kanade, and Stefan Schwoon. A negative result on depth-first unfoldings. Software Tools for Technology Transfer, 10(2):161–166, 2008. |
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
J. Bauer and Reinhard Wilhelm. Static Analysis of Dynamic Communication Systems. In 14th International Static Analysis Symposium, volume 4634. Springer, 2007. |
|
|
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. |
|
|
Thomas Reps, Mooly Sagiv, and J. Bauer. An appreciation of the work of reinhard wilhelm. In Festschrift, pages 1–11. |
|
|
Christian Kern, Mohammad Khaleghi, Stefan Kugele, Christian Schallhart, Michael Tautschnig, and Andreas Weis. Sat7 engineering a modular sat-solver, 2007. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
M. Nickles. Social acquisition of ontologies from communication processes. Journal of Applied Ontology, special issue "Formal Ontologies for Communicating Agents", 2007. |
|
|
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. |
|
|
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. |
|
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. |
|
|
Andreas Holzer. Description Languages for Malicious Software. Master's thesis, Technische Universität München, November 2006. |
|
|
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. |
|
|
Stefan Kugele. Efficient Solving of Combinatorial Problems using SAT-Solvers. Master's thesis, Technische Universität München, October 2006. |
|
|
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. |
|
|
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. |
|
|
J. Esparza, P. Jančar, and A. Miller. On the complexity of consistency and complete state coding. Technical report, University of Stuttgart, July 2006. |
|
|
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. |
|
|
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. |
|
|
J. Bauer and R. Wilhelm. Analysis of Dynamic Communicating Systems by Hierarchical Abstraction. Seminar proceedings 06081, Dagstuhl, Feb 2006. |
|
|
Michael Tautschnig. Development of a tool to solve mixed logical/linear constraint problems. Master's thesis, Technische Universität München, February 2006. |
|
|
A. Bouajjani and J. Esparza. Rewriting models of boolean programs. In Proceedings of RTA 2006, Seattle, USA, 2006. |
|
|
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. |
|
|
G. Delzanno, J. Esparza, and J. Srba. Monotonic set-extended prefix rewriting and verification of recursive ping-pong protocols. Technical report, BRICS, 2006. |
|
|
Javier Esparza, Antonín Kučera, and Richard Mayr. Model checking probabilistic pushdown automata. Logical Methods in Computer Science, 2006. |
|
|
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. |
|
|
J. Bauer. Analysis of Communication Topologies by Partner Abstraction. PhD thesis, Universität des Saarlandes, 2006. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
M. Nickles. Communication structures of open multiagent systems. PhD thesis, Department of Informatics, Technical University of Munich, 2006. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
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. |
|
|
Mihai Christodorescu, Johannes Kinder, Somesh Jha, Stefan Katzenbeisser, and Helmut Veith. Malware normalization. Technical Report 1539, University of Wisconsin, Madison, Wisconsin, USA, November 2005. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
Ahmed Bouajjani, Javier Esparza, and Tayssir Touili. Reachability analysis of synchronized PA-systems. Electronic Notes in Theoretical Computer Science, 138(3):153–178, 2005. |
|
|
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. |
|
|
Stefan Kiefer. Abstraction refinement for pushdown systems. Master's thesis, Universität Stuttgart, 2005. |
|
|
Johannes Kinder. Model checking malicious code. Master's thesis, Technische Universität München, 2005. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
M. Nickles, M. Rovatsos, and G. Weiß. Expectation-oriented modeling. Engineering Applications of Artificial Intelligence (EAAI), 18, 2005. |
|
|
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. |
|
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. |
|
|
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. |
|
|
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. |
|
|
Markus Holzer and Stefan Schwoon. Assembling molecules in Atomix is hard. Theoretical Computer Science, 303(3):447–462, February 2004. |
|
|
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. |
|
|
Ahmed Bouajjani, Javier Esparza, and Tayssir Touili. Reachability analysis of synchronized PA-systems. In Proceedings of Infinity 2004, 2004. |
|
|
Javier Esparza, Antonín Kučera, and Richard Mayr. Model checking probabilistic pushdown automata. In LICS 2004. IEEE Computer Society, 2004. |
|
|
Javier Esparza, Antonín Kučera, and Richard Mayr. Model checking probabilistic pushdown automata. Technical report, Faculty of Informatics, Masaryk University, Brno, 2004. |
|
|
J. Esparza. A polynomial-time algorithm for checking consistency of free-choice signal transition graphs. Fundamenta Informaticae, 62(2):197–220, 2004. |
|
|
Michael Luttenberger. Effiziente Berechnung optimaler Strategien für Paritätsspiele. Master's thesis, Universität Stuttgart, 2004. In German. |
|
|
Matthias Hopf, Michael Luttenberger, and Thomas Ertl. Hierarchical splatting of scattered 4d data. IEEE Computer Graphics and Applications, 24(04):64–72, 2004. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
G. Weiß, J. Duscher, M. Rovatsos, and M. Nickles. Spezifikation von Softwareautonomie. Künstliche Intelligenz (KI), 4/04, 2004. |
|
|
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. |
|
|
Dejvuth Suwimonteerabuth. Verifying Java bytecode with the Moped model checker. Master's thesis, Universität Stuttgart, 2004. |
|
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. |
|
|
Stefan Kiefer. Die Menge der virtuellen Verbindungen im Spiel Hex ist PSPACE-vollständig. Studienarbeit Nr. 1887, Universität Stuttgart, Juli 2003. In German. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
A. Kučera and J. Esparza. A logical viewpoint on process-algebraic quotients. Journal of Logic and Computation, 13(6):863–880, 2003. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
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. |
|
|
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. |
|
|
J. Esparza and C. Lakos, editors. Applications and theory of petri nets 2002, volume 2360 of Lecture Notes in Computer Science. Springer Verlag, 2002. |
|
|
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. |
|
|
J. Esparza, S. Römer, and W. Vogler. An improvement of McMillan's unfolding algorithm. Formal Methods in System Design, 20:285–310, 2002. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
Stefan Schwoon. Model-checking pushdown systems. PhD thesis, Technische Universität München, 2002. |
|
|
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. |
|
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. |
|
|
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. |
|
|
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. |
|
|
Markus Holzer and Stefan Schwoon. Assembling molecules in Atomix is hard. Technical Report TUM-I0101, Technische Universität München, May 2001. |
|
|
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. |
|
|
J. Esparza and C. Schröter. Unfolding based algorithms for the reachability problem. Fundamenta Informaticae, 47(3–4):231–245, 2001. |
|
|
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. |
|
|
J. Bauer. A Control-Flow-Analysis for Multi-Threaded Java with Security Applications. Master's thesis, Saarland University, 2001. |
|
|
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. |
|
|
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. |
|
|
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. |
|
2000 | |
Javier Esparza, Peter Rossmanith, and Stefan Schwoon. A uniform framework for problems on context-free grammars. EATCS Bulletin, 72:169–177, October 2000. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
P. Jančar, J. Esparza, and F. Moller. Petri nets and regular behaviours. Journal of Computer and System Sciences, 59(3):476–503, 1999. |
|
|
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. |
|
|
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. |
|
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. |
|
J. Esparza. Reachability in live and safe free-choice Petri nets is  -complete. Theoretical Computer Science, 198(1–2):211–224, 1998. |
|
|
Stefan Schwoon. Übersetzung von SDL-Spezifikationen in Petri-Netze. Master's thesis, Universität Hildesheim, 1998. In German. |
|
1997 | |
O. Burkart and J. Esparza. More infinite results. Bulletin of the EATCS 62 (Concurrency Column), 1997. |
|
|
E. Best, J. Esparza, B. Grahlmann, S. Melzer, S. Römer, and F. Wallner. The PEP verification system. In FEmSys'97, 1997. Tool presentation. |
|
|
A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In Proc. of CONCUR'97, 1997. |
|
|
J. Esparza and S. Melzer. Model checking LTL using constraint programming. In Proc. of Application and Theory of Petri Nets'97, 1997. |
|
|
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. |
|
|
J. Esparza. Petri nets, commutative context-free grammars, and basic parallel processes. Fundamenta Informaticae, 31:13–26, 1997. |
|
|
J. Esparza. Decidability of model-checking for infinite-state concurrent systems. Acta Informatica, 34:85–107, 1997. |
|
1996 | |
O. Burkart and J. Esparza. More infinite results. Electronic Notes in Theoretical Computer Science, 6, 1996. |
|
|
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. |
|
|
J. Esparza and G. Bruns. Trapping mutual exclusion in the box calculus. Theoretical Computer Science, 153(1):95–128, 1996. |
|
|
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. |
|
|
J. Esparza. More infinite results. In Proc. of INFINITY'96, Research Report MIP-9614, University of Passau, 1996. |
|
|
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. |
|
|
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. |
|
|
S. Melzer and J. Esparza. Checking system properties via integer programming. In Proc. of ESOP'96, Lecture Notes in Computer Science. Springer-Verlag, 1996. |
|
|
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. |
|
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. |
|
|
J. Desel and J. Esparza. Shortest paths in reachability graphs. Journal of Computer and System Sciences, 51(2):314–323, 1995. |
|
|
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. |
|
|
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. |
|
|
P. Jancar and J. Esparza. Deciding finiteness of Petri nets up to bisimulation. SFB-Bericht Nr. 342/23/95A, TU München, 1995. |
|
|
Allan Cheng, Javier Esparza, and Jens Palsberg. Complexity results for 1-safe nets. Theoretical Computer Science, 147(1&2):117–136, 1995. |
|
1994 | |
J. Esparza and M. Nielsen. Decibility issues for Petri nets - a survey. Journal of Informatik Processing and Cybernetics, 30(3):143–160, 1994. |
|
|
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. |
|
|
J. Esparza. Reduction and synthesis of live and bounded free choice Petri nets. Information and Computation, 114(1):50–87, 1994. |
|
|
J. Esparza. Model checking using net unfoldings. Science of Computer Programming, 23:151–195, 1994. |
|
|
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. |
|
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. |
|
|
J. Desel and J. Esparza. Reachability in cyclic extended free-choice systems. Theoretical Computer Science, 114:93–118, 1993. |
|
|
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. |
|
1992 | |
E. Best, J. Desel, and J. Esparza. Traps characterise home states in free choice systems. Theoretical Computer Science, 101:161–176, 1992. |
|
|
J. Esparza and M. Silva. A polynomial time algorithm to decide liveness of bounded free choice nets. Theoretical Computer Science, 102:185–205, 1992. |
|
|
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. |
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
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. |
|
|
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. |
|
|
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. |
|
|
|
Contact
