-
Chapter and Conference Paper
Refinement of Trace Abstraction
We present a new counterexample-guided abstraction refinement scheme. The scheme refines an over-approximation of the set of possible traces. Each refinement step introduces a finite automaton that recognizes a s...
-
Chapter and Conference Paper
Size-Change Termination and Transition Invariants
Two directions of recent work on program termination use the concepts of size-change termination resp. transition invariants. The difference in the setting has as consequence the inherent incomparability of th...
-
Chapter and Conference Paper
Ultimate Automizer with SMTInterpol
Ultimate Automizer is an automatic software verification tool for C programs. This tool is the first implementation of trace abstraction, which is an automata-theoretic approach t...
-
Chapter and Conference Paper
Linear Ranking for Linear Lasso Programs
The general setting of this work is the constraint-based synthesis of termination arguments. We consider a restricted class of programs called lasso programs. The termination argument for a lasso program is a ...
-
Chapter and Conference Paper
Software Model Checking for People Who Love Automata
In this expository paper, we use automata for software model checking in a new way. The starting point is to fix the alphabet: the set of statements of the given program. We show how automata over the alphabet...
-
Chapter and Conference Paper
Ultimate Automizer with Unsatisfiable Cores
Ultimate Automizer is an automatic software verification tool for C programs. This tool is a prototype implementation of an automata-theoretic approach that allows a modular verif...
-
Chapter and Conference Paper
Ranking Templates for Linear Loops
We present a new method for the constraint-based synthesis of termination arguments for linear loop programs based on linear ranking templates. Linear ranking templates are parametrized, well-founded relations su...
-
Chapter and Conference Paper
Termination Analysis by Learning Terminating Programs
We present a novel approach to termination analysis. In a first step, the analysis uses a program as a black-box which exhibits only a finite set of sample traces. Each sample trace is infinite but can be repr...
-
Chapter and Conference Paper
Ultimate Automizer with Array Interpolation
Ultimate Automizer is a software verification tool that is able to analyze reachability of an error label, memory safety, and termination of C programs. For all three tasks, our tool follows an...
-
Chapter and Conference Paper
Fairness Modulo Theory: A New Approach to LTL Software Model Checking
The construction of a proof for unsatisfiability is less costly than the construction of a ranking function. We present a new approach to LTL software model checking (i.e., to statically analyze a program and ...
-
Chapter and Conference Paper
Automated Program Verification
A new approach to program verification is based on automata. The notion of automaton depends on the verification problem at hand (nested word automata for recursion, Büchi automata for termination, a form of d...
-
Chapter and Conference Paper
Ultimate Automizer with Two-track Proofs
Ultimate Automizer is a software verification tool that implements an automata-based approach for the analysis of safety and liveness problems. The version that participates in this year’s competition is...
-
Chapter and Conference Paper
Complementing Semi-deterministic Büchi Automata
We introduce an efficient complementation technique for semi-deterministic Büchi automata, which are Büchi automata that are deterministic in the limit: from every accepting state onward, their behaviour is de...
-
Chapter and Conference Paper
Ultimate Taipan: Trace Abstraction and Abstract Interpretation
Ultimate Taipan is a software model checker for C programs. It is based on a CEGAR variant, trace abstraction [7], where program abstractions, counterexample selection and abstraction refinement are base...
-
Chapter and Conference Paper
Ultimate Automizer with an On-Demand Construction of Floyd-Hoare Automata
Ultimate Automizer is a software verifier that implements an automata-based approach for the verification of safety and liveness properties. A central new feature that speeded up the abstraction refinement of the...
-
Chapter and Conference Paper
Minimization of Visibly Pushdown Automata Using Partial Max-SAT
We consider the problem of state-space reduction for nondeterministic weakly-hierarchical visibly pushdown automata (Vpa). Vpa recognize a robust and algorithmically tractable fragment of context-free languages t...
-
Chapter and Conference Paper
Ultimate Automizer and the Search for Perfect Interpolants
Ultimate Automizer is a software verifier that generalizes proofs for traces to proofs for larger parts for the program. In recent years the portfolio of proof producers that are available to Ultimate has grown c...
-
Chapter and Conference Paper
Ultimate Taipan with Dynamic Block Encoding
Ultimate Taipan is a software model checker that uses trace abstraction and abstract interpretation to prove correctness of programs. In contrast to previous versions, Ultimate Taipan now uses dynamic block encod...
-
Chapter and Conference Paper
The Map Equality Domain
We present a method that allows us to infer expressive invariants for programs that manipulate arrays and, more generally, data that are modeled using maps (including the program memory which is modeled as a m...
-
Chapter and Conference Paper
Incremental Verification Using Trace Abstraction
Despite the increasing effectiveness of model checking tools, automatically re-verifying a program whenever a new revision of it is created is often not feasible using existing tools. Incremental verification ...
