(* Apologies for any cross-postings. *)

皆様，

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

問い合わせ先： 藤田 憲悦 [email protected]

*********************************************************************** +++++ 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: [email protected] (Ken-etsu Fujita, Gunma University) -----