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
- Thursday 10:00-12:00 (except December 6)
- Thursday, December 6, 14:00-16:00
Lectures
- Wednesday 14:30-17:30, Fauteux, Room 136
- Notes from lectures
- Transparencies from the introductory lecture
- Paper for introductory lecture
- September 19: The Coq Proof Assistant (Part 1)
- Papers on JML:
- JML lecture notes
- Papers on PCC: (Paper 1, Paper 2)
- Optional: paper with more in-depth coverage of PCC
- PCC lecture notes
- Protocol Verification lecture notes
- October 31-November 7: The Coq Proof Assistant (Part 2)
- LTL 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 Wednesday, September 19 at 14:30.
- Assignment 2, assigned September 26, due Wednesday, October 10 at 14:30.
- Project Proposal, due Wednesday, October 17
- Assignment 3, assigned October 18, due Wednesday, October 31 at 14:30.
- Sample Solutions for Assignment 3
- Assignment 4, assigned October 31, due Wednesday, November 14 at 14:30.
- Extra credit: 5.4 2(e).
- Solution by Jun Biao Yan (main proof and derived lemma)
- Solution by Cong Wang
Final Exam
- Date: Wednesday, December 5, 14:30-17:30, Fauteux, Room 136
- 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.
- September 12
- Introduction to Formal Methods (Setting the Context for the Course), handout (1 paper)
- Propositional Logic, Chapter 1 (pages 1-40)
- September 19
- Propositional Logic (continued)
- An Introduction to the The Coq Proof Development System, Coq Tutorial Sections 1.1-1.3
- September 26, October 3
- Program Verification, Chapter 4
- October 10
- Application: Verification of Java Programs Using JML (Java Modelling Language), handouts (3 papers)
- Application: Proof-carrying Code, a brief introduction
- October 17
- Application: Proof-carrying Code for the Safety and Security of Mobile Code, handouts (2 papers)
- Predicate Logic, Chapter 2 (pages 93-122)
- October 24
- Predicate Logic (continued)
- Application: Protocol Verification in Predicate Logic
- October 31
- Protocol Verification (continued)
- Predicate Logic in Coq, Coq Tutorial Section 1.4
- November 7
- Application: Protocol Verification in Coq
- Linear Temporal Logic, Chapter 3 (pages 175-187)
- Application: Specification of Reactive Systems
- November 14
- Modal Logic and Agents, Chapter 5 (pages 306-315, 326-331)
- November 21
- Project Presentations
- November 28
- Project Presentations
- December 5
- Final Exam