|title:||Termination checking support in VerCors|
|keywords:||termination, verification, software|
|topics:||Logics and semantics|
Petra van den Bos
Termination of a program is usually a desired property, but sometimes the programmer unintendedly violates this property. For example, if the programmer wrote a non-terminating loop, or used a function call resulting in non-terminating recursion. In this project you will study program termination and implement verification support in the tool VerCors. You will focus on proving termination of loops. Note: In principle it is well-known how to reason about termination, but the challenge of this project is to incorporate this well-known technique into the VerCors verifier.
You will be expected to take the following steps:
- Study papers about verification of loop termination.
- Write an example program with loop termination specifications.
- Understand the VerCors architecture.
- Investigate how to adapt the VerCors architecture such that it supports loop termination specifications.
- Implement the necessary changes.