Description

In Twente, we are developing the VerCors program verifier. VerCors can reason about programs with integers. When reasoning about these integers, we interpret them as mathematical integers. However, in real programs these integers are machine integers or bounded integers. Besides integers, VerCors currently does not support reasoning about bytes, shorts and similar.

In this project, we would like to investigate how we can add support for bounded numbers, (e.g. integers, bytes, shorts and similar):

The following steps would be necessary:
    •    understand how bounded numbers are encoded
    •    how different modes for reasoning (e.g. bounded, mathematic) can be supported 
    •    understand the VerCors architecture
    •    investigate how to add bounded numbers into VerCors
    •    implement the necessary changes