32 citations · 78 across the 16 of their papers we have counts for
6 papers · 1 filter
Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs
Moritz Sinn, Florian Zuleger, Helmut Veith
Difference constraints have been used for termination analysis in the literature, where they denote relational inequalities of the form x' <= y + c, and describe that the value of…
Local Linearizability
Andreas Haas, Thomas A. Henzinger, Andreas Holzer +6
The semantics of concurrent data structures is usually given by a sequential specification and a consistency condition. Linearizability is the most popular consistency condition du…
A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis
Moritz Sinn, Florian Zuleger, Helmut Veith
We present the first scalable bound analysis that achieves amortized complexity analysis. In contrast to earlier work, our bound analysis is not based on general purpose reasoners…
Shape and Content: Incorporating Domain Knowledge into Shape Analysis
Diego Calvanese, Tomer Kotek, Mantas Šimkus +2
The verification community has studied dynamic data structures primarily in a bottom-up way by analyzing pointers and the shapes induced by them. Recent work in fields such as sepa…
On the Concept of Variable Roles and its Use in Software Analysis
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…
Bound Analysis of Imperative Programs with the Size-change Abstraction (extended version)
Florian Zuleger, Sumit Gulwani, Moritz Sinn +1
The size-change abstraction (SCA) is an important program abstraction for termination analysis, which has been successfully implemented in many tools for functional and logic progr…