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.