ARW-96

The Fifth Australasian Refinement Workshop

Held at the Software Verification Research Centre

The University of Queensland

on

9th and 10th April, 1996

Tuesday 9th April 1996

09:00

Registration, Coffee, Introduction

09:30

Refinement and Implementation in the B-Method

Ken Robinson and John Zic, UNSW

Program Refinement with Structure Diagrams

Lindsay Groves VUW, NZ (lindsay@comp.vuw.ac.nz)

10:30

Morning Tea/Coffee

11:00

Criteria by Calculation

Brendan Mahony, DSTO, Canberra (Brendan.Mahony@dsto.defence.gov.au)

Infinite Lists for Specifying Functional Programs in Z

Andrew Martin, SVRC, UQ (apm@cs.uq.edu.au)

Additional notes

Refining specifications to logic programs

Ian Hayes (Ian.Hayes@cs.uq.edu.au) and

Paul Strooper, UQ

12:30

Lunch - UQ Staff and Graduates Club

14:00

The CARE toolset for developing verified programs from formal specifications

David Hemer and Peter Lindsay (hemer,pal@cs.uq.edu.au) SVRC, UQ

CARE: Development of a Parser

Keith Harwood (keithh@tplrd.tpl.oz.au)

The Data Logger case study in CARE

Peter Lindsay SVRC, UQ (pal@cs.uq.edu.au)

15:30

Afternoon Tea/Coffee

16:00

Refinement in a Type Extension Context

Peter Bancroft, Queensland University of Technology (p.bancroft@qut.fit.edu.au) and

Ian Hayes UQ (Ian.Hayes@cs.uq.edu.au)

All refinements big and small

Martin Schwenke ANU (Martin.Schwenke@anu.edu.au) and

Ken Robinson, UNSW

17:00

Free time

19:00

Dinner:

Baan Thai BYO

Park Road

Milton

Wednesday 10th April 1996

 
09:00

`Real-time refinement: A transmitter example`

`Ian Hayes (Ian.Hayes@cs.uq.edu.au) and`

`Mark Utting (marku@cs.uq.edu.au), UQ`

`PICTCalc - a tool for program development in constructive type theory`

`Steve Reeves, Waikato, NZ (stever@waikato.ac.nz)`

`Eliminating intermediate data structures by data refinement`

`Lindsay Groves VUW, NZ (lindsay@comp.vuw.ac.nz)`

10:30

Morning Tea/Coffee

11:00

`Formal Development of a Digital Multiplexed Radio-Telephone System`

`Roderick Durmiendo, Advanced Science and Technology Institute, Manila`

`(ericd@asti.dost.gov.ph)`

`Chris George, United Nations University International Institute for Software Technology, Macau`

`The Quartz refinement method for real-time multi-tasking systems`

`Colin Fidge (cjf@it.uq.edu.au),`

`Mark Utting (marku@it.uq.edu.au),`

`Ian Hayes (Ian.Hayes@it.uq.edu.au)`

`and`

`Peter Kearney SVRC, UQ`

`Applying refinement in an industrial pilot project using Cogito`

`Tracey Hart, CSC Australia, Peter Kearney, SVRC, UQ,`

`Kelvin Ross (kjross@cs.uq.edu.au), SVRC, UQ, Owen Traynor, SVRC, UQ`

12:30

Lunch - UQ Staff and Graduates Club

14:00

`An Architecture for a Unified Refinement/Proof Tool`

`Mark Utting (marku@cs.uq.edu.au), SVRC, UQ`

`Flexible interactive transformational reasoning`

`Mark Staples Cambridge, UK (Mark.Staples@cl.cam.ac.uk)`

`Window Inference for Data Refinement`

`Ray Nickson SVRC, UQ (nickson@cs.uq.edu.au)`

15:30

Afternoon Tea/Coffee

16:00

Discussion: The future of the Refinement Workshop