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
- Friday 10:30-12:30 (until December 9)
Lectures
- Monday 8:30-10:00, Lamoureux Hall (LMX), Room 390
- Thursday 10:00-11:30, Colonel By Hall (CBY), Room C206
- Notes from lectures
- Slides from the introductory lecture
- Paper for introductory lecture
- September 19: The Coq Proof Assistant (Part 1)
- October 6: Programming by Contract example
- Papers on JML:
- October 6-13: JML lecture notes
- Papers on PCC: (Paper 1, Paper 2)
- Optional: paper with more in-depth coverage of PCC
- October 17: PCC lecture notes
- Protocol Verification lecture notes
- November 14: 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
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 12, due Monday, September 19 at 8:30am
- Assignment 2, assigned September 29, due Thursday, October 13 at 10:00am
- Project Proposal, due Monday, October 17
- Assignment 3, assigned October 20, due Thursday, November 10 at 10:00am
- Assignment 4, assigned November 14, due Monday, November 28 at 8:30am
- Project report, due Wednesday, December 7
- Monday, December 12, 9:00-12:00, Lamoureux Hall (LMX), Room 360
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 8 |
| Propositional Logic | Chapter 1 (pages 1-40) | September 12-15 |
| An Introduction to the The Coq Proof Development System | Coq Tutorial Sections 1.1-1.3 | September 19-22 |
| Program Verification | Chapter 4 | September 22-October 6 |
| Application: Verification of Java Programs Using JML (Java Modelling Language) | handouts (3 papers) | October 6-13 |
| Application: Proof-carrying Code for the Safety and Security of Mobile Code | handouts (2 papers) | October 17-31 |
| Predicate Logic | Chapter 2 (pages 93-122) | October 31-November 7 |
| Application: Protocol Verification in Predicate Logic | November 7-14 | |
| Predicate Logic in Coq | November 14 | |
| Application: Protocol Verification in Coq | November 14 | |
| Linear Temporal Logic, and Application: Specification of Reactive Systems | Chapter 3 (pages 175-190) | November 17-21 |
| Modal Logic and Agents | Chapter 5 (pages 306-315, 326-331) | November 28-December 1 |
| Project Presentations (click to see schedule) | December 5-8 |
