The initial one-day workshop of the Bath-AIST project having been so successful, we decided to hold a second workshop in Bath on 17 September 2008. That allowed us to take advantage of the presence in Bath of other closely related researchers from Swansea, who were willing to speak at the seminar.
.Prof James Davenport
.Prof Guy McCusker
.Prof David Pym
.Dr John Power
.Dr Jim Laird
.Dr Paola Bruscoli
.Ms Ana C.M. Abbud
.Mr Martin Churchill
.Dr Keishi Okamoto
.Dr Shunsuke Yatabe
In Rm 6E 2.2
11:15 Peter Mosses: Implicit Propagation in SOS
1:30 Keishi Okamoto: Formalization of System LSI Specification and Automatic Generation of Verification Items
Abstract:The design process of a system LSI traditionally starts with
an informal specification in a combination of a natural language and
some pseudo programming language such as a pseudo C. This informal
specification is used to generate items for verification of
lower-level detailed designs. Engineers generating those verification
items often face the problems of informality. Ambiguities, implicit
assumptions, inconsistencies, etc. in the specification lead to wrong
verification items or critical omission. Informality means that the
generation is basically a manual process prone to simple errors.
Besides those reliability issues, the cost of manual generation is a
big issue in the productivity of design processes.
We aim at automatic generation of verification items from
specifications. The target specification for this study is that of a
system LSI under development at Renesas Technology Corp.
2:15 Arnold Beckmann and Faron Moller: On the Complexity of Parity Games
3:30 Shunsuke Yatabe: A new project on formalizing specifications
Abstract: In this talk we introduce a new on-going research project (jointly with
several companies) for developing a methodology and software tools that
can improve the upper development scene of software product.
This aims to formalize a unified form of specifications of Embedded
Software in a proof assistant system Agda, and develop tools which
assist in writing such formalized specifications.
4:15 Anton Setzer: Proofs by Guarded Recursion