[comp.software-eng] ProCoS Symposium, 14-18 October, Gl. Avernaes, Denmark

bowen@prg.ox.ac.uk (Jonathan Bowen) (03/12/91)

               ****************************************
               *           ProCoS Symposium           *
               * 14-18 October, Gl. Avernaes, Denmark *
               ****************************************


[ProCoS - Provably Correct Systems - is an Esprit Basic Research
Action project, no. 3104, supported in part by the CEC.]


You are kindly invited to attend the first ProCoS Symposium.  It is to
be held 14-18 October, 1991, at Gl. Avernaes Conference Center,
Denmark.


Symposium Theme
===============

The objective of the ProCoS project is to contribute (i) to the
mathematical foundations for the understanding and development of, and
(ii) to the methodological principles, techniques, notations and tools
needed to develop embedded, real-time systems.

These systems are  concurrent and time-critical.  ProCoS therefore
emphasizes parallelism and time in all its work: from application
development to base systems software (compilers and kernels).

The focus for (i) and (ii) spans from mathematical models of the
problem domain proper, via provably correct development of
(applications) software [to control and monitor the problem], to
provably correct compilers and operating system like kernels for the
compilation of developed programs, respectively the execution of
compiled code.

The ProCoS Symposium will present results of the first 30 ProCoS
project months in both areas (i+ii).

With respect to (ii) the ProCoS Symposium will present programming
methodology results in the following areas.

* The provably correct development of application specific embedded,
real-time systems.

* The underlying (ProCoS) requirements definition, functional
specification, parallel programming and transputer-based machine
languages, and transformations between them.

Thus the ProCoS Symposium will cover facets of design calculi,
verification rules and compiling specification.

* The provably correct development of a ProCoS compiler and a
ProCoS run-time system kernel for a transputer architecture.


With respect to (i) the ProCoS Symposium will present computer science
results wrt.:

* theoretical foundations for (a) the semantics of requirements
definition, component specification, parallel programming and
transputer machine languages, (b) the design calculus for transforming
specifications into parallel programs, such programs into transputer
code, and (c) the proof techniques for arguing correctness of run-time
kernel system implementations.


The ProCoS Consortium
=====================

The ProCoS project is conducted by the following groups and has
included the following staff:

* Department of Computer Science, Technical University of Denmark,
Lyngby:  D. Bjorner, M.R. Hansen, K.M. Jensen, H.H. Lovengreen,
J. Nordahl, W. Pawlowski, A.P. Ravn, H. Rischel, J. Sogaard-Andersen,
E.V. Sorensen, Zhou ChaoChen


* Institute for Informatics, Kiel University, Germany:  B. Buth,
K-H. Buth, M. Franzle, B.von Karger, Y. Lackneche, H. Langmaack,
M. Muller-Olm, D. Weber-Wulff

* Programming Research Group, Oxford University, England:  J. Bowen,
S. Brien, He JiFeng, C.A.R. Hoare, Paritosh Pandya, A. Sampaio

* Institute for Informatics, Oldenburg University, Germany:
E.-R. Olderog, S. Rossig, M. Schenke

* Department of Computer Science, Aarhus University, Denmark:
A. Gammelgaard, Fl. Nielson, H. Riis Nielson, B. Steffen

* Department of Computer Science, Royal Holloway and Bedford New
College, London University, England:  U. Martin, P. Mukherjee,
V. Stavridou

* Department of Computer Science, Manchester University, England:
H. Barringer, D. Edwards, B.Q. Monahan



Symposium Seminar Overview
==========================

The Symposium has 3 parts:

* Developing Embedded, Real-time Computing Systems:  Requirements
Capture, Specification and Transformation to Programs

Monday 14 October, 1991

* Interfaces between Languages for Concurrent Systems:  Programming
Language Semantics and Calculi

Tuesday & Wednesday 15-16 October, 1991

* Base Systems Development:  Compiler and Kernel Development

Thursday, resp. Friday 17-18 October, 1991


Each part has slightly overlapping target audiences:

