Project A

Deadline: October 27, 23:59

The project can be solved in many different ways. It is important that you can reasonably justify your design decisions. Feel free to ask for clarification if you are unsure about a task or your approach.

Submission: push your solution to the GitLab repository of your homework group. The latest push before the deadline will be considered as your submission.

Task

Your task is to use the concepts introduced in the course to develop an automated verification tool for a language called MicroViper, a subset of the Viper language considered throughout the course. The details of the MicroViper language are specified further below.

We split the task of implementing a MicroViper verifier into core features, which must be implemented by every submission, and extension features, which you should consider implementing if you aim for a good or excellent grade. The individual features are listed further below.

A written report is not required. However, you must add a file README.md that contains the following:

Structure of your project, for example the main steps of your toolchain and where each step is found in your code.
What has and has not been implemented.
How to install and run your project.
A brief explanation of your design decisions.
An evaluation, for example a set of programs that you verified with both Viper and your implementation.

Grading

As a guideline, your grade is determined by your submission's quality and completeness, that is, how many extension features are supported. Larger groups should aim for supporting more extension features than small groups.

For this project, "supporting a feature" means that the following conditions are met:

The feature is implemented and sufficiently documented such that it can be used by other course participants.
The README.md justifies why your approach for implementing a feature is sound; if you implement an approach discussed in class, it is OK to refer to the corresponding course material.
The feature is tested against at least six (non-trivial) MicroViper programs using the specific feature. Where possible, four of your examples should verify and two should be correctly rejected. The Viper verifier must yield the same result (verify/does not verify) for your test programs unless explicitly stated otherwise in the feature description. You are allowed to use the example programs considered in class.

To obtain the grade 4, your submission must support all core features. An excellent submission aiming for the grade 12 should target four or more extension features.

Programming Language & Infrastructure

Your solution must use an SMT solver, such as Z3, for discharging verification conditions. You can use either an existing Z3 API or generate SMTLIB-2 code and invoke Z3 through your tool.

You can implement your verifier in a programming language of your own choice. For example, there exist libraries for working with Z3 in Rust, F#, and Python.

To reduce the initial overhead, we will provide you with code skeletons including a MicroViper parser and an example for invoking Z3 in selected languages.

Rust code skeleton

F# code skeleton

Every group must submit an original solution. However, it is fine to share supporting infrastructure, for example parsers, as long as you clearly indicate what is shared in your README.md.

Features

We list the core and extension features below. There is no particular order for extension features; you can work on any subset of your choice.

However, remember that you are expected to complete the core features.

You are welcome to propose and implement other extension features. Please first contact the teacher to check if your idea qualifies as an extension feature.

Core Feature 1

Your MicroViper verifier must support programs that consist of a single method, where

no expression in the method's specification or body uses a division operation (/);
the method body contains no loops, no method calls, and no user-defined function calls; and
the method specification contains no user-defined function calls.

Core Feature 2

Your MicroViper verifier must support reasoning about partial correctness (that is, assertion failures still fail verification but termination is not required) of while loops.

Core Feature 3

Your MicroViper verifier must support expressions in the method's specification or body that use the division operation (/).

Hint: Remember to deal with corner cases. For example, what should happen if you add an expression like x / y or 17 / 0 to a pre- or postcondition? Your implementation must remain sound and should be able to verify reasonable usages of /.

Extension Feature 1

Your MicroViper verifier should indicate why verification failed, that is, which specification (e.g. a postcondition) or assertion cannot be verified.

For obvious reasons, supporting this feature does not require that you give example programs that successfully verify.

Extension Feature 2

Extend your MicroViper verifier such that it supports reasoning about partial correctness (that is, assertion failures still fail verification but termination is not required) of multiple methods that may possibly recusively call each other.

Extension Feature 3

Extend your MicroViper verifier such that one can define and call user-defined functions with an implementation, that is an expression that serves as the function body. It is not required that one can attach pre- or postconditions to such functions.

Explain in your README.md whether you use limited functions or not; justify your answer. If possible, try to include examples where using limited functions might help and/or hinder verification.

Hint: Recall that function calls are expressions, that is, they may appear in specifications.

Extension Feature 4

Extend your MicroViper verifier such that one can define and call abstract user-defined functions. That is, it should now be possible to attach pre- or postconditions to user-defined functions; providing a function body is optional.

Hint: Function calls are expressions and may appear in specifications. Consequently, you have to be careful if a function with a pre- or postcondition is called inside of another pre- or postcondition.

Extension Feature 5

Use efficient weakest preconditions in your MicroViper verifier. Try to use larger example programs demonstrating the efficiency gain.

Extension Feature 6

After supporting extension feature 2, extend your MicroViper verifier such that one can declare global variables, that is, var name:type may be used outside of method bodies. For simplicity, we require that global variable names must be distinct from all other variable, method, and function identifiers.

It is not required to compare against Viper for this task.

Hint: Global variables have consequences for how you deal with method calls. You may want to add new annotations to methods. Briefly explain your design decisions in your README.md.

Extension Feature 7

Extend your MicroViper verifier such that one can reason about total correctness of while loops.

