Fall 2016

(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.

PrerequisitesStudents 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

ProfessorDr. 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/
Course OutlineNote 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)