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
- Tuesday 10:30-12:30 (until November 28)
- Friday, December 7, 13:00-14:00
- You may view your final exam during office hours in January 2013: Monday 10:30-12:30
Lectures
- Monday 8:30-10:00, SITE Room J0106
- Thursday 10:00-11:30, SITE Room J0106
- Thursday, December 6, 13:00-16:00, SITE Room C0136 (extra class scheduled for project presentations)
- Notes from lectures
- Slides from the introductory lecture
- Paper for introductory lecture
- September 17: The Coq Proof Assistant (Part 1)
- October 11: Programming by Contract example
- Papers on JML:
- October 15: JML lecture notes
- Papers on PCC: (Paper 1, Paper 2)
- Optional: paper with more in-depth coverage of PCC
- October 29: PCC lecture notes
- November 8: Protocol Verification lecture notes
- November 15: The Coq Proof Assistant (Part 2)
- Temporal Logic lecture notes
- 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 0110 Computer Lab 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.)
- Assignment 1, assigned September 10, due Monday, September 17 at 8:30am
- Assignment 2, assigned September 20, due Thursday, October 4 at 10:00am
- Project Proposal, due Monday, October 29. (If you hand it in by October 18, you will get feedback before the October break.)
- Assignment 3, assigned October 18, due Thursday, November 1 at 10:00am
- Assignment 4, assigned November 15, due Thursday, November 29 at 10:00am
- Project report, due Wednesday, December 5
- Monday, December 10, 9:00-12:00, SITE Room J0106
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.
| Topic | Reading | Date |
|---|---|---|
| Introduction to Formal Methods (Setting the Context for the Course) | handout (1 paper) | September 6 |
| Propositional Logic | Chapter 1 (pages 1-40) | September 10-13 |
| An Introduction to the The Coq Proof Development System | Coq Tutorial Sections 1.1-1.3 | September 17-20 |
| Program Verification | Chapter 4 | September 20-October 15 |
| Application: Verification of Java Programs Using JML (Java Modelling Language) | handouts (3 papers) | October 15-18 |
| Application: Proof-carrying Code for the Safety and Security of Mobile Code | handouts (2 papers) | October 18-November 1 |
| Predicate Logic | Chapter 2 (pages 93-122) | November 1-8 |
| Application: Protocol Verification in Predicate Logic | November 8-15 | |
| Predicate Logic in Coq | Coq Tutorial Section 1.4 | November 15 |
| Application: Protocol Verification in Coq | November 15 | |
| Linear Temporal Logic, and Application: Specification of Reactive Systems | Chapter 3 (pages 175-190) | November 19-22 |
| Modal Logic and Agents | Chapter 5 (pages 306-315, 326-331) | November 26-29 |
| Project Presentations | December 3-6 |
