Boogie

Boogie is an intermediate verification language (IVL), intended as a layer on which to build program verifiers for other languages. It is also the name of the verification tool that takes Boogie programs as input. It can accept the input
of a Boogie program and generate verification conditions that are passed to an SMT solver such as Z3 used by my test.

Build and Run

Building this project is very simple, however, we may need to install many other tools such as “Mono” (I use a MacBook to build this project) and “NuGet”. The information of successfully building is like this.

There are two kinds of verifications said by the authors: Driver tests and Unit tests, however, I couldn’t find the python script for the latter, so I just run the driver tests.

Driver Tests

In this kind of tests, we need to use “lit” and “OutputCheck”. We could run all the tests by “lit .”. The result is shown as follows.

We also could run a single test by giving “lit” a specific folder or file. The picture is a test of a folder.

Analyze the Test

The picture is a function written by Boogie, from which we can see that the Boogie language is something like C language. In addition, in every Boogie file, every function is separated.

If there are some errors occurred, there will be a “.expect” file outputted like this to tell us why they are wrong.

Write A Test

We can write a new file or just add our function to a existed file. The following is my test:

This is the result:

I plan to analyze this project deeply, however, its code is very old so it maybe a little difficult for me to do this. I just do these tests on this projects now. Maybe I will analyze the whole project some day. From this project, I can
learn what is an intermediate verification language (IVL) and how it works. I found that there were many tools adapting this strategy, including the VCC and HAVOC verifiers for C and the verifiers for Dafny, Chalice, and Spec#.

本文链接： http://www.meng.uno/articles/4f0a9591/ 欢迎转载！