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