This is an introductory course on formal software specification and verification, covering various formalisms, methods, and tools for specifying the properties of a software program and for verifying that the program meets its specification. We will focus on deductive (theorem proving) methods. A separate, complementary course entitled “Automatic Verification” covers algorithmic (model checking) methods.

• Dec. 29: slides for Z, B, and Alloy available.
• Dec. 14: slides for Owicki-Gries Method and UNITY Logic available.
• Dec. 14: slides for Why available.
• Nov. 01: HW#4 due on Nov. 11.
• Nov. 01: slides for Soundness and Completeness of Hoare Logic, Predicate Transformers, and Hoare Logic of Procedures available.
• Nov. 01: HW#3.
• Oct. 07: slides for Logical Proofs in Coq and Hoare Logic and notes on Hoare Logic available.
• Oct. 07: HW#2 due on Oct. 14.
• Sep. 23: slides for First-Order Logic available.
• Sep. 23: HW#1 due on Sep. 30.
• Sep. 20: slides for Propositional Logic revised and a note on Natural Deduction available.
• Sep. 16: slides for Introduction and Propositional Logic available.
• Sep. 10: class meetings moved to Thursday 2:20-5:20PM.
• Sep. 09: this website is the sole source of all up to date course information and syllabus; there will be no separate PDF version (unlike in previous years).

Yih-Kuen Tsay (蔡益坤), Room 1108, Management II, 3366-1189, Xtsay@im.ntu.edu.twX (between the enclosing pair of X's)

Wednesday 9:10AM-12:10PM, Room 302, College of Management, Building II
Note: when the class is small enough, we will meet in the seminar room on the 11th floor of that building.

Wednesday 1:30-2:30PM (Room 1108, Management II) or by appointment

Ming-Hsien Tsai (蔡明憲), 3366-1205, Xmhtsai208@gmail.comX (between the enclosing pair of X's).

Computer Programming and Discrete Mathematics

Class Notes and Selected Readings

The goal of this course is to acquaint the students with fundamentals of formal software verification and to prepare them for conducting research in the area. We shall seek to strike a balance between depth and breadth, covering both the foundations and some of the more successful formalisms, techniques, and tools. Below is a tentative list of topics and their schedule:

• Introduction (.5 week: 09/16a)
  [slides]
• Propositional and First-Order Logics (1.5 weeks: 09/16b, 09/23)
  [slides:Propositional Logic, First-Order Logic; notes: Natural Deduction]
• Logical Proofs in the Coq Proof Assistant (1 week: 09/30)
  [slides]
• Verification of Sequential Programs: Hoare Logic (2 weeks: 10/07, 10/14)
  [slides:Hoare Logic, Soundess and Completeness; notes: Rules of Hoare Logic, Proofs with Hoare Logic]
• Predicate Transformers and Program Derivation (1 week: 10/21)
  [slides]
• Procedures (+ Object Orientation) (1 week: 10/28)
  [slides]
• Program Verification Tools: Coq, Why, and Frama-C (3 weeks: 11/04, 11/11, 11/18)
  [slides: Why, Frama-C]
• Data Refinement + Formal Methods: Z, B, and Alloy (3 weeks: 11/25, 12/02, 12/09)
  [slides:Z, B, Alloy]
• Concurrent, Reactive Systems: Owicki-Gries Method, UNITY, Linear Temporal Logic (2 weeks: 12/16, 12/23)
  [slides:Owicki-Gries, UNITY, Temporal Verification]
• Final (2010/12/30)
• Selected Topic: Modular/Compositional Reasoning (1 week: 2011/01/06)
  [slides]
• Selected Topic: Separation Logic (1 week: 2011/01/13)

Homework Assignments 20%, Final 40%, Term Paper/Report 40%

1. Logic for Computer Science: Foundations of Automatic Theorem Proving, J.H. Gallier, Harper & Row Publishers, 1985. (free!)
2. Proof Theory and Automated Deduction, J. Goubault-Larrecq and I. Mackie, Kluwer Academic Publishers, 1997.
3. Logic in Computer Science: Modelling and Reasoning about Systems, M. Huth and M. Ryan, Cambridge University Press, 2004.
4. Foundations for Programming Languages, J.C. Mitchell, The MIT Press, 1996.
5. Formal Syntax and Semantics of Programming Languages, K. Slonneger and B.L. Kurtz, Addison-Wesley, 1995.
6. Verification of Sequential and Concurrent Programs, 2nd Edition, K.R. Apt and E.-R. Olderog, Springer-Verlag, 1997.
7. The Science of Programming, D. Gries, Springer-Verlag, 1981.
8. Predicate Calculus and Program Semantics, E.W. Dijkstra and C.S. Scholten, Springer-Verlag, 1990.
9. Programming from Specifications, 2nd Edition, C. Morgan, 1994.
10. The Z Notation: A Reference Manual, 2nd Edition, J.M. Spivey, 1992. (free!)
11. Software Engineering with B, J.B. Wordsworth, Addison-Wesley, 1996.
12. Modeling in Event-B: System and Software Engineering, J.-R. Abrial, Cambridge University Press, 2010.
13. The Temporal Logic of Reactive and Concurrent Systems: Specification, Z. Manna and A. Pnueli, Springer-Verlag, 1992.
14. Temporal Verification of Reactive Systems: Safety, Z. Manna and A. Pnueli, Springer, 1995.
15. Temporal Verification of Reactive Systems: Progress, Z. Manna and A. Pnueli, Book Draft, 1996. (free!)
16. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, L. Lamport, Addison-Wesley, 2003.
17. Parallel Program Design: A Foundation, K.M. Chandy and J. Misra, Addison-Wesley, 1988.
18. A Discipline of Multiprogramming: Programming Theory for Distributed Applications, J. Misra, Springer, 2001
19. Beauty Is Our Business: A Birthday Salute to Edsger W. Dijkstra, Edited by W.H.J. Feijen, A.J.M. van Gasteren, D. Gries, and J. Misra, Springer-Verlag, 1990
20. The Formal Methods Page http://formalmethods.wikia.com/wiki/Formal_methods, J. Bowen. (Note: this Web portal provides links to numerous formal methods and tools.)