(3 hours of class per week, 3 credits, category T)
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.
Students must satisfy at least one of the following criteria:
- Be enrolled in a computer science or math Ph.D. program
- Be enrolled in a computer science or math Master's program with thesis
- Have a computer science 4-year undergraduate degree
- Be an undergraduate in computer science or math with special permission to enroll
Dr. Amy Felty
562-5800 ext. 6694
- Tuesday 11:30-13:30
- Monday 8:30-10:00, SITE Room C0136
- Thursday 10:00-11:30, SITE Room C0136
- Last class: Wednesday, December 7, 8:30-10:00, SITE Room C0136
- Notes from lectures
- Slides from the introductory lecture
- Paper for introductory lecture
- September 19: The Coq Proof Assistant (Part 1)
- October 13: Programming by Contract example
- Papers on JML:
- October 31: JML lecture notes
- Papers on PCC: (Paper 1, Paper 2)
- Optional: paper with more in-depth coverage of PCC
- November 3: PCC lecture notes
- November 17: Protocol Verification lecture notes
- November 28: Specification of SQR Actions
- Temporal Logic lecture notes
- December 7: The Coq Proof Assistant (Part 2)
- 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 is available online from the University of Ottawa Library. Click here to access it while on campus. It is also available on reserve in the Morisset Library.
- Textbook web page (with www tutor) http://www.cs.bham.ac.uk/research/lics/
35% approximately 7 assignments
35% 2 Term Tests
30% 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.)Assignments
- Each student is required to do each assignment individually.
- Late assignments will not be accepted.
- Assignments will be due at 8:30am on a Monday or 10:00am on a Thursday. They must be submitted by either putting a hard copy in locked assignment box number 2 before class, giving a hard copy to the professor at the beginning of class, or submitting electronically using your Blackboard Learn account. Note: Carleton students can send me their Blackboard Learn usernames and I will add you to the course.
- If you hand in a hard copy, you must staple the pages of your assignment together, and include your Name, Student Number, Course number, and Assignment number.
- If you hand in an electronic copy, you may hand in a single or multiple files in formats such as Word files (.doc), rich text format (.rtf), plain text format (.txt), or PDF (.pdf). Please do not use image files. Include your Name, Student Number, Course number, and Assignment number in every file.
- Assignment 1, assigned September 12, due Monday, September 19 at 8:30am
- Assignment 2, assigned September 22, due Monday, October 3 at 8:30am
- Assignment 3, assigned October 3, due Monday, October 31 at 8:30am
- Assignment 4, assigned November 7, due Thursday, November 17 at 10:00am
- Assignment 5, assigned November 17, due Monday, November 28 at 8:30am
- Assignment 6, assigned December 1, due Monday, December 12 at 10:00am (December 4: Correction to the statement of P6 on page 2 in Question 1)
- Term Test 1: Thursday, October 6
- In class, SITE Room C0136
- Covers material from lectures, textbook, assignments until October 3. This material includes up to the end of Section 4.4 in the textbook, but does not include Section 4.3.3. This material includes both partial and total correctness, but if you are asked to do proofs of Hoare triples, the programs will not contain any loops.
- Closed book
- During the test, you will be provided with copies of Figure 1.2 (natural deduction inference rules for propositional logic), Figure 4.1 (proof rules for partial correctness of Hoare triples), and the file Examples1.v.
- Term Test 2: Monday, November 21
- In class, SITE Room C0136
- Covers material from lectures, textbook and other readings, and assignments on the following topics: JML, PCC, and Chapter 2 (Sections 2.1 and 2.2 only).
- Open book (no electronics)
- Instructions for getting errors in marking corrected
- Final Exam
- Saturday, December 17, 9:30-12:30, Simard Hall (SMD), 60 University, Rooms 222 and 422
- The exam will be open book (no electronics), and will cover all readings and material from class.
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 13 Application: Verification of Java Programs Using JML (Java Modelling Language) handouts (3 papers) October 31-November 3 Application: Proof-carrying Code for the Safety and Security of Mobile Code handouts (2 papers) November 3-10 Predicate Logic Chapter 2 (pages 93-122) November 10-17 Application: Protocol Verification in Predicate Logic November 17-28 Linear Temporal Logic, and Application: Specification of Reactive Systems Chapter 3 (pages 175-190) December 1-5 Predicate Logic in Coq Coq Tutorial Section 1.4 December 5-7 Application: Protocol Verification in Coq December 7