TU BRAUNSCHWEIG

Master Exchange Programme with Stellenbosch University, South Africa

Starting in April 2019, we will be able to offer 2 Master students per year the opportunity to do write their Master thesis at Stellenbosch University, South Africa, under a new Memorandum of Understanding between TU Braunschweig and Stellenbosch University.

You will stay in Stellenbosch from 1 April - 30 September and write your Master Thesis under supervision of a professor at the Computer Science department of Stellenbosch University. TUBS will pay for your return travel. Stellenbosch University will assist you with accomoation, health insurance, visa matters etc. You can apply for a stipend to cover (parts of) your living expenses.

Below you find open Master thesis topics and supervisors for the 2019 Stellenbosch exchange, i.e., 1 April 2019 - 30 September 2019.

If you are interested in the exchange, please email Prof. Dr. Ina Schaefer.


Sequentialization of multi-threaded code under restricted scheduling policies

(supervised by Bernd Fischer )

Sequentialization is a symbolic verification technology for concurrent programs that relies on a translation into reachability-equivalent non-deterministic sequential programs; this allows the reuse of existing high-performance verifiers for sequential progams [1]. However, in many application domains (e.g., resource-constrained embedded systems) the program's threads are scheduled according to a restricted policy (e.g., based on thread or interrupt priorities). For such applications, the standard sequentialization methods can yield wrong results, because they do not take into account the limits of the scheduling policy. This problem has attracted only little attentation (e.g., [2]).

The goal of this project is to implement and evaluate specific sequentialization techniques for a range of such restricted scheduling policies. The work should build on top of our award-winning CSeq-framework, which provides Python components to quickly build sequentialization tools for C/C++ programs.

[1] Omar Inverso, Truc L. Nguyen, Bernd Fischer, Salvatore La Torre, Gennaro Parlato: Lazy-CSeq: A Context-Bounded Model Checking Tool for Multi-threaded C-Programs. ASE 2015: 807-812
[2] Sagar Chaki, Arie Gurfinkel, Soonho Kong, Ofer Strichman: Compositional Sequentialization of Periodic Programs. VMCAI 2013: 536-554


Grammar-Driven Generation of Well-Scoped Programs

(supervised by Bernd Fischer )

Syntactically well-formed programs can be generated from a context-free grammar in a very straightforward manner [1]. However, context-free grammars can, by definition, not express context-sensitive dependencies such as a programming language's scope rules. The purpose of this project is to extend the idea of grammar-driven program generation to ensure that the generated programs are well-scoped, or, conversely, break the scoping rules in a precise way.

There are several generic mechanisms such as attribute grammars or two-stage grammars that can be used to describe context-sensitive dependencies. However, the approach suggested for this project is to use a domain-specific name binding language such as NaBL [2] to formalize the scope rules. NaBL is based on abstract scopes (i.e., syntax tree fragments); scope rules specify which declarations are valid and visible within a scope. The core idea is to systematically derive the minimal syntax tree fragments (which can include several scopes) that are necessary to satisfy resp. violate any given scope rule, which can then be embedded into a derivation. The project should design coverage criteria similar to context-dependent rule coverage [1] for scopes and use these to exhaustively generate positive and negative test cases, i.e., well-scoped programs as well as programs that break specific scope rules. The project should then implement test suite generation algorithms based on these coverage criteria and evaluate their fault localization performance over a wide range of grammars. This could be extended to automatically construct oracles for such tests; this requires encoding observable side effects into the test cases, e.g., in the form of value assignments.

The implementation could build on an existing grammar-based test-case generation in Prolog, but can also be done in another language.

[1] R Laemmel. Grammar testing. Fundamental Approaches to Software Engineering (FASE’01), LNCS 2029:201–216, 2001.
[2] GDP Konat, LCL Kats, G Wachsmuth, E Visser. Declarative Name Binding and Scope Rules. Software Language Engineering (SLE’12). LNCS 7745:311-331, 2012.


EVM Smart Contract Analysis with JPF

(supervised by Willem Visser )

The Ethereum Virtual Machine (EVM) executes the code for Ethereum Smart Contracts. This project entails analysis of EVM bytecode, in the same way as Java PathFinder (JPF) allows analysis of Java bytecode. In fact the JPF analysis framework allows one to change the bytecodes and their semantics (from the standard JVM semantics) and thus allows one to interpret EVM bytecodes instead. One approach to analysis of EVM bytecode is thus to adapt JPF to directly interpret EVM bytecode. This will be the preferred approach. Another approach is to translate EVM bytecodes to JVM bytecodes before analysis, and then to use JPF as is. After JPF can analyse EVM bytecode the second part of the project will entail doing symbolic execution of the EVM bytecode. This is a straight-forward step and will mirror how Symbolic PathFinder works.

There are several generic mechanisms such as attribute grammars or two-stage grammars that can be used to describe context-sensitive dependencies. However, the approach suggested for this project is to use a domain-specific name binding language such as NaBL [2] to formalize the scope rules. NaBL is based on abstract scopes (i.e., syntax tree fragments); scope rules specify which declarations are valid and visible within a scope. The core idea is to systematically derive the minimal syntax tree fragments (which can include several scopes) that are necessary to satisfy resp. violate any given scope rule, which can then be embedded into a derivation. The project should design coverage criteria similar to context-dependent rule coverage [1] for scopes and use these to exhaustively generate positive and negative test cases, i.e., well-scoped programs as well as programs that break specific scope rules. The project should then implement test suite generation algorithms based on these coverage criteria and evaluate their fault localization performance over a wide range of grammars. This could be extended to automatically construct oracles for such tests; this requires encoding observable side effects into the test cases, e.g., in the form of value assignments.

Once the tool can analyse EVM bytecodes symbolically we will focus on the analysis of a number of smart contracts with known issues. Here we will compare to Manticore, a tool we are currently using for this purpose.


Evaluate the COASTAL concolic execution tool for Java

(supervised by Willem Visser )

This project is mostly empirical in nature. It involves doing something that has not been done before, and that is to compare the performance of a classic symbolic execution tool with a concolic tool on the exact same benchmarks. Specifically it will be comparing Symbolic PathFinder (SPF) which uses classic symbolic execution with COASTAL a state-of-the-art. concolic execution tool for Java. The study will involve determining the strengths and weaknesses of each approach, and in particular how each handles cases that cannot be executed symbolically. Another important point would be to compare top-down repeat executions (as in concolic) versus backtracking search (as in classic symbolic execution). We have a wealth of experience with both approaches (we built COASTAL, and we have helped develop SPF).


  last changed 10.10.2018
TU_Icon_E_Mail_1_17x17_RGB pagetop