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.