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.
Prerequisites
-
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
Professor
-
Dr. Amy Felty
SITE 5-068
562-5800 ext. 6694
afelty@site.uottawa.ca
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 is available online from the University of Ottawa Library. Click here to access it while on campus.
- Textbook web page (with www tutor) http://www.cs.bham.ac.uk/research/lics/
-
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 |
|---|---|
| Introduction to Formal Methods (Setting the Context for the Course) | handout (1 paper) |
| Propositional Logic | Chapter 1 (pages 1-40) |
| An Introduction to the The Coq Proof Development System | Coq Tutorial Sections 1.1-1.3 |
| Program Verification | Chapter 4 |
| Application: Verification of Java Programs Using JML (Java Modelling Language) | handouts (3 papers) |
| Application: Proof-carrying Code for the Safety and Security of Mobile Code | handouts (2 papers) |
| Predicate Logic | Chapter 2 (pages 93-122) |
| Application: Protocol Verification in Predicate Logic | |
| Linear Temporal Logic, and Application: Specification of Reactive Systems | Chapter 3 (pages 175-190) |
| Predicate Logic in Coq | Coq Tutorial Section 1.4 |
| Application: Protocol Verification in Coq | |
| Modal Logic and Agents | Chapter 5 (pages 306-315, 326-331) |