* Developing Embedded, Real-time Computing Systems:  Practising
software designers  and engineers, who are developing systems where
control and safety requirements involve interfaces to non-computer,
technology components.

* Interfaces between Languages for Concurrent Systems:  Computer and
computing scientists.

* Base Systems Development: Researchers and software engineers in
research departments of universities, the electronics industry, the
software houses and the computer manufacturers - people who are
investigating development of compilers and operating system kernels.


Seminar Program
===============

Sunday, October 13, 1991:             Arrival before Dinner, 18:30-20:00

20:00-21:00: Overview of the ProCoS project                   D. Bjorner

Reception:                                                   21:00-22:30


Monday, October 14, 1991
------------------------

9:00-9:45:  Embedded, Real-time Computing Systems         Anders P. Ravn

9:45-10:45: Requirements and Design Specifications          Hans Rischel

Refreshment Break:                                            30 minutes

11:15-12:00: Component Specifications                     Anders P. Ravn

Lunch:                                                           2 hours

14:00-14:45: Program Specification                   Kirsten Mark Jensen

14:45-15:30: Program Development                       Wieslaw Pawlowski

Refreshment Break:                                            30 minutes

16:00-16:45: A Detailed Case Study                   Kirsten Mark Jensen

16:45- 17:30: Dependability                           Erling V. Sorensen

Dinner:                                                      18:30-20:00


Tuesday, October 15, 1991
-------------------------

9:00-9:30: Language Interfaces                     Ernst Rudiger Olderog
           Languages for Concurrent Systems

9:30-10:30: Specification-oriented Semantics                   He JiFeng

Refreshment Break:                                            30 minutes

11:00-12:00: The Specification Language SL0        Ernst Rudiger Olderog

Lunch:                                                           2 hours

14:00-14:30: The Programming Language PL          Hans Henrik Lovengreen

14:30-15:30: The Satisfaction Relation "sat"       Ernst Rudiger Olderog
             - and the Mixed Term Language 

Refreshment Break:                                            30 minutes

16:00-16:45: Correct Transformations I                    Stephan Rossig

16:45-17:30: Correct Transformations II                  Michael Schenke

Dinner:                                                      18:30-20:00


Wednesday, October 16, 1991
---------------------------

9:00-9:45: The Machine Language - ML                      Jonathan Bowen

9:45-10:30: Correct Compiling Specification                    He JiFeng

Refreshment Break:                                            30 minutes

11:00-11:20: Summary of Language Interfaces                   Tony Hoare

11:20-12:00: Open Issues                                      Discussion

Lunch:                                                 1 hour 30 minutes

13:30-19:00:           Excursion - the ``South Sea Islands'' Archipelago

Dinner:                                                      19:30-21:00


Thursday, October 17, 1991
--------------------------

9:00-10:00: The Compiler Development Method          Burghard von Karger

10:00-10:30: Proven Correct Front-End Specification  Deborah Weber-Wulff

Refreshment Break:                                            30 minutes

11:00-12:00: Proven Correct Compiling Specification    Markus Muller-Olm
             for the Compiler Implementation Language   & Martin Franzle

Lunch:                                                           2 hours

14:00-14:45: Bootstrapping                                Martin Franzle
             Enhanced Compiling Verification

14:45-15:30: Compiler Implementation                        Bettina Buth

Refreshment Break:                                            30 minutes

16:00-16:45: Rapid Compiler Implementation                Jonathan Bowen

16:45-17:30: Summary of Compiler Development              Hans Langmaack

Banquet: Falsled Inn                                         19:00-23:00


Friday, October 18, 1991
------------------------

9:00-9:30: System Verification                    Hans Henrik Lovengreen
           Operational Approach to Compiling and Kernel Verification

9:30-10:15: Compiling Verification                    Anders Gammelgaard
            - the Operational Approach

Refreshment Break:                                            30 minutes

10:45-11:45: Kernel Development                  Jorgen Sogaard-Andersen

11:45-12:00: Summary of Kernel Development        Hans Henrik Lovengreen

