title: | Termination checking support in VerCors |
keywords: | termination, verification, software |
topics: | Logics and semantics |
committee: |
Marieke Huisman
, Petra van den Bos |
Description
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.