Interested in a software project topic, research project topic, or a thesis topic? Our topic areas include embedded and distributed systems, Internet of Things, virtualization and cloud computing, middleware and operating systems, performance engineering, software verification, program analysis, model-driven development, and more.

Naturally, we will tailor the assignments to your skills and interests, just contact us to get started. Also, do not hesitate to contact us if you have your own idea for a topic that is related to our topic areas.

Or, just take a look at the topic suggestions below, we can start from there.

Verification of LLVM bit-code via a system of constrained Horn clauses

Target
Master thesis
Contact

An approach to verification of software is model checking, which creates a logical model of the program and then checks the model for a given safety property. A logical formalism of constrained Horn clauses (CHCs) [1,2] represents a very useful model of programs that enriches the simple logical representation of theories of first-order logic with semantics being able to capture the behaviour of loops and recursion.

The goal of this thesis is to design and implement a translation from (a subset of) LLVM bit-code [3] to the language of CHCs (using appropriate logical theory) and experiment with different modelling approaches and different CHC back-ends.

  1. Horn clauses: https://en.wikipedia.org/wiki/Horn_clause
  2. https://arieg.bitbucket.io/pdf/satsmtar-school-2018.pdf
  3. LLVM project: https://llvm.org/
  4. Bjørner N., Gurfinkel A., McMillan K., Rybalchenko A. (2015) Horn Clause Solvers for Program Verification. In: Beklemishev L., Blass A., Dershowitz N., Finkbeiner B., Schulte W. (eds) Fields of Logic and Computation II. Lecture Notes in Computer Science, vol 9300. Springer, Cham. https://doi.org/10.1007/978-3-319-23534-9_2

Techniques for equivalence checking in the context of compiler optimizations

Target
Master thesis
Contact

Verification of correctness of compiler optimizations can be done by checking the equivalence of the optimized and unoptimized version (they have the same input-output relation, i.e., they provide the same outputs for the same inputs) of the processed code.

The goal of this thesis is, for various compiler optimizations, especially those considering code with loops, to survey available techniques for verification of their correctness and their shortcomings [1] and improve on them. Among considered approaches, equivalence checking, involving SMT and CHC queries corresponding to the code before and after performing the optimizations, should be involved.

  1. Lopes, N.P., Monteiro, J. Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic. Int J Softw Tools Technol Transfer 18, 359–374 (2016). https://doi.org/10.1007/s10009-015-0366-1
  2. Horn clauses: https://en.wikipedia.org/wiki/Horn_clause
  3. LLVM project: https://llvm.org/

Planning/Scheduling solver based on SMT solver

Target
Bc. thesis
Contact

Planning and scheduling are popular domains with important applications in the industry. SAT solvers have been successfully used in the planning competitions where the planning task is translated to a SAT query (or a series of such queries). The goal of this thesis is to investigate the possibility of translating planing tasks to an SMT query and use an efficient SMT solver as an underlying reasoning engine. The approach should be implemented in a transformation tool.

  1. SAT: https://en.wikipedia.org/wiki/Boolean_satisfiability_problem
  2. SMT: https://en.wikipedia.org/wiki/Satisfiability_modulo_theories

Loop Summarization

Target
Master thesis
Contact

The presence of loops in programs makes the general problem of verification undecidable. However, there are many sub-classes of loops that can be summarized efficiently. A summarized loop is represented by a set of formulas parametrized by the iteration counter. These formulas directly compute the value of variables changed by the loop for any given iteration. Using loop summarization removes the loop from a program and allows application of efficient techniques for verification of loop-free programs.

There exist different techniques for loop summarization some of which are precise, others under-approximate or over-approximate the loop behaviour. (Under-approximation can be useful for bug-finding, while over-approximation can be useful for proving correctness of programs by computing loop invariants.)

The goal of this thesis is to push the boundary of applicability of loop summarization, either by improving existing techniques (or relaxing constraints under which they are applicable) or devising a new summarization technique. Optionally also implement the designed technique and experiment with its applicability on chosen problems.

References on some existing techniques:

  1. Loop acceleration: https://link.springer.com/chapter/10.1007/978-3-030-45190-5_4
  2. Replacing loops with recurrences: https://link.springer.com/article/10.1007%2Fs10009-015-0366-1

Decision procedure for Linear Integer Arithmetic for modern SMT solver

Target
Master thesis
Contact

SMT solvers are software tools for deciding about satisfiability of formulas in first-order logics. They are powerful reasoning engines successfully used in applications such as verification of software. Linear Integer Arithmetic is a popular language for modelling verification problems, providing a good trade-off between precision and solvability.

The goal of the thesis is to implement a decision procedure for Linear Integer Arithmetic according to latest research results in the OpenSMT solver [1], and evaluate its performance, preferably using benchmarks from [2].

  1. OpenSMT: https://github.com/usi-verification-and-security/opensmt/
  2. SMT-LIB: http://smtlib.cs.uiowa.edu
  3. SMT-COMP: https://smt-comp.github.io/2019/

Bit-vector solver for OpenSMT

Target
Master thesis
Contact

