May 07, 2013: Stefan Blom: Witnesses for Software Verification

May 07, 2013Witnesses for Software Verification
Room: Zi 5126Stefan Blom

The VerCors Tool uses the Chalice tool to verify Java programs, which have been specified in separation logic. Because Separation logic is more expressive than the Chalice specification language, the input has to be encoded in order to allow verification with Chalice.

One of the approaches to translating complex formulas to simpler ones, is to replace a formula written in the specification language, with an object written in the programming language that states the original formula holds. Such an object is called a witness.

In this talk, we will discuss separation logic predicates and magic wands and how they are encoded and verified with witnesses using the VerCors Tool.