It is not required to compare against Viper for this task.

Hint: You may want to add new annotations to loops for checking termination. If you introduce such constructs, briefly explain them in your README.md

Extension Feature 8

Extend your MicroViper verifier such that one can reason about total correctness of recursive methods.

It is not required to compare against Viper for this task.

Hint: You may want to add new annotations to methods for checking termination. If you introduce such constructs, briefly explain them in your README.md

The MicroViper Language

Informal summary

The MicroViper language is a subset of the Viper language with methods, functions, loops, variables of type Int or Bool, variable declarations, assignments, conditionals, and the usual expressions and predicates considered in class. As specification constructs, MicroViper admits assume and assert statements, pre- and postconditions (requires and ensures) as well as loop invariants invariant.

When in doubt, your language should work with the Viper verifier (unless you work on extension features that specifically diverge from Viper). This allows you to test your implementation against Viper.

Language specification

MicroViper programs are given by the grammar below. The grammar uses extended syntax inspired by regular expressions: A* denotes zero or more repetitions of A; A? denotes that A is optional, that is, zero or one appearances of A.

An identifier Ident is any non-empty string that

is not a keyword used in the grammar and
starts with a letter or _ followed by arbitrary many letters, _ or digits, that is, it is matched by the regular expression [a-zA-Z_][a-zA-Z_0-9]*.

Document ::= DocumentItem*

DocumentItem ::=
    Method |
    Function

Method ::=
    "method" Ident "(" Vars ")"
    "returns" "(" Vars ")")?
    Specification*
    Body?

Function ::=
    "function" Ident "(" Vars ")" ":" Type
    Specification*
    ("{" Expr "}")?

Specification ::=
    "requires" Expr |
    "ensures" Expr

Body ::= "{" Statement* "}"

Statement :=
    "assert" Expr |
    "var" Var (":=" Expr)? |
    "if" "(" Expr ")" Body ("else" Body)? |
    "while" "(" Expr ")" ("invariant" Expr)* Body |
    Idents ":=" Ident "(" Exprs ")" |
    Idents ":=" Expr

Idents ::= Ident | Ident "," Idents

Vars ::= Var | Var "," Vars
Var ::= Ident ":" Type

Type ::= "Int" | "Bool"

Exprs = Expr | Expr "," Exprs
Expr ::=
    "true" |
    "false" |
    "result" |
    Integer |
    Ident |
    "(" Expr ")",
    Ident "(" Exprs ")" |

    "-" Expr |
    "!" Expr |

    Expr "*" Expr |
    Expr "/" Expr |

    Expr "+" Expr |
    Expr "-" Expr |

    Expr "<=" Expr |
    Expr "<" Expr |
    Expr ">=" Expr |
    Expr ">" Expr |
    Expr "==" Expr |
    Expr "!=" Expr |

    "exists" Var "::" Expr |
    "forall" Var "::" Expr |

    Expr "||" Expr |

    Expr "&&" Expr |

    Expr "==>" Expr

We impose a few more rules for MicroViper programs. Your implementation does not have to check them but implementing rudimentary checks (as done by the code skeletons) may help you identifying issues in your test and example programs.

We will only consider MicroViper programs that respect the following rules:

For each nonterminal, e.g., Expr, rules are grouped together; a newline indicates the beginning of a new group. For example, Expr "*" Expr | Expr "/" Expr is one group and Expr "+" Expr | Expr "-" Expr is another group. The ordering of groups (from top to bottom) indicates the order of precedence. Hence, * and / have a higher precedence than + and -.
The operators *, /, +, -, &, |, &&, || are left-associative; ; and ==> are right-associative.
In contrast to the grammar for PL0, we use one nonterminal Expr for all expressions. Still, we only admit well-typed expressions in MicroViper programs, where the admissible types are Int and Bool. For example, if x and y are of type Int, then 17 / x + 3 * y is well-typed, whereas x ==> y + 3 is not. When in doubt, you can use Viper to check whether an expression is well-typed.
Every expression of type Bool is a predicate. If the expression does not contain any quantifiers (exists or forall), it is a Boolean expression. Predicates may only appear in assert or assume statements as well as in the annotations requires, ensures, and invariant. Boolean expressions can also appear in assignments and as guards of conditionals and loops.
Variables bound by quantifiers must be distinct from all program variables.
Identifiers are used correctly (e.g., identifiers representing functions do not appear left of assignments).
All identifiers representing method and function names must be pairwise distinct from all other identifiers.
The names of all variables appearing in a method (either as parameters or as locally declared variables) must be pairwise distinct.
Variables are not allowed to be used before they are declared.
A method's input parameters (first list Vars in the grammar) are read-only; its output parameters (second list Vars in the grammar) are read-write but have no initial values.
Output parameters may not appear in a method's precondition.
Function calls are expressions and can appear in expressions.
Method calls are statements. They may not appear in expressions. If the list of output parameters of a method is non-empty, then a method call must assign every output parameter to a variable. For example, x, y, z := callMethodWithThreeOutputs().

02245 - Program Verification - Fall 2022