Lunch:                                                           2 hours

14:00-14:45: Advanced topic 1

14:45-15:30: Advanced topic 2

Refreshment Break:                                            30 minutes

16:00-17:00: Summary of ProCoS Project      Dines Bjorner and Tony Hoare

Dinner:                                                      18:30-20:00


Saturday, October 19, 1991:                   Departure after breakfast.


The above tentative programme may be subject to small changes.


Gl. Avernaes
============

Gl. Avernaes is a charming, very comfortable, residential conference
center. It is set on the shore of a small peninsula - Helnaes - in
the midst of the lovely rolling landscape of Funen and its ``South See
Island'' archipelago. Besides very adequate lecture and discussion
rooms, the center offers indoor leisure sports facilities, many cosy
lounges, with fine Danish beer, and a fine kitchen - all set in a
beautiful blend of old and modern Danish architecture.



Fees
====

  Symposium Fee                                              1200 DKr.

  Single room and board                                      3900 DKr.
  Single, modern room with shower, all meals, all refreshments

  Banquet                                                     650 DKr.

  Excursion                                                   250 DKr.

                                                             =========

  Total:                                                     6000 DKr.

As of ultimo January 1991 $1 US is approximately 5.7 DKr., 1 UK pound
is approximately 11.2 DKr., 1 DMK is approximately 3.8 DKr.


Hand-outs
=========

Participants will receive extensive documentation in the form of draft
copies of 4 technical/scientific monographs (approximately 1000 pages)
which the project intends to publish in the summer of 1992.


For More Information
====================

Write, call, e-mail, phone, fax or telex us - and we will provide you
with a detailed description of the contents of each of the lectures -
in the form of the synopsis for 3 of the 4 technical/scientific
monographs.


Reports
=======

By contacting Mrs. Annie Rasmussen at the ID/DTH address given below
you may be able to obtain a copy of: ID/DTH DB 8/5, 30 June 1990, D.
Bjorner: ProCoS Interim Deliverable, a 57 page overview of 80 reports.


Symposium Secretariat
=====================

Please write, FAX, e-mail, or phone:

Mrs. Annie Rasmussen                                  Fax: +45-42-884530
Dept. of Comp. Sci., Bldg. 344                      Phone: +45-45-933332
Techn. Univ. of Denmark                         E-mail: procos@id.dth.dk
DK-2800 Lyngby, Denmark                           Telex: 37529 dthdia dk


------------------------ LaTeX version follows. ------------------------

\documentstyle[12pt]{article}

\oddsidemargin 1pt
\evensidemargin 1pt
\marginparwidth 30pt
\topmargin 1pt
\headheight 1pt
\headsep 1pt
\footskip 24pt
\textheight 650pt
\textwidth 460pt

\newcommand{\procos}{{\sc ProCoS}}
\newcommand{\proj}{{\sc \procos\ Project}}
\newcommand{\symp}{{\sc \procos\ Symposium}}

\title{\hfill {\huge ProCoS}\thanks{{\bf ProCoS}--- 
Provably Correct Systems --- is an Esprit Basic Research Actions
project, no. 3104, supported in part by the CEC.}\\
      \hfill Symposium\\
      \hfill 14--18 October, \\ \hfill Gl.\ Avern{\ae}s, Denmark}

\author{}
\date{}


\begin{document}

\maketitle

\begin{abstract} \noindent
You are kindly invited to attend the first \procos\ Symposium.
It is to be held October 14--18, 1991, at Gl.\ Avern{\ae}s
Conference Center, Denmark.
\end{abstract}


\section{Symposium Theme}

The objective of the \proj\ is to contribute (i) to the mathematical
foundations for the understanding and development of, and (ii) to the
methodological principles, techniques, notations and tools needed to
develop {\em embedded, real-time systems\/}.

These systems are  concurrent and time-critical.  \procos\ therefore
emphasizes parallelism and time in all its work: from application
development to base systems software (compilers and kernels).

