70 citations · 123 across the 26 of their papers we have counts for
33 papers
A Cost-Aware Probability Monad for Liquid Haskell
Matthias Hetzenberger, Georg Moser, Florian Zuleger
Probabilistic algorithms and data structures are widely used to obtain favourable expected performance guarantees. While their mathematical analysis is often well understood, mecha…
Automated Amortised Analysis of Skew Heaps and Leftist Heaps (Extended Version)
Armin Walch, Georg Moser, Berry Schoenmakers +1
We study the fully automated amortised analysis of purely functional data structures like skew heaps, as well as weight- and rank-biased leftist heaps. For that we generalise earli…
Regular Grammars as Effective Representations of Recognizable Sets of Series-Parallel Graphs
Marius Bozga, Radu Iosif, Florian Zuleger
Series-parallel (SP) graphs are binary edge-labeled graphs with a designated source and target vertex, built using serial and parallel composition. A set of graphs is recognizable…
To Zip Through the Cost Analysis of Probabilistic Programs
Matthias Hetzenberger, Georg Moser, Florian Zuleger
Probabilistic programming and the formal analysis of probabilistic algorithms are active areas of research, driven by the widespread use of randomness to improve performance. While…
Regular Grammars for Sets of Graphs of Tree-Width 2
Marius Bozga, Radu Iosif, Florian Zuleger
Regular word grammars are restricted context-free grammars that define all the recognizable languages of words. This paper generalizes regular grammars from words to certain classe…
Deciding Boolean Separation Logic via Small Models (Technical Report)
Tomáš Dacík, Adam Rogalewicz, Tomáš Vojnar +1
We present a novel decision procedure for a fragment of separation logic (SL) with arbitrary nesting of separating conjunctions with boolean conjunctions, disjunctions, and guarded…
Tree-Verifiable Graph Grammars
Mark Chimes, Radu Iosif, Florian Zuleger
Hyperedge-Replacement grammars (HR) have been introduced by Courcelle in order to extend the notion of context-free sets from words and trees to graphs of bounded tree-width. While…
Effective MSO-Definability for Tree-width Bounded Models of an Inductive Separation Logic of Relations
Lucas Bueri, Radu Iosif, Florian Zuleger
A class of graph languages is definable in Monadic Second-Order logic (MSO) if and only if it consists of sets of models of MSO formulæ. If, moreover, there is a computable bound o…
The Treewidth Boundedness Problem for an Inductive Separation Logic of Relations
Marius Bozga, Lucas Bueri, Radu Iosif +1
The treewidth boundedness problem for a logic asks for the existence of an upper bound on the treewidth of the models of a given formula in that logic. This problem is found to be…
Characterizations of Monadic Second Order Definable Context-Free Sets of Graphs
Radu Iosif, Florian Zuleger
We give a characterization of the sets of graphs that are both definable in Counting Monadic Second Order Logic (CMSO) and context-free, i.e., least solutions of Hyperedge-Replacem…
Parameterized Model-checking of Discrete-Timed Networks and Symmetric-Broadcast Systems
Benjamin Aminof, Sasha Rubin, Francesco Spegni +1
We study the complexity of the model-checking problem for parameterized discrete-timed systems with arbitrarily many anonymous and identical processes, with and without a distingui…
Expressiveness Results for an Inductive Logic of Separated Relations
Radu Iosif, Florian Zuleger
In this paper we study a Separation Logic of Relations (SLR) and compare its expressiveness to (Monadic)Second Order Logic (M)SO. SLR is based on the well-known Symbolic Heap fragm…
Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Version)
Florian Sextl, Adam Rogalewicz, Tomáš Vojnar +1
Biabduction-based shape analysis is a compositional verification and analysis technique that can prove memory safety in the presence of complex, linked data structures. Despite its…
On the Expressiveness of a Logic of Separated Relations
Radu Iosif, Florian Zuleger
We compare the model-theoretic expressiveness of the existential fragment of Separation Logic over unrestricted relational signatures (SLR) -- with only separating conjunction as l…
Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
Lorenz Leutgeb, Georg Moser, Florian Zuleger
In this paper, we present the first fully-automated expected amortised cost analysis of self-adjusting data structures, that is, of randomised splay trees, randomised splay heaps a…
Low-Level Bi-Abduction
Lukáš Holík, Petr Peringer, Adam Rogalewicz +3
The paper proposes a new static analysis designed to handle open programs, i.e., fragments of programs, with dynamic pointer-linked data structures - in particular, various kinds o…
Type-Based Analysis of Logarithmic Amortised Complexity
Martin Hofmann, Lorenz Leutgeb, Georg Moser +2
We introduce a novel amortised resource analysis couched in a type-and-effect system. Our analysis is formulated in terms of the physicist's method of amortised analysis, and is po…
Strong-Separation Logic
Jens Pagel, Florian Zuleger
Most automated verifiers for separation logic target the symbolic-heap fragment, disallowing both the magic-wand operator and the application of classical Boolean operators to spat…
The Polynomial Complexity of Vector Addition Systems with States
Florian Zuleger
Vector addition systems are an important model in theoretical computer science and have been used in a variety of areas. In this paper, we consider vector addition systems with sta…
Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS
Tomáš Brázdil, Krishnendu Chatterjee, Antonín Kučera +3
Vector Addition Systems with States (VASS) provide a well-known and fundamental model for the analysis of concurrent processes, parameterized systems, and are also used as abstract…
Ranking Functions for Vector Addition Systems
Florian Zuleger
Vector addition systems are an important model in theoretical computer science and have been used for the analysis of systems in a variety of areas. Termination is a crucial proper…
Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic
Christina Jansen, Jens Katelaan, Christoph Matheja +2
We introduce heap automata, a formalism for automatic reasoning about robustness properties of the symbolic heap fragment of separation logic with user-defined inductive predicates…
On the automated verification of web applications with embedded SQL
Shachar Itzhaky, Tomer Kotek, Noam Rinetzky +4
A large number of web applications is based on a relational database together with a program, typically a script, that enables the user to interact with the database through embedd…
Liveness of Parameterized Timed Networks
Benjamin Aminof, Sasha Rubin, Francesco Spegni +1
We consider the model checking problem of infinite state systems given in the form of parameterized discrete timed networks with multiple clocks. We show that this problem is decid…