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.