Institute of Computer Languages
Compilers and Languages Group
über
| 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/
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.
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.