Department of Information Technology

Charge! and Kopitiam

Efficient verification of Java-programs using higher-order separation logic in Coq.


Date and Time

Wednesday, May 16th, 2012 at 10:30


Polacksbacken, room 1112


In this talk, we present an Eclipse plugin that allows its users to write, compile, specify, and verify the correctness of a subset of Java-programs. The plugin is split into two parts -- Kopitiam and Charge!. Kopitiam is the Java front-end where the user writes programs and specifications; Charge! is the Coq back-end where the user verifies that the Java-programs conforms to their specifications. Charge! is a collection of tactics for working with a shallow embedding of a higher-order separation logic for a subset of Java in Coq. The tactics make it possible to reason at a level of abstraction similar to pen-and-paper separation-logic proof outlines. In particular, the tactics allow the user to reason in the embedded logic rather than in the concrete model, where the stacks and heaps are exposed. The development is generic in the choice of heap model, and most of the development is also independent of the choice of programming language.

The presentation will be in two parts. The first part covers the theoretical background required for the tactics of Charge!, and the second part is a live demo where we verify the correctness of a few simple Java programs.

Back to the seminar page

Updated  2012-05-04 13:34:01 by Frédéric Haziza.