1994 Research Review

NOTE: These slides were presented to sponsors and peers at a 1994 Computational Logic Research review and are provided as a historical snapshot of that research program. For a brief descriptive summary, see 1994 Research Review Summary.

Agenda

WEDNESDAY, APRIL 20

8:00 AM REGISTRATION
Continental Breakfast

INTRODUCTION

8:30 AM : Good - Mathematical Modeling of Digital Systems [slides]

FOUNDATIONS

9:00 AM : Moore - A Computational Logic for an Applicative Core Language (Acl2) [slides]

10:00 AM Break

10:30 AM : Kaufmann - Acl2 ... Continued [slides]
11:30 AM : Cowles (UWyoming) - Reusable Libraries for Acl2 [slides]
12:00 PM : Akers - Static Type Checking for the Acl2 Logic [slides]

12:30 PM : Lunch
1:30 PM : Huet (INRIA) - An Overview of the Coq Proof Assistant and its
Application to Program Validation and Protocol Verification [slides]
2:00 PM : Boyer - QED: Towards a Mechanically Proof-Checked Encyclopedia of Mathematics [slides]

LANGUAGES

2:15 PM : Flatau - A Verified Implementation of an Applicative
Language with Dynamic Storage Allocation [slides]
2:45 PM : Smith,M - Modeling Ada [slides]

3:30 PM : Break

4:00 PM : Kaufmann - A Substitute for VCGs in Proving Properties of Programs [slides]
4:45 PM : Akers - Toward a Mathematical Semantics for C [slides]
5:00 PM : Yu (DEC) - Reusability of an MC68020 Model in Modeling the DEC Alpha [slides]

5:30 PM : Adjourn

THURSDAY, APRIL 21

8:00 AM : REGISTRATION
Continental Breakfast

HARDWARE

8:30 AM : Hunt - Identifying Approaches to the Formalization of DSPs [slides]
9:00 AM : Albin - 68020 Model Validation [slides]
9:15 AM : Smith,L - FM9001 Model Validation [slides]
9:30 AM : Hunt - Designing a VHDL Simulator in Acl2 [slides]

10:15 AM : Break

10:45 AM : Russinoff - Modeling Synchronous and Asynchronous Behavior in VHDL [slides]
11:45 AM : Hunt & Greenwood (Motorola) - Modeling a Motorola DSP Design [slides] , [slides]

12:15 PM : Lunch

CONTROLLERS

1:15 PM : Wilding - A Verified Scheduling Theorem [slides]
1:30 PM : Wilding - Toward Verified Real-Time Applications [slides]
2:00 PM : Carranza - Verifying the Behavior of a Fuzzy Logic Controller [slides]
2:30 PM : Young - Modeling a Real-Time Railroad Gate Controller [slides]

3:00 PM : Break

SYSTEMS SOFTWARE

3:30 PM : Cohen - Proving a Separation Kernel [slides]
4:00 PM : Bevier - A Mathematical Specification for the Mach Kernel [slides]
4:45 PM : Smith,L - Testing the Mach Kernel for Specification Compliance [slides]
5:00 PM : Bevier - Security Analysis of Kernel Models [slides]

5:30 PM : Adjourn

FRIDAY, APRIL 22

MODELING A MOTOROLA DSP DESIGN

** PROPRIETARY SESSION **

12:15 PM : Adjourn

This page is URL http://www.computationallogic.com/reviews/94/index.html