Quick Index

• Weaving Formal Methods into the Undergraduate Computer Science Curriculum
• Main Idea
• Broad View of Formal Methods
• Underlying Mathematics
• Why Did We "Fail" in the Past?
• Why Can We Succeed Now?
• How to Succeed in the Future
• Common Elements (I)
• Common Elements (II)
• Common Elements (III)
• Tools
• Model Checkers
• Hardware Example
• State Machine for CPU
• Homework Questions
• Specification / Program Checkers
• Extended Static Checking
• Multiset Example
• ESC/Java Code
• ESC/Java Code
• Design Checkers
• Storage Allocation Example
• Nitpick Specification
• Claim Violated
• Writing Specs: MSE Homework Exercises
• TLA Example
• Looking at a Typical CS Curriculum
• Obvious
• Not So Obvious
• Pros and Cons to Weaving
• Approach
• Recap