Software Model Checking in the Multicore Era

contact: ahmed rezine

ceniit project 12.04

Context

In less than a decade, concurrency and the imperative to parallelize have invaded almost every computer application domain. In fact, most commercialized computers have nowadays a Multicore inside and mainstream Graphical Processing Units have already hundreds of them. One of the main reasons for this trend is that processors' clock frequencies have reached their inevitable plateau. Future computer platforms will contain more and more cores, requiring more and more concurrent or parallel code to be produced. Harnessing the potential concurrent software can offer on modern platforms is both an opportunity and a complex challenge.

Already, it is not rare to see programmers spend more time finding and fixing bugs in existing sequential code than they do writing new one. It is estimated that more than half of the software development costs of a typical project are spent on identifying and fixing defects. Software errors that remain uncovered can result in huge material losses or even human casualties. The ever increasing dependency on complex computer systems, especially for safety critical systems, and the inherent impossibility for testing to cover all scenarios have pushed big names like Microsoft and NASA to investigate and to gradually adopt formal methods and automatic verification techniques like software model checking.

Goal and Vision

Software verification is at a turning point, and promising results are currently being obtained by several academic and industrial actors. This project will allow LiU to be part of these developments and profit industrial partners from the latest developments in the area.