Models of Computation |
|
Description |
The Models of Computation (MoC) group is committed to studying techniques, tools, and frameworks for modelling and reasoning about the correctness and reliability of software and systems. We strive to make a meaningful impact on the design, implementation, and maintenance of complex and critical systems by enabling better understanding and confidence in their behavior. For this, the MoC group applies techniques from and contributes to the fields of verification, program analysis, logic and automata theory. |
Group members |
|
Publications |
2020
Multi-linear strategy extraction for QBF expansion proofs via local soundness
Matthias Schlaipfer, Friedrich Slivovsky, Georg Weissenbacher, Florian Zuleger. SAT 2020: Theory and applications of satisfiability testing - SAT 2020, pages 429-446, 2020. [pdf] [doi]
Thread-modular counter abstraction for parameterized program safety
Thomas Pani, Georg Weissenbacher, Florian Zuleger. Formal methods in computer-aided design, pages 67-76, 2020. [pdf] [doi]
Beyond symbolic heaps: Deciding separation logic with inductive definitions
Jens Katelaan, Florian Zuleger. 23rd international conference on logic for programming, artificial intelligence and reasoning, alicante, spain, volume 73, pages 390-408, 2020. [pdf] [doi]
Eliminating message counters in threshold automata
Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger. Automated technology for verification and analysis - 18th symposium, 2020, hanoi, vietnam, volume 12302, pages 196-212, 2020. [pdf] [doi]
The polynomial complexity of vector addition systems with states
Florian Zuleger. Foundations of software science and computation structures - 23rd international conference, dublin, ireland, volume 12077, pages 622-641, 2020. [pdf] [doi] 2019
Verifying safety of synchronous fault-tolerant algorithms by bounded model checking
Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger. International conference on tools and algorithms for the construction and analysis of systems, pages 357-374, 2019. [pdf]
Effective entailment checking for separation logic with inductive definitions
Jens Katelaan, Christoph Matheja, Florian Zuleger. 25th international conference, TACAS 2019, pages 319-336, 2019. [pdf]
SL-COMP: Competition of solvers for separation logic
Mihaela Sighireanu, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger, 25th international conference, TACAS 2019, pages 116-132, 2019. [pdf] 2018
Parameterized model checking of synchronous distributed algorithms by abstraction
Benjamin Aminof, Sasha Rubin, Ilina Stoilkovska, Josef Widder, Florian Zuleger. VMCAI, pages 1-24, 2018. [pdf] [doi]
Parameterized model checking of synchronous distributed algorithms by abstraction
Benjamin Aminof, Ilina Stoilkovska, Sasha Rubin, Josef Widder, Florian Zuleger. Verification, model checking, and abstract interpretation - 19th international conference, VMCAI 2018, los angeles, CA, USA, january 7-9, 2018, proceedings, pages 1-24, 2018. [pdf] [doi]
From shapes to amortized complexity
Tomas Fiedor, Lukas Holik, Adam Rogalewicz, Moritz Sinn, Tomás Vojnar, Florian Zuleger. Verification, model checking, and abstract interpretation - 19th international conference, VMCAI 2018, los angeles, CA, USA, january 7-9, 2018, proceedings, pages 205-225, 2018. [pdf] [doi]
Using loop bound analysis for invariant generation
Pavel Čadek, Clemens Danninger, Moritz Sinn, Florian Zuleger. Formal methods in computer-aided design, pages 1-9, 2018. [pdf] [doi]
Rely-guarantee reasoning for automated bound analysis of lock-free algorithms
Thomas Pani, Georg Weissenbacher, Florian Zuleger. Formal methods in computer-aided design, pages 1-9, 2018. [pdf] [doi]
Inductive termination proofs with transition invariants and their relationship to the size-change abstraction
Florian Zuleger. Static analysis - 25th international symposium, SAS 2018, freiburg, germany, august 29-31, 2018, proceedings, pages 423-444, 2018. [pdf] [doi]
Efficient algorithms for asymptotic bounds on termination time in VASS
Tomas Brazdil, Krishnendu Chatterjee, Antonin Kucera, Peter Novotny, Dominik Velan, Florian Zuleger. Proceedings of the 33rd annual ACM/IEEE symposium on logic in computer science, LICS 2018, oxford, UK, july 09-12, 2018, pages 185-194, 2018. [pdf] [doi]
Automated clustering and program repair for introductory programming assignments
Ivan Radicek, Sumit Gulwani, Florian Zuleger. Proceedings of the 39th ACM SIGPLAN conference on programming language design and implementation, PLDI 2018, philadelphia, PA, USA, june 18-22, 2018, pages 465-480, 2018. [pdf] [doi]
Monadic refinements for relational cost analysis
Ivan Radicek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Florian Zuleger. Proceedings of the ACM on programming languages, volume New York, NY, USA, pages 1-32, 2018. [pdf] [doi] 2017
Empirical software metrics for benchmarking of verification tools
Yulia Demyanova, Thomas Pani, Helmut Veith, Florian Zuleger. Formal Methods in System Design, volume 50, pages 289-316, 2017. [doi]
On the automated verification of web applications with embedded SQL
Itzhaky Shachar, Tomer Kotek, Noam Rinetzky, Mooly Sagiv, Orr Tamir, Helmut Veith, Florian Zuleger. 20th international conference on database theory, ICDT 2017, pages 1-18, 2017.
Complexity and resource bound analysis of imperative programs using difference constraints
Moritz Sinn, Helmut Veith, Florian Zuleger. Journal of Automated Reasoning, volume 59, pages 3-45, 2017.
Automata and program analysis
Laure Daviaud, Thomas Colcombet, Florian Zuleger. Fundamentals of computation theory - 21st international symposium, FCT 2017, pages 3-10, 2017.
Systematic predicate abstraction using variable roles
Yulia Demyanova, Philipp Rümmer, Florian Zuleger. NASA formal methods - 9th international symposium, NFM 2017, pages 265-281, 2017.
Unified reasoning about robustness properties of symbolic-heap separation logic
Jens Katelaan, Christina Jansen, Florian Zuleger, Christoph Matheja, Thomas Noll. Programming languages and systems - 26th european symposium on programming, pages 611-638, 2017. [doi] 2016
Prompt alternating-time epistemic logics
Benjamin Aminof, Aniello Murano, Sasha Rubin, Florian Zuleger. KR, pages 258-267, 2016.
Monadic second order finite satisfiability and unbounded tree-width
Tomer Kotek, Helmut Veith, Florian Zuleger. CSL, pages 1-20, 2016.
Automatic verification of multi-agent systems in parameterised grid-environments
Benjamin Aminof, Aniello Murano, Sasha Rubin, Florian Zuleger. AAMAS, pages 1190-1199, 2016. 2015
Loop patterns in c programs
Thomas Pani, Helmut Veith, Florian Zuleger. ECEASST, volume 72, 2015. [pdf]
On the expressive power of communication primitives in parameterised systems
Benjamin Aminof, Sasha Rubin, Florian Zuleger. LPAR, pages 313-328, 2015. [doi]
Difference constraints: An adequate abstraction for complexity analysis of imperative programs
Moritz Sinn, Helmut Veith, Florian Zuleger. FMCAD, pages 144-151, 2015.
Empirical software metrics for benchmarking of verification tools
Yulia Demyanova, Thomas Pani, Helmut Veith, Florian Zuleger. CAV, pages 561-579, 2015. [doi]
Asymptotically precise ranking functions for deterministic size-change systems
Florian Zuleger. CSR, pages 426-442, 2015. [doi]
Liveness of parameterized timed networks
Benjamin Aminof, Sasha Rubin, Francesco Spegni, Florian Zuleger. ICALP, volume 9135, pages 375-387, 2015. [doi]
Extending ALCQIO with trees
Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger. LICS 2015, pages 511-522, 2015. [pdf] [doi]
Verification of asynchronous mobile-robots in partially-known environments
Benjamin Aminof, Aniello Murano, Sasha Rubin, Florian Zuleger. PRIMA, pages 185-200, 2015. [doi] 2014
Shape and content: Incorporating domain knowledge into shape analysis
Diego Calvanese, Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger. International workshop on description logics, 2014. [pdf]
Shape and content - a database-theoretic perspective on the analysis of data structures
Diego Calvanese, Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger. IFM, pages 3-17, 2014. [doi]
Size-change abstraction and max-plus automata
Thomas Colcombet, Laure Daviaud, Florian Zuleger. MFCS, pages 208-219, 2014. [doi]
A simple and scalable static analysis for bound analysis and amortized complexity analysis
Moritz Sinn, Florian Zuleger, Helmut Veith. CAV, pages 745-761, 2014. [doi]
Feedback generation for performance problems in introductory programming assignments
Sumit Gulwani, Ivan Radicek, Florian Zuleger. FSE, pages 41-51, 2014. [doi]
Towards a description logic for program analysis: Extending ALCQIO with reachability
Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger. International workshop on description logics, 2014. [pdf] 2013
On the concept of variable roles and its use in software analysis
Yulia Demyanova, Helmut Veith, Florian Zuleger. FMCAD, pages 226-230, 2013. [pdf]
Ramsey vs. Lexicographic termination proving
Byron Cook, Abigail See, Florian Zuleger. Tools and algorithms for the construction and analysis of systems, pages 47-61, 2013. [doi] 2011
Bound analysis of imperative programs with the size-change abstraction
Florian Zuleger, Moritz Sinn, Sumit Gulwani, Helmut Veith. Lecture notes in computer science, pages 280-297, 2011. [doi] 2010
The reachability-bound problem
Sumit Gulwani, Florian Zuleger. PLDI'10 proceedings of teh ACM SIGPLAN conference on programming language design and implementation, pages 292-304, 2010. [doi] |