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.


Emneord: concurrency, verification, static analysis, java
Publisert 7. okt. 2020 14:34 - Sist endret 8. okt. 2020 07:35

Omfang (studiepoeng)