-
Chapter and Conference Paper
Ultimate TestGen: Test-Case Generation with Automata-based Software Model Checking (Competition Contribution)
We introduce Ultimate TestGen, a novel tool for automatic test-case generation. Like many other test-case generators, Ultimate TestGen builds on verification technology, i.e., it checks the (un)reachability of te...
-
Chapter and Conference Paper
Ultimate Automizer and the Abstraction of Bitwise Operations
The verification of Ultimate Automizer works on an SMT-LIB-based model of a C program. If we choose an SMT-LIB theory of (mathematical) integers, the translation is not precise, because we overapproximate bitwise...
-
Chapter and Conference Paper
Petrification: Software Model Checking for Programs with Dynamic Thread Management
We address the verification problem for concurrent program that dynamically create (fork) new threads or destroy (join) existing threads. We present a reduction to the verification problem for concurrent progr...
-
Chapter and Conference Paper
Ultimate Automizer and the CommuHash Normal Form
The verification approach of Ultimate Automizer utilizes SMT formulas. This paper presents techniques to keep the size of the formulas small. We focus especially on a normal form, called CommuHash normal form tha...
-
Chapter and Conference Paper
Ultimate Taipan and Race Detection in Ultimate
Ultimate Taipan integrates trace abstraction with algebraic program analysis on path programs. Taipan supports data race checking in concurrent programs through a reduction to reachability checking. Though the su...
-
Chapter and Conference Paper
Ultimate GemCutter and the Axes of Generalization
Ultimate GemCutter verifies concurrent programs using the CEGAR paradigm, by generalizing from spurious counterexample traces to larger sets of correct traces. We integrate classical CEGAR generalization with ort...
-
Chapter and Conference Paper
Verification of Concurrent Programs Using Petri Net Unfoldings
Given a verification problem for a concurrent program (with a fixed number of threads) over infinite data domains, we can construct a model checking problem for an abstraction of the concurrent program through...
-
Chapter and Conference Paper
Separating Map Variables in a Logic-Based Intermediate Verification Language
In SMT solver based verification, the program to be verified is often given in an intermediate verification language such as Boogie. We present a program transformation that aims at splitting mathematical arra...
-
Chapter and Conference Paper
Ultimate Taipan with Symbolic Interpretation and Fluid Abstractions
Ultimate Taipan is a software model checker that combines trace abstraction with abstract interpretation on path programs. In this year’s version, we replaced our abstract interpretation engine and now use a comb...
-
Chapter and Conference Paper
Semantic Fault Localization and Suspiciousness Ranking
Static program analyzers are increasingly effective in checking correctness properties of programs and reporting any errors found, often in the form of error traces. However, developers still spend a significa...
-
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 ...
-
Chapter and Conference Paper
Geometric Nontermination Arguments
We present a new kind of nontermination argument, called geometric nontermination argument. The geometric nontermination argument is a finite representation of an infinite execution that has the form of a sum of ...
-
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 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...
