-
Notifications
You must be signed in to change notification settings - Fork 41
Finished Project Topics
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
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
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.
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).
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.
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.
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.
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.
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.
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.
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
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.
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?
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.
Contact: Christian
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.
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).
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.
Contact: Christian and Matthias
- 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).
2013 VMCAI - Christ, Ermis, Schäf, Wies - Flow-Sensitive Fault Localization
Given a consistent (feasible) error trace in a program automaton, find statements that are irrelevant for feasibility of the trace.
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.
Construct the flow insensitive trace formula for the tiger trace; check satisfiability.
Two shortcomings of the naive approach:
- works only if tiger trace is infeasible (cases where error trace is feasible iff tiger trace is infeasible?)
- naive approach is not flow-sensitive
How to address these shortcomings:
- 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.
- 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).
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.
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.
- Home
- Ultimate Development
- Ultimate Build System
- Documentation
- Project Topics