Formal Methods: Past, Present, and Future

• Formal Methods: Past, Present, and Future.
• Outline.
• What are Formal Methods?.
• The Enterprise of Formal Methods.
• Power of Formal Methods.
• Why Formal Methods?.
• Two Decades of Progress.
• ----.
• ----.
• Algebraic Specification of Stacks.
• Two Process Mutual Exclusion.
• Symbol Table in Z.
• Seitz's FIFO Queue Element.
• Active Building Controller.
• SRT Division Algorithm (Pentium).
• A Historical Perspective: 80's.
• ----.
• ----.
• ----.
• A Historical Perspective: 80's.
• Roots of Formal Methods.
• A Historical Perspective: 80's.
• The CLInc "Stack".
• MicroGypsy Example.
• Part of the FM8502 Core Image.
• CICS Results.
• A Sense of Urgency.
• More History.
• State of the Art.
• State of the Art.
• Formal Methods: Do They Scale?.
• Case Studies: Software Specification.
• TCAS-II Internal Model of Other Aircraft.
• Case Studies: Hardware Verification.
• Encore Gigamax Cache Coherence Protocol.
• Case Studies: Software Verification.
• Paris Metro.
• Explosion Test Environment Controller.
• Formal Methods: Do They Scale?.
• Challenges for the Future.
• A Lightweight Approach.
• Promising Directions for the Near Future.
• For More Information.
• My Grand Vision.