Florian Zuleger

Armin Walch, Georg Moser, Berry Schoenmakers et al.

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 earlier works on automated amortised resource analysis by developing a type inference based approach with a generic type system. This allows for modular reasoning and the inference of precise and optimal cost bounds. More specifically, we extend the work on the ATLAS system by Leutgeb et al. which was developed to cover the analysis of splay trees and some closely related data structures. To enable the analysis of skew heaps, however, and the even more challenging (amortised) analysis of leftist heaps, we have developed a range of new techniques for type-based automated analysis. By introducing a generic type system we allow for arbitrary (classes of) potential functions, compared to the use of hard-coded potential functions in ATLAS, which we have implemented in Haskell in an entirely modular way. We have also greatly enhanced the existing type inference algorithm by extensions in multiple directions, including path-sensitive reasoning, data structure invariants, and template parameters for piecewise defined potential functions. We show how our newly developed system supports the use of all known potential functions for analysing skew heaps and leftist heaps, confirming the known bounds.

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 if membership depends only on its image under a homomorphism into a finite algebra. For SP-graphs, and more generally, for graphs of bounded tree-width, recognizability coincides with definability in Counting Monadic Second-Order (CMSO) logic. Despite this strong logical characterization, the conciseness and algorithmic effectiveness of syntactic representations of recognizable sets of SP (and bounded-tree-width) graphs remain poorly understood. Building on previously introduced regular grammars for SP-graphs, we show that recognizable sets admit concise and effective syntactic representations. The main contribution is an improved construction of finite recognizer algebras whose size is singly-exponential in the size of a regular grammar, improving upon the previously known double-exponential bound. As a consequence, the problems of intersection and language inclusion for sets represented by regular grammars are shown to be ExpTime-complete, thus improving on a previously known 2ExpTime upper bound.

Yulia Demyanova, Helmut Veith, Florian Zuleger

Human written source code in imperative programming languages exhibits typical patterns for variable use such as flags, loop iterators, counters, indices, bitvectors etc. Although it is widely understood by practitioners that these variable roles are important for automated software analysis tools, they are not systematically studied by the formal methods community, and not well documented in the research literature. In this paper, we study the notion of variable roles on the example of basic types (int, float, char) in C. We propose a classification of the variables in a program by variable roles, and demonstrate that classical data flow analysis lends itself naturally both as a specification formalism and an analysis paradigm for this classification problem. We demonstrate the practical applicability of our method by predicting membership of source files to the different categories of the software verification competition SVCOMP 2013.