[Prev][Next][Index][Thread]

BRICS Autumn School in Verification


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

*************************************************************
 This message is being forwarded on several mailing lists.
 Please excuse receipt of multiple copies and please 
 forward to any colleagues whom it might interest.
*************************************************************



                Preliminary Announcement

                 BRICS Autumn School in 
                    Verification 

            October 28 -- November 2, 1996
                   Aarhus, Denmark


Description
===========

BRICS, centre for  Basic  Research In Computer  Science, was
founded in 1994 by  the Danish National  Research Foundation
at University   of  Aarhus and  University  of  Aalborg; the
director  is  Professor Glynn   Winskel.   Each year,  BRICS
focusses  on a selected theme in  the area of Algorithms and
Complexity Theory, Logic, and Semantics.

This year's BRICS theme is Verification. The activities will
cover verification  of computing  systems in a  broad sense.
More specifically,  we  intend to investigate  specification
formalisms,  proof  principles,  and technology of automated
tools for verification. Events   will take place  during the
autumn of '96.

As  a  special activity, the autumn   school  will cover the
topics

            "Theorem Proving and Model Checking"

with special focus on

 "Combining deductive methods  with model checking techniques"

The contents of the autumn  school will be the  presentation
of a selected set of  tools and principles (theorem provers,
model checkers and combinations) focussing on ``Cutting-Edge
Applications-Oriented    Techniques''.      Lectures     and
presentation   of  the  application of  the   tools  will be
weighted somewhat equally.

The aim of the autumn school is that the participants leave with:

* an understanding of theorem proving and model checking and their
  status, based on our choices of concrete tools

* (hands-on) experience with (state of the art) applications of the
  tools

* a feeling for the advantages and disadvantages of theorem proving vs.
  model checking

* ideas of possibilities of combining theorem proving and model
  checking

* possible research projects (short and long term)

Participants
============

The autumn school is intended to attract Ph.D.  students and
other   researchers.   A  working  knowledge  of  English is
assumed.

We anticipate approximately  30  participants.  Participants
will be selected on  the  basis of their applications   (see
below).   There    is no registration   fee, lunch   will be
provided free, and  BRICS  grants covering  lodging expenses
for attending  students will be available.  Participants are
expected to pay for their own travel.

Program
=======

The invited speakers are

David Basin, Max-Planck-Institut f|r Informatik
Ed Clarke, CMU 
Tom Henzinger, University of California at Berkeley
Gerard Holzmann, Bell Laboratories, USA
Tom Melham, Glasgow
Randy Pollack (likely), Chalmers
Mandayam Srivas, SRI

They intend to cover topics including:

* (automata theoretic) decision procedures

* symbolic   model     checking  (abstraction, compositional
  reasoning, and symmetry)

* theorem proving

* proof checking 

* type theory for representing mathematics

* applications to hardware, real time and hybrid systems

In addition, tools will be presented (including HOL, HyTech,
LEGO, Mona, PVS, SMV, and SPIN) and a panel-discussion among
the invited speakers will  be held at  the end of the autumn
school.

Local arrangements
=================

Lectures  will take  place at   the  Department of  Computer
Science,  University of   Aarhus.   Lodging will be  offered
close to campus and the  city centre.  The city features  an
attractive  old part   with  cafis,  bars, and  restaurants.
Forests,  museums, and  other  attractions  are  within easy
reach by public transport.

An excursion is planned.

Organisers
==========

David Basin, Allan Cheng, Kim  Guldstrand  Larsen, Tom  Melham,   
and Mogens Nielsen.

Application
===========

An  application  should consist  of  a  Curriculum Vitae, at
least one letter of recommendation, and a description---less
than  a   page---of research  interests and accomplishments.
The application should   be  mailed to  the  address  below.
Participants will  be selected  on  basis of  their research
interests and qualifications in the area.

Deadlines
=========

Applications must be received by June 1, 1996.
Answers will be mailed out soon after.

Address
=======

att. Autumn School
BRICS
Department of Computer Science
University of Aarhus
Ny Munkegade, Bldg. 540
DK-8000 Aarhus C
Denmark

Information will also be available on the WWW-page

http://www.brics.dk/Activities/96/Verification/index.html