| |
|
|
|
Tuesday, 9 September 1997 |
| 16:00 |
- |
20:00 |
|
Registration and Check-In |
| |
|
|
|
|
| |
|
|
|
Wednesday, 10 September
1997 |
| 7:30 |
- |
15:00 |
|
Registration and Check-In |
| 8:00 |
- |
8:30 |
|
Deluxe Continental Breakfast |
| |
|
|
|
|
| |
|
|
|
Session 1: Introduction and Motivation,
chaired by Ricky Butler |
| 8:30 |
- |
9:00 |
|
Welcome and Introduction to Lfm97 |
| |
|
|
|
Ricky Butler, Michael
Holloway |
| 9:00 |
- |
9:30 |
|
Harm Reduction Technology |
| |
|
|
|
Richard Platek |
| 9:30 |
- |
10:00 |
|
Are Formal Methods Best Used for Refutation
or for Verification? |
| |
|
|
|
John Rushby |
| 10:00 |
- |
10:20 |
|
break |
| |
|
|
|
|
| |
|
|
|
Session 2: Requirements (1), chaired
by Michael Holloway |
| 10:20 |
- |
10:50 |
|
Requirements Analysis of Real-Time Control
Systems Using PVS |
| |
|
|
|
Bruno Dutertre and Victoria
Stavridou |
| 10:50 |
- |
11:20 |
|
Reuse of a Formal Model for Requirements
Validation |
| |
|
|
|
Robyn Lutz |
| 11:20 |
- |
11:50 |
|
Applying the SCR Requirements Method
to a Simple Autopilot |
| |
|
|
|
Ramesh Bharadwaj and
Constance Heitmeyer |
| 11:50 |
- |
13:10 |
|
lunch |
| |
|
|
|
|
| |
|
|
|
Session 3: Requirements (2), chaired
by Victor Carreno |
| 13:10 |
- |
13:40 |
|
A Tabular Language for System Design |
| |
|
|
|
Steven Johnson |
| 13:40 |
- |
14:10 |
|
Verifying Communication Related Safety
Constraints in RSML Specifications |
| |
|
|
|
Mats P.E. Heimdahl |
| 14:10 |
- |
14:40 |
|
Avionics Research at ORA |
| |
|
|
|
David Guaspari |
| 14:40 |
- |
15:00 |
|
break |
| |
|
|
|
|
| |
|
|
|
Session 4: Research Topics, chaired
by Paul Miner |
| 15:00 |
- |
15:30 |
|
Towards High-Assurance High-Performance
Program Synthesis |
| |
|
|
|
Michael Lowry, Steven
Roach, and Jeffrey Van Baalen |
| 15:30 |
- |
16:00 |
|
On the Automatic Discovery of Loop Invariants |
| |
|
|
|
Andrew Ireland and Jamie
Stark |
| 16:00 |
- |
16:30 |
|
PV: A Model-Checker for Verifying LTL-X
Properties |
| |
|
|
|
Ratan Nalumasu and Ganesh
Gopalakrishnan |
| 16:30 |
- |
17:00 |
|
Automated Deductive Verification of Parallel
Systems |
| |
|
|
|
Hassen Saïdi |
| |
|
|
|
|
| |
|
|
|
Thursday,
11 September 1997 |
| 7:30 |
- |
15:00 |
|
Registration and Check-In |
| 8:00 |
- |
8:30 |
|
Southern Continental
Breakfast |
| |
|
|
|
|
| |
|
|
|
Session 5: Applications (1), chaired
by Kelly Hayhurst |
| 8:30 |
- |
9:00 |
|
Plotting The Escape from The Tower: A
Formalist's Practicality Primer |
| |
|
|
|
James Sutton |
| 9:00 |
- |
9:30 |
|
Formal Verification of the AAMP5 and
AAMP-FV Microcode |
| |
|
|
|
Steve Miller |
| 9:30 |
- |
10:00 |
|
Formal Verification of Fault-Tolerant
Algorithms |
| |
|
|
|
Patrick Lincoln |
| 10:00 |
- |
10:20 |
|
break |
| |
|
|
|
|
| |
|
|
|
Session 6: Theorem Proving Issues,
chaired by Victor Carreno |
| 10:20 |
- |
10:50 |
|
Domain Checking Z Specifications |
| |
|
|
|
Mark Saaltink |
| 10:50 |
- |
11:20 |
|
Issues in the Formal Verification of State
of the Art Processor Architectures |
|
|
|
|
Mandayam Srivas |
| 11:20 |
- |
11:50 |
|
Robust Computer System Proofs in PVS |
|
|
|
|
Matthew Wilding |
| 11:50 |
- |
13:10 |
|
lunch |
|
|
|
|
|
|
|
|
|
Session 7: Hardware and Operating Systems,
chaired by Paul Miner |
| 13:10 |
- |
13:40 |
|
Formalizing Partitioning in Integrated
Modular Avionics |
|
|
|
|
Ben DiVito |
| 13:40 |
- |
14:10 |
|
Hardware Verification at ORA |
|
|
|
|
Mark Bickford |
| 14:10 |
- |
14:40 |
|
Derivation of the PCI Bus Protocol |
|
|
|
|
Bhaskar Bose |
|
|
|
|
|
|
|
|
|
Session 8: Applications (2), chaired
by Kelly Hayhurst |
| 15:00 |
- |
15:30 |
|
Formally-based CAD Environments |
|
|
|
|
Damir Jamsek |
| 15:30 |
- |
16:00 |
|
A Provably Correct Embedded Verifier for
the Certification of Safety Critical Software |
|
|
|
|
A. Cimatti, F. Giunchiglia,
P. Pecchiari, B. Pietra, J. Profeta, D. Romano, P. Traverso, B. Yu |
| 16:00 |
- |
16:30 |
|
Formalization and Analysis of the Separation
Minima for Aircraft in the North Atlantic Region |
|
|
|
|
Nancy Day, Jeffrey Joyce,
and Gerry Pelletier |
| 16:30 |
- |
17:00 |
|
Proving Properties of Accidents |
|
|
|
|
C. W. Johnson |
|
|
|
|
|
|
|
|
|
Friday, 12 September 1997 |
|
|
|
|
Session 9: Technology Transfer,
chaired by Michael Holloway |
| 8:30 |
- |
9:00 |
|
Why Are Formal Methods Not Used More Widely? |
|
|
|
|
John Knight, Colleen
DeJong, Matthew Gibble, and Luís Nakano |
| 9:00 |
- |
9:45 |
|
The New NASA Formal Methods Guidebook |
|
|
|
|
John Kelly, Ben DiVito,
Judith Crow, and John Rushby |
| 9:45 |
- |
10:45 |
|
Modeling and Validating SAFER in VDM-SL |
|
|
|
|
Sten Agerholm and Peter
Gorm Larsen |
|
|
|
|
|
|
|
|
|
Session 10: Hardware Design, chaired
by Ricky Butler |
| 10:45 |
- |
11:15 |
|
Fundamental Hardware Design in PVS |
|
|
|
|
James Leathrum |
| 11:15 |
- |
11:45 |
|
Coinductive Verification of Hardware Optimizations |
|
|
|
|
Paul Miner |
| 11:45 |
- |
12:00 |
|
Closing Remarks |
|
|
|
|
Michael Holloway |
