Software Model Checking in the Multicore Era

A CENIIT funded Research Project

Project leader: Ahmed Rezine, ahmed.rezine[email]liu.se

Last update April 2014

Background and Motivation

Modern software commonly exhibits features like concurrency, distribution, unbounded data domains, dynamic data-structures and recursion. These result in state spaces of arbitrary sizes and introduce subtle behaviors whose correctness is notoriously difficult to check. In this context, size refers to the number of threads and variables values, depth of the stack or amount of allocated heap. These difficulties are exacerbated by the unavoidable rise of multicore computers and by the imperative need to parallelize both new and legacy software. Due to inherent technological limitations, most commercialized stationary computers have nowadays a multicore inside. Future computers will contain more and more cores, requiring more and more concurrent or parallel code to be produced. The challenge is to get the most of the potential multicore computers do offer, but without getting overwhelmed by the complexity of the software bugs. It is indeed notoriously arduous to write correct concurrent programs because of the high intricacy of their behaviors. In addition to the bugs commonly found in sequential code, those found in concurrent code are essentially due to unexpected interleavings between the actions of the concurrent programs. Building techniques to help the programmer check the behavior of concurrent programs, to track bugs in order to fix them, and ultimately, to prove their absence is a challenging yet crucial task. Without such help, the nightmare of manually ensuring correctness of concurrent computer programs will only worsen.

Cegar

Accomplishments so Far

Readers and writers Michael and Scott Dekker's mutex

Available Master Thesis Projects

Current students:

Previous students:

Cooperation

National and International Cooperation:

Academia Sinica - Taiwan, Brno University - Czech Republic, IMDEA Madrid - Spain, Uppsala University, FOI Stockholm, Genoa University - Italy.

Industrial Cooperation:

Saab Linköping, Ericsson Linköping, Kista, Prover Technology Stockholm

Publications

Project's publications

Related publications

Other activities: