[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.
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.
public void withdrawlAction(int *accountBalance) {
int displayedBalace := *accountBalance;
int withdrawlAmount := readCustomerInput();
*accountBalance := displayedBalace - withdrawlAmount;
}
|
public void withdrawlAction(int *accountBalance) {
int displayedBalace := *accountBalance;
int withdrawlAmount := readCustomerInput();
*accountBalance := displayedBalace - withdrawlAmount;
}
|
Do the programs always reduce the account balance by the withdrawl amounts?
In this project we will analyze methods to verify concurrent programs.