+++ Computer Science Seminar in Kiryu +++


Thursday, September 18, 2014
14:00--15:30 in the J3 lecture room (the building no. 6 of the map below),
Kiryu campus, Gunma University

"Verification of programs using Frama-C and Why3"

Dr. Aleksy Schubert (The University of Warsaw, Poland)

Frama-C is a tool that makes it possible to do a variety of analyses
for C programs annotated with C specification language called ACSL
(The ANSI/ISO C Specification Language). One of the possible ways to
use Frama-C is to generate verification conditions for appropriately
defined Hoare logic that is in line with C programming language semantics.
These verification conditions can subsequently be discharged
by Why3 tool that makes it possible to manage the proving of
necessary properties. During the talk I will present an overview of
the tools and show a number of interesting examples to demonstrate
how these tools work together to make possible verification of practical

Access to Kiryu campus, Gunma University:

Map of Kiryu campus:

For more information, please contact at the following \beta-normal form:
   (\lambda A. fujitA@cs.gunmA-u.Ac.jp)a

(Ken-etsu Fujita, Gunma University).