Bit-vector solvers typically rely on two things: powerful pre-processing of bit-vector terms and efficient SAT solver to solve the bit-blasted problem, i.e., the transformed input formula. The goal of this thesis is to review the state-of-the-art approaches to bit-vector solving and implement the most promising one in the OpenSMT solver [1]. For an approach using bit-blasting, a different heuristic for tuning the underlying SAT solver should be compared.

  1. OpenSMT: https://github.com/usi-verification-and-security/opensmt/
  2. SMT-LIB: http://smtlib.cs.uiowa.edu
  3. SMT-COMP: https://smt-comp.github.io/2019/

Regression Benchmarking

Regression benchmarking refers to the practice of evaluating performance of individual software releases with performance tests, much as it is done with functional tests in functional regression testing. The following topics are related to our ongoing research activities in regression benchmarking:

Evaluating regression detection accuracy

In the past years, we have collected a large database of measurements, partially annotated with information about performance regressions. This task is about coming up with data analysis algorithms, including possible applications of deep learning approaches, to identify performance regressions in the measurements, and evaluating the detection accuracy and efficiency.

Medium size project for people interested in data analysis and real life software performance, suitable as individual research project, bachelor or master thesis. Some knowledge of statistics and general experimental methodology is useful.

Alternatively, the task can be about implementing innovative approaches to detection research, for example in the form of an API that would permit crowdsourcing the data analysis.

Small to medium size project for people interested in programming, suitable as individual research project, bachelor or master thesis. Knowledge of Python and Django, plus API technologies in general, is useful.

Seeking regression root causes

Discovering the root cause (reason) of a particular performance regression is usually a manual task. This task is about coming up with methods and tools for easing this task. Of particular interest is the ability to identify incidental performance changes that do not require developer attention.

Medium to large size project for people who enjoy researching difficult open problems, suitable as individual research project or master thesis. Knowledge of compilers and other programming tools, and computer architectures, is useful.

Assessing performance test coverage

Although the concept of test coverage is well defined for functional tests, an analogous concept for performance tests is still missing. This task is about coming up with ways to characterize performance test coverage.

A medium to large size project for people who enjoy open research topics, suitable as individual research project or master thesis. Knowledge of compilers and general working of computers is useful.

Modern JVM Benchmark Suite

The development of modern compilers and programming language runtimes relies on empirical measurements to assess application performance. These measurements require benchmark suites that are reasonably compact but also represent practical applications. One such suite is Renaissance.

Renaissance is in constant development and provides many contribution opportunities:

Extending the suite with benchmarks in other languages

Java Virtual Machine can execute a spectrum of languages supported by modern dynamic compilers (C, R, JS, Ruby and so on). Renaissance currently only supports Java and Scala, this task should extend the build system and include more workloads.

Medium size project for people who like coding in diverse environments, knowledge of Java, Scala build system, and build systems in general is useful.

Augmenting the existing workloads with validation

In the context of compiler development, execution correctness is not necessarily guaranteed. To detect incorrect compiler or runtime behavior, some workloads in Renaissance validate their own results. This task should extend validation to all existing Renaissance workloads.

Small to medium size project for people who like coding in diverse environments, knowledge of Java, Scala, and frameworks such as Spark is useful.

Analyzing the workload coverage

It is essential that the benchmark workloads are diverse enough to approximate many applications, but also compact enough to execute in relatively short time. This task should come up with ways to analyze the coverage of the compiler or runtime by the benchmark.

A medium to large size project for people who enjoy open research topics, knowledge of compilers and general working of computers is useful.

(Foundations of) Smart Collaborative Disassembler

Target
Team software project (4-5 team members)
Contact

The goal is to build an advanced disassembler that could be used in a collaborative fashion, i.e., with multiple users disassembling the same binary at the same time. The project should lay foundation for supporting multiple processors and binary formats, but is only required to provide support for one or two. Besides collaborative disassembly, the main focus would be designing an internal representation that would enable static analysis, limited symbolic execution, and also allow the user to reorganize and move instructions between basic blocks within the confines of the data flow graph.

Modularization of Dynamic Analyses

Target
Master thesis
Contact

Dynamic program analysis tools based on code instrumentation serve many important software engineering tasks. However, constructing new analysis tools is difficult, because existing frameworks offer little or no support to the programmer beyond the incidental task of instrumentation. The goal of this project is to develop an extension of the DiSL instrumentation framework that would support composing dynamic analyses in a modular fashion so that tasks related to maintenance of analysis state could be separated and reused.

This topic can also be an extension of the Modular Weaver for DiSL project.

Modular Weaver for DiSL

Target
Bc. thesis or Individual software project
Contact

DiSL is a bytecode instrumentation framework utilizing a domain-specific language for instrumentation hosted in Java. At the heart of DiSL is a weaver which inserts user-defined snippets of Java code into the base program. The existing weaver in the DiSL framework is rather monolithic, hindering maintenance and development of new features. The goal of the project is to modularize the DiSL weaver into multiple self-contained transformations that are applied on the Java bytecode in a predefined order.