Sophie Lathouwers

Hi! I've been following the documentation to migrate a project but I'm running into a problem in the final step. The project consists of a core project which depends on...

Empty conditions generated

1

Hi! I've been trying to run Toradocu on some of my examples to generate specifications but unfortunately it doesn't seem to generate any useful conditions or properties. All of the...

\result may not occur in the postcondition of a constructor?

1

The following program does not verify: ``` public class Purse { private int balance; /*@ context Perm(balance, write); @ ensures balance == 0; @*/ public Purse() { balance = 0;...

Verification result is confusing when there are expected errors

1

Currently, you can indicate whether you expect certain errors in a file that you verify. If you then verify the program, it'll tell you that the verification was succesful if...

Add PreconditionUnsatisfied to "What does this VerCors error message mean?"

1

It would be good to add an explanation of this error to the page that describes all the common VerCors error messages.

Find out which backends are still supported

4

Currently we are always using the silicon backend to verify our programs. However, we used to also support backends such as Dafny, Chalice and Boogie. We need to figure out...

Updated paper titles + last activity dates using ProVerBMate

1

This adds paper titles where there was only a DOI and updates the last activity dates for repositories. The changes are all generated using ProVerBMate. The 'last activity' date specifically...