From Miriam Leeser 4 Apr 89
Date: Tue, 4 Apr 89 16:56:44 EDT
From: mel%hyperion.EE.cornell.edu@munnari.oz (Miriam Leeser)
To: info-hol@clover.ucdavis.edu
Subject: Hardware Workshop to be held at Cornell July 5-7
Status: RO

I am  sending more information about the workshop -
        Hardware Specification, Verification and Synthesis:
                Mathematical Aspects

To be held at Cornell University July 5-7, 1989.  A few weeks ago I
sent this news group a short description of this workshop.  Below is a
registration form and a latex version of the preliminary program.  The
registration fee includes the cost of lunches, coffee breaks, and the
banquet.

Miriam Leeser   mel@tesla.ee.cornell.edu
Geoffrey Brown  gbrown@tesla.ee.cornell.edu

***********************************************************************

{\large\bf Mathematical Sciences Institute Workshop on} \\*[0.10in]
{\Large\bf Hardware Specification, Verification and Synthesis:} \\*[0.10in]
{\Large\bf Mathematical Aspects} \\*[0.20in]
{\large\bf Preliminary Program}

\underline{Wednesday, July 5}
\item [8:45 - 9:00] Welcome -- Robert Constable, Cornell University
\item [9:00 - 9:50] {\it Design for Verifiability: Formal Verification
within the VLSI Design Process}  George J. Milne, University of Strathclyde
\item [9:50 - 10:40] {\it Verification of Digital Circuits by Symbolic
Logic Simulation}  Randal E. Bryant, Carnegie Mellon University
\item [11:00 - 11:50] {\it Constraints and Multilevel Hierarchical
Verification} \\ Daniel Weise, Stanford University
\item [1:00 - 1:50] {\it The Design Verification of a Working SECD
Chip} \\ Graham Birtwistle and Brian Graham, University of Calgary
\item [1:50 - 2:40] {\it Formal Verification of State-Machines in
Higher Order Logic} Paul N. Lowenstein, National Semiconductor Corp.
\item [3:00 - 3:50] {\it A Mechanically Derived Systolic
Implementation of Pyramidal Algorithms}
Farshid Arman, Bikash Sabata and Christian Lengauer, The
University of Texas at Austin

\underline{Thursday, July 6}
\item [9:00 - 9:50] {\it Behavior Preserving Transformations for
High-Level Synthesis} Raul Camposano, IBM Thomas J. Watson Research Center
\item [9:50 - 10:40] {\it From Programs to Transistors: Verifying
Hardware Synthesis Tools} Miriam E. Leeser and Geoffrey M. Brown,
Cornell University
\item [11:00 - 11:50] {\it Combining Engineering Vigor with
Mathematical Rigor} \\ Shiu-Kai Chin, Syracuse University
\item [1:00 - 1:50] {\it Using Higher-Order Logic to Reason about
Asynchronous Behavior} Jeffrey J. Joyce, Cambridge University
\item [1:50 - 2:40] {\it On the Specification and Synthesis of
Mixed-Mode (Synchronous + Asynchronous) Systems} P. A. Subramanyam, \\
AT\&T Bell Laboratories
\item [3:00 - 3:50] {\it Compositional Model Checking} \\ Edmund M.
Clarke, Jr.  Carnegie Mellon University
\item [3:50 - 4:40] {\it to be announced} Alain Martin, California
Institute of Technology


\underline{Friday, July 7}
\item [9:00 - 9:50] {\it Manipulating Logical Organization with System
Factorizations} Steve Johnson, Indiana University
\item [9:50 - 10:40] {\it The Verification of Circuit Generation
Functions} \\ Warren Hunt, Computational Logic, Inc.
\item [11:00 - 11:50] {\it Hardware Verification Using Clio} Mandayam
Srivas and Mark Bickford, Odyssey Research Associates, Inc.
\item [1:00 - 1:50] {\it Verification Of Combinational Logic in Nuprl}
\\ David Basin and Peter DelVecchio, Cornell University
\item [1:50 - 2:40] {\it Using Type Theory for Reasoning About Digital
Systems} \\ Keith Hanna, University of Kent
\item [3:00 - 3:50] {\it Categories for the Working Hardware Designer}
\\ Mary Sheeran and Phillip L. Wadler, Glasgow University