Oppgaven er ikke lenger tilgjengelig

Verification Tool for Concurrent Software

Writing bug-free, safe, software in a modern language like Java can be quite a challenge: apart from getting the business logic of what is to be implemented right, null-pointer accesses and other bugs get in our way.

For concurrent/multi-threaded software, we face yet another challenge: firstly, we need to figure out where to use concurrency primitives like locking to protect shared data. Design decision have a big influence on performance here—of course we could just use one "giant" lock to protect resources, but then we'd almost end up with a sequential application again.

More critically, we may accidentally introduce deadlocks or data-races, which will make our application get stuck or produce garbled results.

At PMA, we have developed a basic theory about how to analyse such software (we're certainly not the first; there's lots of existing theory and even commercial tools). Now, the challenge is to turn this into a useable tool for Java (analysing synchronized blocks, or locking using java.util.concurrent) or for C-programs using the pthreads-API. Another alternative would be the Go language.

A prospective student would try to use an existing program analysis framework like Soot to...

  • implement the analysis,
  • collect performance results on scalability,
  • run experiments on existing open-source software projects,
  • contribute to publications/conference submissions.

It may be possible to visit TU Darmstadt (Germany) during the thesis.


Emneord: concurrency, verification, static analysis, java
Publisert 22. sep. 2014 16:14 - Sist endret 14. des. 2017 12:04


  • Christian Bergersen

Omfang (studiepoeng)