8:30 – 9:00 (optional) A Quick Tutorial on Formal Methods (FM) [Rick Butler] (PowerPoint)

9:00 – 9:15 Why SPIDER Design Assurance is based on FM [Paul Miner] (PowerPoint)

9:15 – 9:30 Why SATS needs Formal Methods [Victor Carreno] (pdf)

9:30 – 9:45 Why Fundamental Algorithms Should Be Formally Verified [Cesar Munoz] (pdf)

9:45 – 10:00 BREAK

10:00 – 10:15 FM & Accident Analysis: What's the Connection? [Michael Holloway] (pdf)

10:15 – 10:30 Is Software Still a Problem?[ Kelly Hayhurst] (Powerpoint)

10:30 – 11:15 Formal Analysis of a Preliminary SATS concept [Carreno/Gottliebsen] (part1 ps) (part2 ps)

11:15 - 1:00 LUNCH

1:00 – 1:30 SPIDER -- Where Are We Now? [Paul Miner/ Geser] (Powerpoint)

1:30 – 2:00 Using SPIDER for Intrusion Tolerance [Jeff Maddalon] (Powerpoint)

9:00 - 9:30 Object Oriented Technology for Commercial Aviation [Kelly Hayhurst] (Powerpoint)

9:30 – 10:00 The Columbia Accident Investigation Board Report [Michael Holloway] (pdf)

10:00 – 11:30 Columbia Accident Colloqium (at H.J.E REID CENTER)

11:30 - 12:30 Lunch

12:30 – 1:00 Formal Methods Contribution to the SATS Concept [Munoz/Carreno] (pdf)

1:00 – 1:30 Formal Verification of a Terminal Area Scheduler [Alfons Geser] (ps)

1:30 – 1:45 BREAK

1:45 – 2:15 Support Tools for the PVS Theorem Prover [Ben Di Vito] (pdf)

2:15 – 2:45 PVS Vector Library [Rick Butler] (pdf)

2:45 – 3:05 NASA Library [Rick Butler] (ps)

Curator and Responsible NASA Official: C. Michael Holloway
larc privacy statement
last modified: 15 October 2003 (08:13:48)
Note: The tag identifies links that are outside of the NASA domain.