*******************************************************************************

+++ Computer Science Seminar in Kiryu +++

Programme

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)

Abstract: 
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
programs.

*******************************************************************************
Access to Kiryu campus, Gunma University:
   http://www.st.gunma-u.ac.jp/other/14.html

Map of Kiryu campus:
   http://www.st.gunma-u.ac.jp/other/13.html

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).
-------------------------------------------------------------------------------