Methodologies in formal software specification, development, and verification. The use of theorem proving, automated deduction, and other related formal methods for software correctness. Applications in program verification, mobile code safety, and protocol verification.
Professor
-
Dr. Amy Felty
SITE 5-068
562-5800 ext. 6694
afelty@site.uottawa.ca
Office Hours
- Wednesday 10:30-12:30 (except December 3)
- Wednesday, December 3, 12:30-13:30 and 14:00-15:00, or by appointment
Lectures
- Monday 8:30-10:00, MacDonald Room 120
- Thursday 10:00-11:30, Vanier Room 283
- Notes from lectures
- Transparencies from the introductory lecture
- Paper for introductory lecture
- September 15: The Coq Proof Assistant (Part 1)
- October 2: Programming by Contract example
- Papers on JML:
- October 6: JML lecture notes
- Papers on PCC: (Paper 1, Paper 2)
- Optional: paper with more in-depth coverage of PCC
- October 9: PCC lecture notes (October 19: minor errors corrected)
- Protocol Verification lecture notes
- October 30: The Coq Proof Assistant (Part 2)
- Temporal Logic lecture notes (updated November 30)
- Modal logic lecture notes
Textbook
- Logic in Computer Science: Modelling and Reasoning about Systems, Michael R.A. Huth and Mark D. Ryan, Cambridge University Press, 2nd edition, 2004.
- The textbook will be available at Benjamin Books, 122 Osgoode Street.
- Textbook web page (with www tutor) http://www.cs.bham.ac.uk/research/lics/
-
33% approximately 4 short assignments
33% Term project or paper. (To be presented to the class at the end of the term.)
34% Final Exam
Accounts and Software
-
For Assignment 2 and some later assignments, you will use the Coq
Proof Assistant. If you want to use it on the machines in the SITE
graduate lab (STE 2051) and don't have an account, you will have to
get one. (If you are not a SITE student, you must be registered in the
course to get an account. If you are not, see me first.)
Assignments
- Assignment 1, assigned September 8, due Monday, September 15 at 8:30am
- Assignment 2, assigned September 25, due Thursday, October 9 at 10:00am
- Project Proposal, due Thursday, October 16
- Assignment 3, assigned October 21, due Monday, November 3 at 8:30am
- Assignment 4, assigned November 6, due Thursday, November 20 at 10:00am
- Extra Credit: Find a natural deduction proof for the following in modal logic KT45: [](p -> []q) -> [](<>p -> q), due Monday, November 24 at 8:30am
Final Exam
- Date: December 4, 8:30-11:30
- SITE Room F0126
- Open Book
- 34% of Final Mark
Course Outline
Note that this schedule is subject to change during the semester. This course will cover logic-based formal methods, and will concentrate on applications. We will study enough logic to understand these applications. Some background in logic is useful, but not required. Reading assignments listed below are in the course textbook. They will be supplemented by handouts. For links to electronically available material, see "Notes from lectures" above.
| Topic | Reading | Date |
|---|---|---|
| Introduction to Formal Methods (Setting the Context for the Course) | handout (1 paper) | September 4 |
| Propositional Logic | Chapter 1 (pages 1-40) | September 8, 11 |
| An Introduction to the The Coq Proof Development System | Coq Tutorial Sections 1.1-1.3 | September 15 |
| Program Verification | Chapter 4 | September 18-October 2 |
| Application: Verification of Java Programs Using JML (Java Modelling Language) | handouts (3 papers) | October 6 |
| Application: Proof-carrying Code for the Safety and Security of Mobile Code | handouts (2 papers) | October 9-20 |
| Predicate Logic | Chapter 2 (pages 93-122) | October 20-23 |
| Application: Protocol Verification in Predicate Logic | October 23-30 | |
| Predicate Logic in Coq | Coq Tutorial Section 1.4 | October 30 |
| Application: Protocol Verification in Coq | November 3 | |
| Linear Temporal Logic, and Application: Specification of Reactive Systems | Chapter 3 (pages 175-191) | November 3-6 |
| Computation Tree Logic, and Application: Model Checking | Chapter 3 (pages 191-192, 207-229) | November 10-13 |
| Modal Logic and Agents | Chapter 5 (pages 306-315, 326-331, 331-336, 339-343) | November 17-24 |
| Project Presentations | November 27 | |
| Review | December 1 |