======Software Specification and Verification, Fall 2009======
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.

===== Announcements =====
  * Jan. 15: slides for Compositional Reasoning available.
  * Dec. 23: solutions to {{courses:ssv2009:hw1s.pdf|HW#1}}, {{courses:ssv2009:hw2s.pdf|HW#2}}, and  {{courses:ssv2009:hw3s.pdf|HW#3}} available.
  * Dec. 16: slides for Temporal Verification available.
  * Dec. 14: slides for the Owicki-Gries Method and UNITY available.
  * Dec. 14: slides for Z, B, and Alloy available.
  * Dec. 03: slides for the Why tool available.
  * Oct. 28: slides for Hoare Logic (II): Procedures available.
  * Oct. 21: {{courses:ssv2009:hw4.pdf|HW#4}} due on Oct. 28.
  * Oct. 21: slides for Predicate Transformers available.
  * Oct. 19: slides for Soundness and Completeness of Hoare Logic available.
  * Oct. 14: {{courses:ssv2009:hw3.pdf|HW#3}} due on Oct. 21.
  * Oct. 07: {{courses:ssv2009:hw2.pdf|HW#2}} due on Oct. 14.
  * Oct. 07: slides for Hoare Logic available.
  * Sep. 30: {{courses:ssv2009:hw1.pdf|HW#1}} due on Oct. 7.
  * Sep. 30: slides for Logical Proofs in Coq available.
  * Sep. 23: slides for First-Order Logic available for download.
  * Sep. 16: {{courses:ssv2009:hw0.pdf|HW#0}} due on Sep. 23.
  * Sep. 16: {{courses:ssv2009:ssv2009info.pdf|PDF version}} of this page (as of today, without subsequent updates); slides for Introduction and Propositional Logic and notes on System LK, Example Proofs, and Natural Deduction available for download.


===== Instructor =====

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

===== Lectures =====

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.

===== Office Hours =====

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

===== TA =====

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

===== Prerequisites =====

Computer Programming and Discrete Mathematics

===== Textbook =====

//Class Notes// and //Selected Readings//

===== Syllabus/Schedule (with links to slides/notes) =====

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) \\ [{{courses:ssv2009:introduction.pdf|slides}}]
  * Propositional and First-Order Logics (1.5 weeks: 09/16b, 09/23) \\ [slides:{{courses:ssv2009:logic_propositional.pdf|Propositional Logic}}, {{courses:ssv2009:logic_first_order.pdf|First-Order Logic}}; notes: {{courses:ssv2009:sequent_LK.pdf|System LK}}, {{courses:ssv2009:sequent_proofs.pdf|Example Proofs}}, {{courses:ssv2009:natural_deduction.pdf|Natural Deduction}}]
  * Logical Proofs in the Coq Proof Assistant (1 week: 9/30) \\ [{{courses:ssv2009:natural_deduction_in_Coq.pdf|slides}}]
  * Verification of Sequential Programs: Hoare Logic (2 weeks: 10/07, 10/14) \\ [slides:{{courses:ssv2009:hoare_logic.pdf|Hoare Logic}}, {{courses:ssv2009:hoare_logic_soundness_completeness.pdf|Soundess and Completeness}}; notes: {{courses:ssv2009:hoare_logic_rules.pdf|Rules of Hoare Logic}}, {{courses:ssv2009:hoare_logic_proofs.pdf|Proofs with Hoare Logic}}]
  * Predicate Transformers and Program Derivation (1 week: 10/21) \\ [{{courses:ssv2009:predicate_transformers.pdf|slides}}]
  * Procedures (+ Object Orientation) (1 week: 10/28) \\ [{{courses:ssv2009:procedures.pdf|slides}}]
  * Logical Proofs in Coq (continued) (1 week: 11/04)
  * Program Verification Tools: Why and Frama-C (1 week: 11/25) \\ [{{courses:ssv2009:why.pdf|slides}}]
  * Data Refinement + Formal Methods: Z, B, and Alloy (3 weeks: 11/11, 11/18, 12/02) \\ [slides:{{courses:ssv2009:Z.pdf|Z}}, {{courses:ssv2009:B.pdf|B}}, {{courses:ssv2009:Alloy.pdf|Alloy}}]
  * Concurrent, Reactive Systems: Owicki-Gries Method, UNITY, Linear Temporal Logic (2 weeks: 12/09, 12/16) \\ [slides:{{courses:ssv2009:concurrency.pdf|Owicki-Gries}}, {{courses:ssv2009:UNITY.pdf|UNITY}}, {{courses:ssv2009:temporal_verification.pdf|Temporal Verification}}]
  * Selected Topics: Modular/Compositional Reasoning (1 week: 12/23) \\ [{{courses:ssv2009:compositional_reasoning.pdf|slides}}]
  * **Final** (**2009/12/30**)
  * Selected Topics: Separation Logic (1 week: 2010/01/07)
  * Data Refinement + Formal Methods (continued): VDM (1 week: 2010/01/14)

===== Grading =====

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

===== References =====
  - //Logic for Computer Science: Foundations of Automatic Theorem Proving//, J.H. Gallier, Harper & Row Publishers, 1985. (free!)
  - //Proof Theory and Automated Deduction//, J. Goubault-Larrecq and I. Mackie, Kluwer Academic Publishers, 1997.
  - //Logic in Computer Science: Modelling and Reasoning about Systems//, M. Huth and M. Ryan, Cambridge University Press, 2004.
  - //Foundations for Programming Languages//, J.C. Mitchell, The MIT Press, 1996.
  - //Formal Syntax and Semantics of Programming Languages//, K. Slonneger and B.L. Kurtz, Addison-Wesley, 1995.
  - //Verification of Sequential and Concurrent Programs, 2nd Edition//, K.R. Apt and E.-R. Olderog, Springer-Verlag, 1997.
  - //The Science of Programming//, D. Gries, Springer-Verlag, 1981.
  - //Predicate Calculus and Program Semantics//, E.W. Dijkstra and C.S. Scholten, Springer-Verlag, 1990.
  - //Programming from Specifications, 2nd Edition//, C. Morgan, 1994.
  - //The Z Notation: A Reference Manual, 2nd Edition//, J.M. Spivey, 1992. (free!)
  - //Software Engineering with B//, J.B. Wordsworth, Addison-Wesley, 1996.
  - //Software Abstractions: Logic, Language, and Analysis//, D. Jackson, MIT Press, 2006.
  - //The Temporal Logic of Reactive and Concurrent Systems: Specification//, Z. Manna and A. Pnueli, Springer-Verlag, 1992.
  - //Temporal Verification of Reactive Systems: Safety//, Z. Manna and A. Pnueli, Springer, 1995.
  - //Temporal Verification of Reactive Systems: Progress//, Z. Manna and A. Pnueli, Book Draft, 1996. (free!)
  - //Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers//, L. Lamport, Addison-Wesley, 2003.
  - //Parallel Program Design: A Foundation//, K.M. Chandy and J. Misra, Addison-Wesley, 1988.
  - //A Discipline of Multiprogramming: Programming Theory for Distributed Applications//, J. Misra, Springer, 2001
  - //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
  - //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.)