CW 550

Cedric Cuypers, Bart Jacobs, and Frank Piessens
Verification of data-race-freedom of a Java chat server with VeriFast

Abstract

Even now, when computers have become a vital part of our society, software errors are still common, and their effects can be devastating. From the recent rise of multicores emerged the need for multi-threading software and a way to cope with its typical software errors such as data-races and deadlocks. This paper shows how VeriFast can be used to verify the data-race-freedom of a multi-threaded Java application, by means of a simple Java chat server example. We will cover the verification of jar files in general, how to deal with Java core classes and interfaces such as ArrayList and the specifics of verifying a multi-threaded Java application, using Thread, Runnable and Semaphore as building blocks. To achieve this, we need to take a closer look at VeriFast elements such as predicate families, predicate constructors and fractional permissions. This paper is intended as an experience report. We will conclude with some suggested improvements and possible future work.

report.pdf (192K) / mailto: B. Jacobs