Skip to content

Finished Project Topics

Matthias Heizmann edited this page Feb 26, 2023 · 15 revisions

Quantifier Elimination for div and mod

Contact: Matthias

Given a logical formula F, the task of quantifier elimination is to find a quantifier-free formula F' that is logically equivalent to F. Ultimate has difficulties to eliminate variables that occur inside a div or mod operation. For example if we have a formula of the form $\exists x. F[x \operatorname{mod} K]$ we transform this into the logically equivalent formula $\exists x,aux_{div},aux_{mod}.F[aux_{mod}]\land x=aux_{div}*K+aux_{mod}\land 0\leq aux_{mod}< K$ and eliminate $x$ immediately via the DER technique. Unfortunately this transformation is not helpful if dividend of the mod operator is more complex, because then we cannot apply DER for x but introduced new quantified variables. In this project we consider a new elimination technique that can handle term of the form $\exists x. F[a\cdot x +b \operatorname{mod} K]$, were a is some integer and b is some term in which x does not occur.

Computing Representative Automata for Maximal Causality Reduction

Contact: Dominik

In this project, we built on previous work (see below) on integration of Trace Abstraction Refinement (a verification algorithm) with Maximal Causality Reduction (a technique to simplify analysis of concurrent programs). The goal was to improve the efficiency of the verification, by developing a suitable automata operation for Maximal Causality Reduction.

Statement Abstraction for POR

Contact: Dominik

This project was focused on improving our partial order reduction, by implementing a method to abstract statements in a way that leads to more statements being independent (i.e., their execution order does not matter).

Repeated Lipton Reduction in Trace Abstraction Refinement

Contact: Dominik

The goal of this project was to generalize the Lipton reduction (or Petri net large block encoding, see below) already implemented in Ultimate to be applicable in more situations and achieve better reductions. Particularly, we integrated the reduction in one of our verification algorithms, applying it repeatedly in order to benefit from the partial verification work.

Link to project page

Sleep Set POR in Trace Abstraction Refinement

Contact: Dominik

In this project, we integrated a form of partial order reduction into Ultimate. The goal was to be able to verify concurrent programs more efficiently, and even proving correctness of concurrent programs that we were unable to verify before. Together with subsequent work, this eventually resulted in a new verification tool, Ultimate GemCutter.

Link to project page

Owicki-Gries Proofs

Contact: Dominik

In this project we investigated how proofs of program correctness produced by Ultimate could be translated to Owicki-Gries proofs, a well-known notion of correctness proofs for concurrent programs. Owicki-Gries proofs can be exponentially smaller than the proofs usually produced by Ultimate, and we tried different methods to produce small proofs if possible.

Link to project page

Trace Abstraction with Maximal Causality Reduction

Contact: Dominik

In this project we have adapted a model checking technique for concurrent programs, Maximal Causality Reduction, to the verification of infinite-state programs, in particular to Trace Abstraction Refinement. We have integrated the technique into Ultimate Automizer.

Link to project page

Large Block Encoding for Concurrent Programs

Contact: Matthias

In this project we have implemented Petri Net Large Block Encoding in Ultimate. This technique is based on Lipton reductions, a form of Partial Order reduction, and allows us to verify concurrent programs much faster, by reducing the size of the Petri net representing the program and reducing the number of interleavings that the verification must consider.

Link to project page

Implementation of Tree Automata Operations

Contact: Alexander

In a previous project we have laid the grounds for tree automata in our automata library. In this project we want to review standard algorithms such as intersection, difference, determinization, etc. for tree automata from the literature and implement them. In particular, for efficiency reasons, we want to develop new on-the-fly algorithms which do not construct the whole automaton at once but only on demand.

Loop Acceleration

Contact: Daniel or Matthias

We fail to prove that the following program is incorrect, because we have to unroll the loop 10000 times until we find the error.

i := 0;
while (i<10000) {
     i++;
}
assert i==23;

Develop techniques that let us replace the loop by i := 10000 and find the error immediately. See e.g., 2015FMSD - Kroening, Lewis, Weissenbacher - Under-Approximating Loops in C Programs for Fast Counterexample Detection, 2012ISSTA - Strejcek,Trtik - Abstracting Path Conditions, 2010CAV - Bozga,Iosif,Konecny - Fast Acceleration of Ultimately Periodic Relations

Verify real-world software

Contact: Daniel

As Ultimate matures, we are interested in gathering experience with the verification of real-world software written in C. To this end, we want to use existing tools (naturally, Ultimate among them) to verify properties of real-world software.

The properties may range from rather simple common runtime errors (e.g., nullpointer dereferences, division by zero, etc.) over finding over/underflows to functional properties specified by annotations.

Possible software sources are

  • Parts of Trezor, a hardware bitcoin wallet.
  • Newlib, an open-source math library
  • Closed-source examples
  • Own proposals

The project would involve selecting a suitable problem, trying to solve it with Ultimate and/or various other tools, and reporting the results.

Parse and preprocess multiple C files

Contact: Daniel

Ultimate relies on the CDT infrastructure to parse C files. But Ultimate currently supports only programs that are contained in a single file and are already preprocessed.

Users expect program analysis tools to be able to analyze programs that are scattered over multiple files, e.g. source files and headers. Our target audience is usually familiar with command line tools and compilers, especially gcc. Our user interface should therefore be similar to gcc's command line interface (i.e., we may add options ff:or specifying files, headers and entry function separately). There are many examples of gcc's syntax for this, e.g. this one.

