Yih-Kuen Tsay's Wiki @ IM.NTU

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
======Software Specification and Verification, Fall 2024======
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. Its goal is to acquaint the students with fundamentals of formal software verification and to prepare them for conducting research in the area. We will focus on deductive (theorem proving) methods. A separate, complementary course entitled "Automatic Verification" covers algorithmic (model checking) methods.

===== Announcements =====
  * 12/18: papers/files for the {{courses:ssv2024:ssv2024final.pdf|final}} are due 5:30PM.
  * 12/11: {{courses:ssv:old_exams.zip|old exams}}.
  * 12/11: {{courses:ssv2024:hw7.pdf|HW#7}} for exercise (not counted toward grade).
  * 12/11: slides for Compositional Reasoning available.
  * 12/03: solutions to homework assignments: {{courses:ssv2024:hw4_s.pdf|HW#4}} (revised 12/04), {{courses:ssv2024:hw5_s.pdf|HW#5}}.
  * 12/03: {{courses:ssv2024:hw6.pdf|HW#6}} due on 12/11.
  * 11/27: slides for UNITY and Temporal Verification available.
  * 11/27: slides for the Owicki-Gries Method available.
  * 11/20: {{courses:ssv2024:termproject.pdf|Term Project}}: proposals due 12/13 and final results due 12/27.
  * 11/20: slides and an example for Using Frama-C available.
  * 11/13: slides for Frama-C and ACSL available (revised 11/20).
  * 11/06: {{courses:ssv2024:hw5.pdf|HW#5}} due on 11/20.
  * 11/06: slides for Hoare Logic (II): Procedures available.
  * 11/06: solutions to homework assignments: {{courses:ssv2024:hw3_s.zip|HW#3}}.
  * 10/29: slides for Predicate Transformers available (revised 10/30).
  * 10/16: {{courses:ssv2024:hw4.pdf|HW#4}} (revised 10/23) due on 10/30.
  * 10/14: slides for Soundness and Completeness of Hoare Logic available (revised 10/23).
  * 10/14: slides for Hoare Logic (I) and two notes available (revised 10/18).
  * 10/09: the class will meet in Room 403 of Management College Building 1, starting from this day till the original room (Room 203) becomes ready again.
  * 10/02: {{courses:ssv2024:hw3.pdf|HW#3}} (revised 10/09) due on 10/16.
  * 09/25: solutions to homework assignments: {{courses:ssv2024:hw1_s.pdf|HW#1}}, {{courses:ssv2024:hw2_s.pdf|HW#2}} (revised 10/02).
  * 09/24: slides and a note for Coq available (revised 09/26).
  * 09/18: {{courses:ssv2024:hw2.pdf|HW#2}} due on 09/25.
  * 09/11: {{courses:ssv2024:hw1.pdf|HW#1}} due on 09/18.
  * 09/02: {{courses:ssv2024:hw0.pdf|HW#0}} due on 09/11.
  * 09/02: slides for Course Introduction, Propositional Logic, and First-Order Logic and a note on Natural Deduction available.
  * 08/26: this wiki site created to complement the NTU COOL site for this course
===== Instructor =====
[[http://im.ntu.edu.tw/~tsay/|Yih-Kuen Tsay (蔡益坤)]], NTU IM Dept., 3366-1189, Xtsay@ntu.edu.twX (between the enclosing pair of X's) 

===== Lectures =====
Wednesday 2:20-5:20PM, Room 203, Management Building 1

===== Office Hours =====
Tuesday 1:30~2:00PM, Wednesday 1:30~2:00PM, or by appointment, Room 1108,
Management Building 2.

=====TAs=====
There is no TA for this course.

===== Prerequisites =====
Computer Programming and Discrete Mathematics

===== Textbook =====
//Class Notes// and //Selected Readings//

===== Syllabus/Schedule (with links to slides/notes) =====
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: Reasoning about Programs (.5 week: 09/04a) [{{courses:ssv2024:introduction.pdf|slides}}]
  * Fundamentals: Propositional and First-Order Logics (2.5 weeks: 09/04b, 09/11, 09/18) [slides:{{courses:ssv2024:logic_propositional.pdf|Propositional Logic}}, {{courses:ssv2024:logic_first_order.pdf|First-Order Logic}}; notes: {{courses:ssv2024:natural_deduction.pdf|Natural Deduction}}]
  * Verification Tools: Coq (2 weeks: 09/25, 10/02 canceled, 10/09) [{{courses:ssv2024:natural_deduction_in_Coq.pdf|slides}}; notes:{{courses:ssv2024:natural_deduction_tactics.pdf|Tactics for Natural Deduction in Coq}}]
  * Sequential Programs: Hoare Logic (I) (2 weeks: 10/16, 10/23) [slides:{{courses:ssv2024:hoare_logic.pdf|Hoare Logic}}, {{courses:ssv2024:hoare_logic_soundness_completeness.pdf|Soundess and Completeness}}; notes: {{courses:ssv2024:hoare_logic_rules.pdf|Rules of Hoare Logic}}, {{courses:ssv2024:hoare_logic_proofs.pdf|Proofs with Hoare Logic}}]
  * Predicate Transformers (1 week: 10/30) [{{courses:ssv2024:predicate_transformers.pdf|slides}}]
  * Procedures: Hoare Logic (II) (1 week: 11/6) [{{courses:ssv2024:procedures.pdf|slides}}]
  * Verification Tools: Frama-C + Plugins (2 weeks: 11/13, 11/20) [slides: {{courses:ssv2024:frama-c_acsl.pdf|Frama-C and ACSL}}, {{courses:ssv2024:Using-Frama-C.pdf|Using Frama-C}}; examples:{{courses:ssv2024:frama-c-simple-examples.zip|Simple Examples}}, {{courses:ssv2024:frama-c-example.zip|Frama-C Example}}]
  * Concurrent, Reactive Systems: Owicki-Gries Method (1 week: 11/27) [{{courses:ssv2024:concurrency.pdf|slides}}]
  * Concurrent, Reactive Systems: UNITY and Linear Temporal Logic (1 week: 12/04) [slides: {{courses:ssv2024:UNITY.pdf|UNITY}},{{courses:ssv2024:temporal_verification.pdf|Temporal Verification}}]
  * Selected Topics: Modular/Compositional Reasoning (1 week: 12/11) [{{courses:ssv2024:compositional_reasoning.pdf|slides}}]
  * **Final Exam** (**2024/12/18**)

===== Grading =====

Homework Assignments 20%, Participation 10%, Final Exam 40%, Term Paper/Report 30%.

===== References =====
  - //[[http://www.cis.upenn.edu/~jean/gbooks/logic.html|Logic for Computer Science: Foundations of Automatic Theorem Proving]]//, J.H. Gallier, Harper & Row Publishers, 1985. (Note: click on the link to author's free download site.)
  - //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.
  - The Coq Proof Assistant: https://coq.inria.fr.
  - //Interactive Theorem Proving and Program Development//, Y. Bertot and P. Castéran, Springer, 2004.
  - //[[http://www.cis.upenn.edu/~bcpierce/sf/|Software Foundations]]//, B.C. Pierce, C. Casinghino, M. Greenberg, V. Sjöberg, and B. Yorgey. (Note: click on the link to authors' free download site.)
  - //[[http://adam.chlipala.net/cpdt/|Certified Programming with Dependent Types
]]//, A. Chilipala. (Note: click on the link to author's free download site.)
  - //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, Third Edition//, K.R. Apt, F.S. de Boer, and E.-R. Olderog, Springer, 2009.
  - //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, Prentice Hall, 1994.
  - Frama-C: https://www.frama-c.com; Why3: https://www.why3.org; Why3-coq: https://opam.ocaml.org/packages/why3-coq/.
  - //[[https://link.springer.com/book/10.1007/978-3-031-55608-1|Guide to Software Verification with Frama-C]]//, Editors: Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, 2024.
  - //[[https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf|Introduction to C program proof with Frama-C and its WP plugin]]//, Allan Blanchard, 2020.
  - [[https://www.frama-c.com/download/acsl-tutorial.pdf|ACSL Mini-Tutorial]], Virgile Prevosto.
  - //[[https://spivey.oriel.ox.ac.uk/wiki3/files/zrm/zrm.pdf|The Z Notation: A Reference Manual, 2nd Edition]]//, J.M. Spivey, 1992. (Note: click on the link to author's free download site.)
  - //Software Engineering with B//, J.B. Wordsworth, Addison-Wesley, 1996.
  - //Modeling in Event-B: System and Software Engineering//, J.-R. Abrial, Cambridge University Press, 2010.
  - //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.
  - //[[http://www.cs.stanford.edu/~zm/tvors3.html|Temporal Verification of Reactive Systems: Progress]]//, Z. Manna and A. Pnueli, Book Draft, 1996. (Note: click on the link to authors' free download site.)
  - //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.)
Yih-Kuen Tsay's Wiki @ IM.NTU

User Tools

Site Tools

Page Tools
