Show The Graduate Center Menu
 
 

Formal Methods

Instructor: Associate Professor Subash Shankar


Overview:

Formal methods is the formal modeling of computer systems to rigorously analyze their properties and/or prove that they work correctly. It has grown greatly from its early days in proving correctness of toy programs and is now used to verify almost all processor chips. The next goal is software and embedded systems, especially as software is increasingly used for safety critical systems.

This is a research oriented course surveying the 3 primary techniques of formal methods: model checking, theorem proving, and static analysis. The course will not make you an expert on any of these; however, you should gain enough understanding to know which tools/methodologies to use on real problems, and also be able to tackle research problems in formal methods.
 

Prerequisites:

There are no formal prerequisites. However, you should review propositional and first order logic if needed. As most tools are for Linux/Unix, you should also be comfortable as a user of these platforms.
 

Text:

A collection of papers will be posted on blackboard.
 

Requirements / Grading:

  • Reading papers before each week’s lecture and participating in discussion
  • Presenting technical papers in the latter part of the course
  • Three small projects using tools from each of the 3 primary topics of the course
  • One larger project applying tools to verify a real system, along with a small paper/proposal and presentation documenting your results and ideas you may have on what is needed to improve your results.
     

Schedule:   

(Tools: Spin, SMV, CVC, PVS and Frama-C)

Introduction to Formal Methods (1 wk)

Model Checking

  • Linear and Branching Time Temporal Logics (1 wk)
  • Model Checking: Fundamental model checking algorithm, explicit state model checkers (e.g., Spin), symbolic model checkers (e.g., SMV) (2 wks)

Theorem Proving

  • SAT and SMT solvers (e.g., CVC) (1 wk) 
  • Higher order logics, theorem provers (e.g., PVS), and their application to software verification (2 wks)

Static Analysis

  • Logics of Programs (1 wk) 
  • Program Slicing (static, dynamic, conditioned) (1 wk) 
  • Abstract Interpretation (1 wk) 
  • Tools for static analysis (e.g., Frama-C) (1 wk)

Student Presentations (3 wks)

Although I am open to other suggestions, I suspect that the majority will be more detailed presentations of topics [very briefly] alluded to during the above units. These include: 

  • Model checkers for timed systems
  • Model checkers for probabilistic systems 
  • Theorem provers based on other logics , and how the logic affects their use in formal methods. 
  • Other program logics (including game logics)
  • Verification methodologies integrating 2 (or all 3) of the pri- mary areas 
  • Formal Methodologies (e.g., the B-method) 
  • SAT/SMT-based synthesis and/or refinement 
  • Static analysis tools aimed at particular problems

If you are potentially interested in one of the topics, please contact me quickly and I can point you to more papers so that you can finalize your choice.
 

Final Exam (1 wk)

There will be a final exam, with part or all of it being the large project paper/presentation.