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