The focus for (i) and (ii) spans from mathematical models of the
problem domain proper, via provably correct development of
(applications) software [to control and monitor the problem], to
provably correct compilers and operating system like kernels for the
compilation of developed programs, respectively the execution of
compiled code.

The \symp\ will present results of the first 30 \proj\ months in both
areas (i+ii).

With respect to (ii) the \symp\ will present programming methodology
results in the following areas.

\begin{itemize}

\item The provably correct development of application specific
embedded, real-time systems.

\item The underlying (\procos) requirements definition, functional
specification, parallel programming and transputer-based machine
languages, and transformations between them.

Thus the \symp\ will cover facets of design calculi, verification rules
and compiling specification.

\item The provably correct development of a \procos\ compiler and a
\procos\ run-time system kernel for a transputer architecture.

\end{itemize}

With respect to (i) the \symp\ will present computer science results
wrt.:

\begin{itemize}

\item theoretical foundations for (a) the semantics of requirements
definition, component specification, parallel programming and
transputer machine languages, (b) the design calculus for transforming
specifications into parallel programs, such programs into transputer
code, and (c) the proof techniques for arguing correctness of run-time
kernel system implementations.

\end{itemize}

\section{The ProCoS Consortium}

The ProCoS project is conducted by the following groups and has
included the following staff:

\begin{itemize}

\item {\sc Department of Computer Science, Technical University of 
Denmark, Lyngby:}
D.\ Bj{\o}rner, 
M.R.\ Hansen,
K.M.\ Jensen, 
H.H.\ L{\o}vengreen,
J.\ Nordahl,
W.\ Paw{\l}owski,
A.P.\ Ravn,
H.\ Rischel,
J.\ S{\o}gaard-Andersen,
E.V.\ S{\o}rensen,
Zhou ChaoChen


