« October 2017 »
October
MoTuWeThFrSaSu
1
2345678
9101112131415
16171819202122
23242526272829
3031
Uni-Logo
You are here: Home Teaching Student Projects and Thesis Topics Available [Varies] Verification of Concurrent Programs
Document Actions

[Varies] Verification of Concurrent Programs

Course type Bachelor-Project, Bachelor Thesis, Master Laboratory or Master Team Project
Instructors Matthias Heizmann
Credits Depending on course type
Course Catalog
Consider the following program which is a simplified implementation of an ATM.
public void withdrawlAction(int *accountBalance) {
    int displayedBalace := *accountBalance;
    int withdrawlAmount := readCustomerInput();
    *accountBalance := displayedBalace - withdrawlAmount;
}
Does the program reduce the account balance by the withdrawl amount?


Now consider the a setting where we have two ATMs each executing this program in parallel. We assume that the procedure is not executed atomically. Each interleaving of statements of both programs is possible.

 

Do the programs always reduce the account balance by the withdrawl amounts?

 

In this project we will analyze methods to verify concurrent programs.

Personal tools