The main goal of this project is making Ultimate's C interface able to create one analysable representation (one control flow graph) from a C program distributed over several input files and headers.

We expect that the main (early) work will be research regarding the inner workings of CDT. You can see how we currently use CDT in the class CDTParser and there in the method parseAST(...). There, we create a wrapper node around an IASTTranslationUnit. The first question will be: can we create just one translation unit from the whole program (i.e., from multiple input files), or do we have to find another approach?

Implementation of Hybrid Automata Support

Contact: Marius

Hybrid automata are a way to model real-world cyber-physical systems. A hybrid automaton is essentially a non-deterministic automaton, where - in addition - the locations contain invariants over the automaton's variables and some description of the change of the dynamic variables in form of a differential equation. This way, a hybrid automaton is allowed to stay in some location, instead of taking an enabled transition immediately, as long as the invariant of such location is not violated. Its variables are changed according to the specified dynamics as long as it stays in said location.

A network of hybrid automata contains multiple hybrid automata that share some variables. A run of such a network of hybrid automata considers all contained hybrid automata in parallel.

A well-known model checker for networks of hybrid systems is SpaceEx which is specialized for the computation of differential equations. It performs a reachability analysis of the state space of the network and checks for safety properties. SpaceEx' input is an XML file that contains a description of the hybrid automaton network.

The task of this project is to use the already existing SpaceEx XML parser and to implement the construction of the parallel product of all hybrid automata contained in a network of hybrid automata. Furthermore, this "flattened" SpaceEx model should then be translated into a Boogie program, thus enabling Ultimate's analysis plugins, such as Automizer or Abstract Interpretation, to perform some analyses on the result.

The goal of this project is to end up with a translation of hybrid automata to Boogie code which in turn can be used to check some properties on. Furthermore, when a property has been checked on the Boogie code, we would like to reason about the original hybrid system. Finally, we would like to compare accuracies, run times, pitfalls, etc. of the Boogie translation and Ultimate analysis process to SpaceEx' analysis to find out where either tool can be improved to provide more precise results.

Delta Debugger for Model Checkers of C Programs

Contact: Christian

Motivation:

Consider a program P and a test input T such that there is an unexpected behavior of P applied to T. We want to find out the reason why this behavior has occurred. Usually, the behavior is an error and we want to find the bug in the implementation which lead to that error. A typical problem in practice is that the example might be very big, so the analysis is hard. A possible approach to simplify the example is called delta debugging.

Delta debugging:

Given an example and a set of simplification rules, a delta debugger applies the rules to the example as long as possible. The output will be an example which

  • is (locally) minimal with respect to the set of rules,
  • still has the same behavior (i.e., the bug).
Task:

We have a Java framework with a lot of tools which work on C programs (e.g., for program verification) and already have a working implementation of a delta debugger for a different type of input (an automaton for our automata library).

  • You implement the general architecture of a delta debugger for C programs in our Java framework. This means given a C program, minimize it with respect to a set of rules.
  • Afterward, you develop and implement some possible rules to make it applicable.

In principle, you need not have any knowledge about the C programming language. You write the delta debugger in Java, while the C programs are only the input to your tool. For more sophisticated rules, you need to aquire some basic knowledge about C.

Fault Localization

Contact: Christian and Matthias

Motivation/Applications:
  • Analyzing an error trace helps a programmer understand the reason for an error.
  • Checking overapproximation in traces is relevant for an error.
  • Trace generalization (for test generation - avoids "similar" tests).
Relevant Literature:

2013 VMCAI - Christ, Ermis, Schäf, Wies - Flow-Sensitive Fault Localization

Problem:

Given a consistent (feasible) error trace in a program automaton, find statements that are irrelevant for feasibility of the trace.

General approach:

Analyze the "tiger" trace. Construct some trace formula for the tiger trace. Check satisfiability of this trace formula. Use interpolants or an unsatisfiable core to find the relevant conjuncts/statements.

Naive approach:

Construct the flow insensitive trace formula for the tiger trace; check satisfiability.

Two shortcomings of the naive approach:

  1. works only if tiger trace is infeasible (cases where error trace is feasible iff tiger trace is infeasible?)
  2. naive approach is not flow-sensitive

How to address these shortcomings:

  1. Do not analyze solely the tiger trace but analyze tiger trace + precondition, namely the weakest precondition wp(false, error-trace). Because not(wp(false, error-trace)) together with the tiger trace is infeasible.
  2. Use the flow-sensitive trace formula.
  • Obstacle: Algorithm (from the paper) is only defined for traces that contain additional control flow information (if, endif, ...).
  • Task: Develop a new algorithm for traces without control flow information (e.g., traces that orginate from program with gotos).

Minimization of Büchi Nested Word Automata

Contact: Christian and Matthias

Extend ''2005 SIAMCOMP - Etessami, Wilke, Schuller - Fair Simulation Relations, Parity Games, and State Space Reduction for Buchi Automata'' to nested word automata.

Minimization of Nested Word Automata by Reduction to (Max)SAT

Contact: Christian and Matthias

In this project we encoded the minimization problem for nested word automata (NWA) as a (propositional) logical formula. Any satisfying assignment corresponds to a quotienting of an equivalent NWA. A "minimal" NWA (with respect to this technique) can then be obtained from a satisfying assignment with a maximum number of ''true'' assignments.

Clone this wiki locally