Workshop on Refinement and Abstraction

Workshop on Refinement and Abstraction

[HAGIYA Masami]

                        CALL FOR PARTICIPATION


                Workshop on Refinement and Abstraction

                           Nov 15-17, 1999

                              ETL Osaka
                                Japan

                http://www.etl.go.jp/~yoshiki/RAW.html


Refinement has become an important research field in computer science.
It was first proposed in the engineering context of verification of
large scale programs, or "verification in the large."  The idea was to
put together a proof that a program behaves correctly assuming the
correctness of the library modules in use and a correctness proof of
those modules, obtaining a full proof of program correctness.  There
have been scientific attempts to analyse refinement using universal
algebra, relational algebra and lattice theory.  In the late 90's,
those mathematical tools have extended to category theory, and a
deeper connection with traditional programming semantics is now being
sought.

On the other hand, the programming technique called "abstract
interpretation" has turned out to be useful for software verification.
It has led to a hybrid method called abstract model checking, which is
an amalgamation of the deductive formal proof method and model
checking.  In particular, abstraction is useful in reducing the number
of states of a transition system, making model checking more tractable
in many cases.

The words "refinement" and "abstraction" sound as though they have
opposite directions.  The two approaches, however, seem to have much
in common.  For instance, transformations between two models (an
"abstract" model and "concrete" model) play an essential role in both
methods.  The aim of this workshop is to provide an opportunity for
people working in refinement and abstraction to get together and to
learn how the two fields are related.  To that end, we shall limit the
number of attendants (to about 30 people) for economy of
communication.

We plan to publish an after-meeting-booklet containing articles
related to the talks given in the workshop.

Invited speakers:

        Ralph-Johan Back (Abo Akademi University, Turku)
        Patrick Cousot (ENS, Paris)
        He Jifeng (United Nations University, Macau)
        David Schmidt (Kansas State University)
        Bernhard Steffen (University of Dortmund)
	Akira Mori (JAIST, Japan)

Accommodation.

	For participants of this workshop, Hotel New Archaic, where
	the workshop will be held, offers the following special rate.

                Single room :  7,000 Yen(+SVC,TAX)
                Twin room :   12,000 Yen(+SVC,TAX)

                Breakfast :    1,400 Yen(+SVC,TAX) extra

	To get this rate, you need to book BY E-MAIL, BEFORE Friday 29
	October, 1999, with the explicit statement that you are to
	participate the Workshop on Refienemnt and Abstraction
	sponsored by ETL.

	E-mail address for booking: archaic@mxq.mesh.ne.jp 

	There are some non-smoking rooms but the numberis limited.
	So, quick reservation would be recommended if you need it.

Organisers:

        Yoshiki Kinoshita (ETL Osaka)
        Masami Hagiya (University of Tokyo)
        A. John Power (University of Edinburgh)

Place:
 
	Hotel New Archaic
	2-7-1 shouwadouri, Amagasaki-shi, Hyogo 660-0881
	Tel:+81-6-6488-7777, Fax:+81-6-6488-0700

	Hotel New Archaic is situated to the northeast of Hanshin
	Amagasaki Station along Route 2.  It takes ca. 6-minutes on
	foot from Hanshin Amagasaki Station.

Sponsor:

        ETL (Centre Of Excellence Project---Global Information
        Processing Technology)

Tentative Program:

        See http://www.etl.go.jp/~yoshiki/RAW.html
        for the abstracts of the talks.

Monday, Nov 15

2:00 -- 3:00

He JiFeng
Refinement Induces the Enriched Semantics of Programming Languages (invited)

3:00 -- 3:30 break

3:30 -- 4:15

Koichi Takahashi
Valid Abstract Model Checking of Safety Property

4:15 -- 5:00

Yoshiki Kinoshita
Refinement and Free Extension of Simulations

Tuesday, Nov 16

9:30 -- 10:30

Bernhard Steffen
Dataflow Analysis as Model Checking of Abstract Interpretations (invited)

10:30 -- 11:00 break

11:00 -- 12:00

Akira Mori
A Behavioral Model Checker for CafeOBJ (invited)

12:00 -- 13:30 lunch

1:30 -- 2:15

Mitsuharu Yamamoto
On Formal Verification of Graph Search Algorithms and Its Application
to Model Checking

2:15 -- 3:00

Akihiko Takano
Nested Datatypes and Program Fusion

3:00 -- 3:30 break

3:30 -- 4:30

Patrick Cousot
Abstraction in abstract interpretation (invited)

4:30 -- 5:00 break

5:00 -- 5:30 business meeting

6:00 --      workshop dinner

Wednesday, Nov 17

9:30 -- 10:30

Ralph-Johan Back
Refinement of interactive and concurrent systems (invited)

10:30 -- 11:00 break

11:00 -- 11:45

Furusawa Hitoshi
On Soundness and Compuleteness of Simulations with respect to Refinement

11:45 -- 12:30

Mizuhito Ogawa
Automatic Verification Based on Abstract Interpretation

12:30 -- 2:00 lunch

2:00 -- 3:00

David Schmidt
Properties of Binary Relations for Abstraction and Refinement (invited)

3:00 -- 3:30 break

3:30 -- 5:00 discussions

Registration:

        For registration to the workshop,
        send the following data to Ms. Midoriko Yokoyama by e-mail.
        E-mail : midoriko@etl.go.jp

        - Names in full :
        - Address :
        - Phone/Fax :
        - Oranization :
        - Date of transfer to our bank :

        Registration fee is 10,000yen that includes:
        - admission to the workshop
        - lunches during the workshop
        - workshop dinner on Nov 16
        - materials distributed during the workshop

        Payments should be made in Yen currency by bank transfer.
        Notice: Registration fee 10,000yen does not include the bank charge.
        (Payments by cash at the registration counter on the first day of
         the workshop are also possible.)

        Bank name : Sakura Bank
        Branch bank name :  Sonoda
        Beneficiciary's name : ETL  YOSHIKI  KINOSHITA
        ID number : 357-4561405 (Ordinary bank account)

For further information, contact:

        Ms. Midoriko Yokoyama

        Osaka LERC
        ETL
        Nakouji 3-11-46
        Amagasaki, Hyogo
        661-0974 Japan

        E-mail: midoriko@etl.go.jp
        Fax: +81-6-6491-5028
        Phone: +81-6-6494-7825