[ut.ee] CMC will sponsor a student to attend VLSI school on Formal Verification

dunc@eecg.toronto.edu (Duncan Elliott) (04/10/89)

Reposted from uw.general.  We probably have some information about
this here at UofT.


Article 757 of uw.general:
Xref: jarvis.csri.toronto.edu junk:10602 uw.general:757
Path: jarvis.csri.toronto.edu!utgpu!watmath!maytag!watvlsi!jabarby
From: jabarby@watvlsi.waterloo.edu (Jim Barby)
Newsgroups: uw.vlsi,uw.general
Subject: CMC will sponsor a student to attend VLSI school on Formal Verification
Message-ID: <4275@watvlsi.waterloo.edu>
Date: 5 Apr 89 23:10:38 GMT
Distribution: uw
Organization: U of Waterloo, Ontario
Lines: 140

The Canadian Microelectronics Corporation will sponser a grad student
from a Canadian University to attend the "VLSI School" on "Formal
Verification Techniques in VLSI design".  The successful candiate's
supervisor will have to pay the first $1,000 and CMC will pay the
balance (of approximately $4,000).  The following is a brief summary of
the course and intent.  For those interested in applying, please contact
myself (jabarby@watvlsi) or Joan Pache (jpache@watvlsi) as we have all
the details and additional information necessary.  I should point out
this is a fantastic opportunity for a PhD student starting to work in the
formal verification area.

                                 Formal Verification
                                    Techniques in
                                     VLSI Design
                                SUMMER SCHOOL IN ITALY

                The Canadian Microelectronics Corporation will sponsor
             a postgraduate student to attend a VLSI summer school to be
               held at the Scuola Superiore G. Reiss Romoli facility in
                        L'Aquila Italy from July 10-14, 1989.


          The primary goal of the Canadian Microelectronics Corporation is
          to create an environment of support for university research and
          scholarship in microelectronics.  The corporation has 28
          university, 9 industrial and 4 federal government members.  The
          International Travel Award program contributes to an
          understanding of the international nature of microelectronics

          A report about the VLSI school will be sent to all members of the
          corporation.  The successful applicant in 1988 was Ralph Mason of
          the Technical University of Nova Scotia who attended a VLSI
          school in Norway, Innovations in VLSI Architecture and Design

          To be eligible, an applicant must be a full-time student in a
          postgraduate degree program in a Canadian University (or similar
          degree-granting institution).  Applications must be received by
          the CMC by April 26, 1989 and notification of decisions is
          scheduled for May 26, 1989.  Application details and procedures
          are available from:

          Prof. J.A. Barby              Canadian Microelectronics Corp.
          jabarby@watvlsi               Queen's University
          Electrical Eng. Dept.         210A Carruthers Hall
                                        Kingston, Ontario
               or                  or   K7L 3N6        Attn:  Janet Tite

          Joan Pache                    CDNnet    : vlsiic@cmc.ca
          jpache@watvlsi                NetNorth  : VLSIIC@QUCDNCMC
          VLSI Group                    ENVOY     : CMC.VLSIIC
          at UofW Ext. 4084             Fax       : (613)548-8104
          (519)888-4084                 Telephone : (613)545-2914

                                        - 2 -


                                   L'Aquila, Italy
                                   July 10-14, 1989

                                CONTENT OF THE COURSE

          The Concept of Formal Verification

          Formal Verification within the scope of Design Automation

          The requirement of Formal Verification:

               -    Formal Representation systems

               -    Automatic Proof Systems

          Formal Description Systems:

               -    Taxonomy

               -    First-Order Logic

               -    Specific Calculi

               -    Higher-Order Logic

               -    Temporal Logic

               -    Functional Languages

          Automatic Proof Systems:

               -    Theorem Provers

               -    Tautology Checkers

          Practical experiences on:

               -    Use of Formal Systems

               -    Use of Theorem Provers

               -    Use of Tautology Checkers

          Verification of Microprogrammable Architectures

          The Industrial Impact of Formal Verification

                                        - 3 -

          The Honeywell-Bull Experience

          Critical Assessment of Formal Verification:
               reality vs. utopia, applicability and trends


               F. Anceau BULL-CRG, Louvenciennes, F
               D. Borrione    IMAG/ARTEMIS, Grenoble, F
               A.J. Camilleri Hewlett Packard Labs., Bristol, UK
               P. Camurati    Politecnico di Torino, Torino, I
               H. Eveking     Institut fur Datentechnik, Darmstad, D
               P. Prinetto    Politecnico di Torino, Torino, I
	Jim Barby  (U of Waterloo VLSI Group, Waterloo Ont.)

  Duncan Elliott, Dept. EE, University of Toronto, Toronto, Canada M5S 1A5
  dunc@eecg.toronto.edu  dunc@eecg.utoronto.ca  uunet!utai!eecg!dunc
  LAT: 43 39' 35.9"N  LON: 79 23' 41.7"W ELEVATION: 349.30          VE3PKD