Description

In Twente, we are developing the VerCors program verifier. VerCors transforms input programs step-by-step into its backend Viper and in turn Z3, the SMT solver. One of these transformations is rewriting expressions to make it easier for Z3 to verify. 

The current rewrite system allows for rewrite rules that are purely syntactical. This means that an expression is rewritten only if it matches the rewrite rule exactly. This approach lackssupport for more complex and expressive rewrite rules.

In this project, we would like to investigate how we can improve the rewrite system.
The following steps would be necessary:
    •    understand the rewrite system
    •    understand the VerCors architecture
    •    investigate how we can adapt the current rewrite system to support more complex rewrite rules
    •    implement the necessary changes