3rd NASA LaRC Formal Methods Workshop

H. J. E. Reid Conference Center, May 10-12, 1995

Final Agenda

Wednesday, May 10, 1995

7:45 Bus Leaves Courtyard Hotel for Reid Conference Center

8:00 - 8:45 Late Registration

Session 1: Introduction to Formal Methods, chaired by Ricky Butler

8:45 - 9:00 Welcome

Milton Holt, Chief, Information & Electromagnetic Technology Division

9:00 - 9:30 Rationale for Formal Methods

Ricky Butler, NASA Langley Research Center

9:30 - 10:30 An Informal Introduction to Formal Methods

Michael Holloway, Ricky Butler, Paul Miner, NASA Langley Research Center

10:30 - 11:00 Break

11:00 - 12:00 An Informal Introduction to Formal Methods (continued)

12:00 - 12:30 Overview of NASA Langley's Formal Methods Program

Ricky Butler, NASA Langley Research Center

12:30 - 1:30 Lunch in NASA Cafeteria

Session 2: LaRC-sponsored Industrial Applications, chaired by Ricky Butler

1:30 - 2:00 The AAMP5/AAMP-FV Project

Steve Miller, Rockwell-Collins

2:00 - 2:30 Union Switch & Signal Project

Joe Profeta, Union Switch & Signal

Doug Hoover, Odyssey Research Associates

2:30 - 3:00 Honeywell Software Development Project

Lance Sherry, Honeywell

Doug Hoover, Odyssey Research Associates

3:00 - 3:30 Break

Session 3: Industry Perspectives on Formal Methods, chaired by Michael Holloway

3:30 - 5:00 Panel Session

Scott French, Loral ATC

Steve Miller, Rockwell-Collins

Joe Profeta, Union Switch & Signal

Lance Sherry, Honeywell

5:00 - 6:00 Cash Bar Social in Reid Conference Center

6:00 Bus Leaves Reid Conference Center for Courtyard Hotel

Thursday, May 11, 1995

8:00 Bus Leaves Courtyard Hotel for Reid Conference Center

Session 4: Software Systems (1), chaired by Ricky Butler

8:30 - 9:30 Formal Verification for Fault-Tolerant Architectures/PVS Design

John Rushby, SRI International

9:30 - 10:30 Formal Methods Demonstration Project for Space Applications

Ben DiVito, VÍGYAN, Inc.

John Kelly, Jet Propulsion Laboratory

10:30 - 10:45 Break

Session 5: Software Systems (2), chaired by Michael Holloway

10:45 - 11:45 Ada 9X Language Precision Team

David Guaspari, Odyssey Research Associates

11:45 - 12:30 Introduction to Penelope and Its Applications

David Guaspari, Odyssey Research Associates

12:30 - 1:30 Lunch in NASA Cafeteria

Session 6: Hardware Systems, chaired by Paul Miner

1:30 - 2:00 The Formal Verification Technology Used on AAMP5

Mandayam Srivas, SRI International

2:00 - 2:30 Specification and Verification of VHDL Designs

Damir Jamsek, Odyssey Research Associates

2:30 - 3:15 Derivational Reasoning System

Bhaskar Bose, Derivation Systems Inc.

3:15 - 3:30 Break

Session 7: Researcher Perspectives on Formal Methods, chaired by Jim Caldwell

3:30 - 5:00 Panel Session

David Dill, Stanford University

Doug Hoover, Odyssey Research Associates

Steve Johnson, Indiana University

Natarajan Shankar, SRI International

5:00 Bus Leaves Reid Conference Center for Courtyard Hotel

6:15 Bus Leaves Courtyard Hotel for Workshop Dinner

6:30 - 8:00 Dinner at Captain George's Seafood Restaurant

8:00 Bus Leaves Captain George's for Courtyard Hotel

Friday, May 12, 1995

8:00 Bus Leaves Courtyard Hotel for Reid Conference Center

Session 8: Research Issues (1), chaired by Michael Holloway

8:30 - 9:15 Safety Analysis

John Knight, University of Virginia

9:15 - 10:00 Non-standard Analysis and Embedded Software

Richard Platek, Odyssey Research Associates

10:00 - 10:30 Break

Session 9: Research Issues (2), chaired by Victor Carreno

10:30 - 11:15 Hybrid Fault Algorithms

Pat Lincoln, SRI International

11:15 - 12:00 Model Checking

David Dill, Stanford University

12:00 - 1:30 Lunch in NASA Cafeteria

Session 10: Research Issues (3), chaired by Ricky Butler

1:30 - 2:00 The DDD Scheme Machine

Steve Johnson, Indiana University

2:00 - 2:30 Formal Development of a Clock Synchronization Circuit

Paul Miner, NASA Langley Research Center

2:30 - 2:45 Closing Remarks

Ricky Butler, NASA Langley Research Center

3:30 Bus Leaves Reid Conference Center for Courtyard Hotel

last changed: 16 May 1995 (14:26:46)