\item {\sc Institute for Informatics, Kiel University, Germany:}
B.\ Buth,
K-H.\ Buth,
M.\ Fr{\"a}nzle,
B.von Karger,
Y.\ Lackneche,
H.\ Langmaack,
M.\ M{\"u}ller-Olm,
D.\ Weber-Wulff

\item {\sc Programming Research Group, Oxford University, England:}
J.\ Bowen,
S.\ Brien,
He JiFeng,
C.A.R.\ Hoare,
Paritosh Pandya,
A.\ Sampaio

\item {\sc Institute for Informatics, Oldenburg University, Germany:}
E.-R.\ Ol\-de\-rog,
S.\ R{\"o}ssig,
M.\ Schenke

\item {\sc Department of Computer Science, {\AA}rhus University, 
Denmark:}
A.\ Gammelgaard,
Fl.\ Nielson,
H.\ Riis Nielson,
B.\ Steffen

\item {\sc Department of Computer Science, Royal Holloway and Bedford 
New College, London University, England:}
U.\ Martin,
P.\ Mukherjee,
V.\ Stavridou

\item {\sc Department of Computer Science, Manchester University, 
England:}
H.\ Barringer,
D.\ Edwards,
B.Q.\ Monahan

\end{itemize}


\newpage

\section{Symposium Seminar Overview}

The Symposium has 3 parts:

\begin{enumerate}

\item {\bf Developing Embedded, Real-time Computing Systems:} 
Requirements Capture, Specification and Transformation to Programs

Monday 14.\ October, 1991

\item {\bf Interfaces between Languages for Concurrent Systems:}
Programming Language Semantics and Calculi

Tuesday--Wednesday 15.--16.\ October, 1991

\item {\bf Base Systems Development:}
Compiler and Kernel Development

Thursday, resp.\ Friday 17.--18.\ October, 1991

\end{enumerate}

\noindent
Each part has slightly overlapping target audiences:

\begin{enumerate}

\item {\sc Developing Embedded, Real-time Computing Systems:}
Practising software designers  and engineers, who are developing
systems where control and safety requirements involve interfaces to
non-computer, technology components.

\item {\sc Interfaces between Languages for Concurrent Systems:}
Computer and computing scientists.

\item {\sc Base Systems Development:} Researchers and software
engineers in research departments of universities, the electronics
industry, the software houses and the computer manufacturers --- people
who are investigating development of compilers and operating system
kernels.

\end{enumerate}

\section{Seminar Program}

\begin{description}

\item[Sunday, October 13, 1991]:
\hfill Arrival before Dinner, 18:30--20:00

\begin{description}

\item[20:00--21:00]: Overview of the \procos\ project \hfill D.\ Bj{\o}rner

\item[Reception]: \hfill 21:00--22:30

\end{description}


\item[Monday, October 14, 1991]:

\begin{description}

\item[9:00--9:45]:  Embedded, Real-time Computing
Systems \hfill Anders P.\ Ravn

\item[9:45--10:45]: Requirements and Design Specifications
 \hfill Hans Rischel

\item[Refreshment Break]: \hfill 30 minutes

\item[11:15--12:00]: Component Specifications \hfill Anders P.\ Ravn

\item[Lunch]: \hfill 2 hours

\item[14:00--14:45]: Program Specification \hfill Kirsten Mark Jensen

\item[14:45--15:30]: Program Development \hfill Wies{\l}aw Paw{\l}owski

\item[Refreshment Break]: \hfill 30 minutes

\item[16:00--16:45]: A Detailed Case Study \hfill Kirsten Mark Jensen

\item[16:45-- 17:30]: Dependability \hfill Erling V.\ S{\o}rensen

\item[Dinner]: \hfill 18:30--20:00

\end{description}

\item[Tuesday, October 15, 1991]:

\begin{description}

\item[9:00--9:30]: Language Interfaces 
\hfill Ernst R{\"u}diger Olderog

Languages for Concurrent Systems

\item[9:30--10:30]: Specification-oriented Semantics \hfill He JiFeng

\item[Refreshment Break]: \hfill 30 minutes

\item[11:00--12:00]: The Specification Language SL$_0$
\hfill Ernst R{\"u}diger Olderog

\item[Lunch]: \hfill 2 hours

\item[14:00--14:30]: The Programming Language PL 
\hfill Hans Henrik L{\o}vengreen

\item[14:30--15:30]: The Satisfaction Relation {\tt sat}
\hfill Ernst R{\"u}diger Olderog

--- and the Mixed Term Language 

\item[Refreshment Break]: \hfill 30 minutes

\item[16:00--16:45]: Correct Transformations I
\hfill  Stephan R{\"o}ssig

\item[16:45--17:30]: Correct Transformations II
\hfill Michael Schenke

\item[Dinner]: \hfill 18:30--20:00

\end{description}

\item[Wednesday, October 16, 1991]:

\begin{description}

\item[9:00--9:45]: The Machine Language --- ML \hfill Jonathan Bowen

\item[9:45--10:30]: Correct Compiling Specification \hfill He JiFeng

\item[Refreshment Break]: \hfill 30 minutes

\item[11:00--11:20]: Summary of Language Interfaces \hfill Tony Hoare

\item[11:20--12:00]: Open Issues \hfill Discussion

\item[Lunch]: \hfill 1$\frac{1}{2}$ hours

\item[13:30--19:00]: Excursion --- the ``South Sea Islands'' Archipelago

\item[Dinner]: \hfill 19:30--21:00

\end{description}

\item[Thursday, October 17, 1991]:

\begin{description}

\item[9:00--10:00]: The Compiler Development Method
\hfill Burghard von Karger

\item[10:00--10:30]: Proven Correct Front-End Specification
\hfill Deborah Weber-Wulff

\item[Refreshment Break]: \hfill 30 minutes

\item[11:00--12:00]:  Proven Correct Compiling Specification
\hfill Markus M{\"u}ller-Olm

for the Compiler Implementation Language
\hfill \& Martin Fr{\"a}nzle

\item[Lunch]: \hfill 2 hours

\item[14:00--14:45]: Bootstrapping
\hfill Martin Fr{\"a}nzle

Enhanced Compiling Verification

\item[14:45--15:30]: Compiler Implementation
\hfill Bettina Buth

\item[Refreshment Break]: \hfill 30 minutes

\item[16:00--16:45]: Rapid Compiler Implementation
\hfill Jonathan Bowen

\item[16:45--17:30]: Summary of Compiler Development \hfill Hans
Langmaack

\item[Banquet]: Falsled Inn \hfill 19:00--23:00

\end{description}

\item[Friday, October 18, 1991]:

\begin{description}

\item[9:00--9:30]: System Verification
\hfill Hans Henrik L{\o}vengreen

Operational Approach to Compiling and Kernel Verification

\item[9:30--10:15]: Compiling Verification
\hfill Anders Gammelgaard

-- the Operational Approach

\item[Refreshment Break]: \hfill 30 minutes

\item[10:45--11:45]: Kernel Development
\hfill J{\o}rgen S{\o}gaard-Andersen

\item[11:45--12:00]: Summary of Kernel Development
\hfill Hans Henrik L{\o}vengreen

\item[Lunch]: \hfill 2 hours

\item[14:00-14:45]: Advanced topic 1

\item[14:45-15:30]: Advanced topic 2

\item[Refreshment Break]: \hfill 30 minutes

\item[16:00--17:00]: Summary of \procos\ Project
\hfill Dines Bj{\o}rner and Tony Hoare

\item[Dinner]: \hfill 18:30--20:00

\end{description}

\item[Saturday, October 19, 1991]: Departure after breakfast.

\end{description}

The above tentative programme may be subject to small changes.

\section{Gl.\ Avern{\ae}s} 

Gl.\ Avern{\ae}s is a charming, very comfortable, residential
conference center. It is set on the shore of a small peninsula ---
Heln{\ae}s --- in the midst of the lovely rolling landscape of Funen
and its ``South See Island'' archipelago. Besides very adequate lecture
and discussion rooms, the center offers indoor leisure sports
facilities, many cosy lounges, with fine Danish beer, and a fine
kitchen --- all set in a beautiful blend of old and modern Danish
architecture.


\newpage

\section{Fees}

\begin{itemize}

\item Symposium Fee \hfill 1200 DKr.

\item Single room and board  \hfill 3900 DKr.

Single, modern room with shower, all meals, all refreshments

\item Banquet \hfill 650 DKr.

\item Excursion \hfill 250 DKr.

\item[] \hfill \ldots\ldots\ldots

\item Total: \hfill 6000 DKr.

\end{itemize}

\noindent
As of ultimo January 1991 \$1 US is approximately 5.7 DKr., \pounds1
is approximately 11.2 DKr., 1 DMK is approximately 3.8 DKr.

\section{Hand-outs}

Participants will receive extensive documentation in the form of draft
copies of 4 technical/scientific monographs (approximately 1000 pages)
which the project intends to publish in the summer of 1992.

\section{For More Information}

Write, call, e-mail, phone, fax or telex us --- and we will provide
you with a detailed description of the contents of each of the
lectures --- in the form of the synopsis for 3 of the 4
technical/scientific monographs. 

\section{Reports}

By contacting Mrs.\ Annie Rasmussen at the ID/DTH address given below
you may be able to obtain a copy of: {\em ID/DTH~DB~8/5, 30 June 1990,
D.\ Bj{\o}rner: ProCoS Interim Deliverable,\/} a 57 page overview of 80
reports.


\section{Symposium Secretariat}

Please write, FAX, e-mail, or phone:

\vspace*{4mm}

Mrs.\ Annie Rasmussen \hfill Fax: +45 42\,884530

Dept.\ of Comp.\ Sci., Bldg. 344 \hfill Phone: +45 45\,933332

Techn.\ Univ.\ of Denmark \hfill E-mail: procos@id.dth.dk

DK-2800 Lyngby, Denmark \hfill Telex: 37529 dthdia dk

\end{document}


--
Jonathan Bowen, <Jonathan.Bowen@prg.oxford.ac.uk>
Oxford University Computing Laboratory.