[logic-ml] CSセミナーin桐生

[Fujita Kenetsu]

(* Apologies for any cross-postings. *)

皆様，

群馬大学の藤田と申します．
コンピュータ・サイエンスのセミナーのご案内です．
どなたでも参加できますので，どうぞお気軽にお越し下さい．

問い合わせ先：
藤田 憲悦
fujita at cs.gunma-u.ac.jp

***********************************************************************
+++++ CS seminar in Kiryu: Programme +++++

URL:
 http://www.cs.gunma-u.ac.jp/~fujita/research/20140918Seminar.html

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

Title:
"Verification of programs using Frama-C and Why3"

Speaker:
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:
fujita at cs.gunma-u.ac.jp (Ken-etsu Fujita, Gunma University)
-----