Institute of Computer Languages
Compilers and Languages Group

Talks 2012 - Kokichi Futatsugi

Der Arbeitsbereich für Programmiersprachen und Übersetzer am Institut für Computersprachen lädt zu folgender 4-teiliger Vortrags- und Tutoriumsreihe ein:

Kokichi Futatsugi, Prof. Dr.

Japan Advanced Institute of Science and Technology (JAIST)
Nomi, Ishikawa, Japan

über

INTRODUCTION TO SPECIFICATION AND VERIFICATION IN CafeOBJ

Datum: Mittwoch, 18. Juli 2012
Vortrag: 10:00 - 11:30
Übung: 14:00 - 15:30
Thema: Basics of CafeOBJ and Peano Style Natural Numbers

Datum: Mittwoch, 25. Juli 2012
Vortrag: 10:00 - 11:30
Übung: 14:00 - 15:30
Thema: Parametrized Modules and Generic List Structure

Datum: Mittwoch, 1. August 2012
Vortrag: 10:00 - 11:30
Übung: 14:00 - 15:30
Thema: Definition of the Minila Programming Language and its Interpreter and Virtual Machine

Datum: Mittwoch, 8. August 2012
Vortrag: 10:00 - 11:30
Übung: 14:00 - 15:30
Thema: Compiler of Minila and its Verification with Proof Scores

Alle Vorträge finden statt in der Argentinierstraße 8, 4. Stock (Mitte), Bibliothek E185.1

Course Material: Lecture notes and slides, the CafeOBJ system, code examples, and more, can be downloaded at the homepage of the course at http://www.jaist.ac.jp/~kokichi/class/TUW1207+08/

Zusammenfassung:

After introductory explanations of the CafeOBJ algebraic specification language system, the lectures gradually develop executable algebraic semantics (or specifications) of a simple imperative programming language called Minila. The semantics/specifications are composed of that of an interpreter of Minila, an abstract machine, and a compiler from Minila to machine codes of the abstract machine. A verification of a part of the compiler is also given.

The lectures are prepared for the beginners for CafeOBJ and only fundamental knowledge of algorithms and data structures, automata and languages, elementary mathematical logic are assumed. The lectures are also designed to be combined with interactive exercises with the CafeOBJ language system, and all attendees are expected to bring in their personal computers to class room. After attending the lectures, the attendees are expected to be able to construct elementary formal semantics/specifications in CafeOBJ and write proof scores for verifying properties about the semantics/specifications.

Kurzbiographie von Kokichi Futatsugi

Kokichi Futatsugi has been a professor of JAIST since 1993. Before getting a full professorship at JAIST, he worked at ETL (Electrotechnical Laboratory), MITI (Ministry of International Trade and Industry), Japanese Government and was appointed the Chief Researcher of ETL in 1992. He worked also at SRI International (Stanford Research Institute), California for 1983-1984 as a visiting researcher. His research interests include formal specification languages, formal methods, systems verifications, software requirements/specifications, and his current research activities are centered around formal specification and verification based on CafeOBJ (an executable formal specification language). He got a Fellow Award of Japan Society for Software Science and Technology in 2008, and is now adviser/editor of international journals like IJSI (www.ijsi.org), JAL (www.elsevier.com/locate/jal), and JHOSC(www.springerlink.com/content/102420/).
(http://www.jaist.ac.jp/~kokichi/)

Sie möchten auf diese Vortragsreihe durch Aushang hinweisen? Eine druckfertige Einladung im pdf-Format dafür finden Sie hier.

Complang
   About Us
   Research
   Lehre
   Service
      Robotics
      Library
      Talks 2017
      Talks 2016
      Talks 2015
      Talks 2014
      Talks 2013
      Talks 2012
      Talks 2011
      Talks 2010
      Talks 2009
      Talks 2008
      Talks 2007
      Talks 2006
      Talks 2005
      Talks 2004
Sitemap
Contact
Fast Access:
Previous Talk
Next Talk
Faculty of Informatics
Vienna University of Technology
top | HTML 4.01 | last update: 2017-02-13 (Webmaster)