The Third Annual Internal Formal Methods Workshop

October 22-23, 2003

B1220, Rm 110

Wednesday, Oct 22

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)

Thursday, Oct 23

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 link to external site tag identifies links that are outside of the NASA domain.
>