Advanced formal methods

Information for aform07

Last updated 070525, 08:55

NEWS:

070525: Takehome to be emailed at 9am, not uploaded here.
070429: Assignment #5 uploaded
070416: Slides lecture 8 uploaded. Also exercises in slides lecture 7.
070409: Lecture room from 070410 onwards is 5th floor seminar room, Lindstedtsv. 5, room 4523
070329: Now featuring some project ideas.
070326: Lecture wednesday March 28 dropped. New lectures will be announced after easter.

Advanced formal methods, 5 credits, is a continuation course in formal methods, following up on the course 2D1452 Formal Methods. The course is suitable for final year undergraduates and beginning postgraduate students.

Course contents are intended to vary from year to year. Earlier installations have focused on modelling languages for mobility and security such as the pi-calculus and its derivatives. This years installation focuses on machine-assisted theorem proving in higher order logics and related formalisms. The basic goal is to understand how often very domain-specific theories relevant to computer science and, most often, programming languages, can be formed and used for rigorous, machine-checkable proof. This can be surprisingly useful in many contexts, for instance to analyze communication protocols, programming languages, or specific algorithms.

We cover the theoretical basis for theorem proving and proof search, specific logics and proof systems, proof techniques and the use of theorem provers, and to the extent we have time, some concrete case studies, for instance for modelling of the Java Virtual Machine, or the verification of security protocols. Topics include lambda calculus, natural deduction, higher order logics, term rewriting, recursion and induction, and other material as needed.

Prerequisites: Students must have good background in logic and discrete mathematics. Past exposure to semantics and formal methods is a distinct advantage.

Lecturer: Mads Dam, CSC

Requirements: There will be homework and assignments during the course, and a final take-home exam. Further, each student will need to complete and modelling/verification miniproject, to be presented at a final course workshop in May (to be scheduled). All course elements must be passed. The overall grade will be determined by the take-home exam.

Schedule and locations: Six (6) lectures have been scheduled in advance, check here for timing and locations. Depending on the number of participants we may decide to remove or (probably) add lectures. Changes:

Lecture wednesday March 28 dropped.
New lectures scheduled: 13-15, April 10th, 13-15, April 12th, 9-11. April 17th, 13-15, April 19th, all in room 4523, Lindstedtsvägen 5, 5th floor.
Final workshop: 9-12, may 11th, room 4523
Dates for take home: TBD

Slides and lectures:

Lecture 1, Introduction pdf ppt and start of untyped lambda-calculus pdf ppt, first 6 slides only.

Homework besides those in slides is the following (voluntary) brain teaser:

Prove that the following rule is not derived in the proof system for beta reduction (here -> is the beta indexed version of slide number 6): From t -> t' and s -> s' conclude t s -> t' s'. Hint: Come up with an invariant I(t,t') and show that whenever t -> t' is derivable then I(t,t'), and show secondly that there is an example of t, t', s, s' such that I(t,t'), I(s,s'), but not I(t s, t' s'). Conclude.

Lecture 2, Untyped lambda-calculus until free and bound variables.
Lecture 3, rest of untyped lambda-calculus, simply typed lambda calculus pdf ppt up to and including unique typing and normal forms.
Homework: Exercise 7 in untyped lambda-calculus slides, exercise 1-6 in simply type lambda calculus slides.
Lecture 4, simply type lambda-calculus cont'd, until strong normalization more terms and types, confluence (Andreas)
Homework: Exercise 7-10 in simply typed lambda-calculus slides
Lecture 5, strong normalization, exercises, project ideas (see below)
Homework: Exercise 11-13 in simply typed lambda-calculus slides. Think about projects so we can settle this first thing after easter. Continue with Isabelle, rest of Nipkow-Paulson-Wenzel, ch. 2, and ch. 3. Do exercise 2.4.1 and all exercises in ch 3.
Lecture 6, Isabelle, types and terms pdf ppt
Homework: Finish exercises in Nipkow et al ch 3 + assignment 3
Lecture 7, Isabelle, proofs and simplification pdf ppt
Homework: Exercises in slides
Lecture 8, Isabelle, HOL - higher order logic pdf ppt
Homework: Exercises in slides.
Lecture 9, Isabelle, Sets, inductively defined set pdf ppt
Homework: Exercises in slides.
Reading; Paper by A. Avron, Gentzen-Type Systems, Resolution and Tableaux Journal of Automated Reasoning 10, 265-281 (1993)
Homework: Assignment 5

Assignments:

Assignment #1: Do exercises 1-6 in the slides on untyped lambda-calculus. Extra exercise: Look at the end of slides for lecture 2. Due date: Friday March 23. Drop solutions in my mailtray in CSC, level 4, or email me.
Assignment #2: Do exercise 1, 4, 6, 7, 9, 10 in slides on typed lambda-calculus. Due date: Friday March 30, same procedure as #1 or hand in at lecture.
Assignment #3: Exercise 12 in typed lambda-calculus slides. Exercise 1 and 2 in Isabelle types and terms slides. Due date: Friday April 13. Please submit answer to Isabelle exercise as email attachment. File must be self-contained.
Assignment #4: All exercises in slides for lecture 7-9. Due date Monday April 23. Submit answers to Isabelle exercises as email attachments.
Assignment #5: pdf. Due date Friday May 5.

Project ideas: The general task is to formalize and solve some problem in Isabelle. You are free to suggest your own projects, but please check with me for suitability first. Otherwise, here are a few project ideas:

Security type systems: Formalize and prove type soundness in Isabelle of the Volpano-Smith type system. Paper. See also this survey paper.
Recreate Bond and Anderson's API level attack on the IBM 4758 in Isabelle. Check out this report for background information and pointers.
Use Paulson's method to analyze some suitably complex security protocol(s), for instance in the Avispa suite. Proposal: Start with some simple extension of NSPK and then gradually crank up the ambition level, regarding either protocol or query complexity, or both.
Define and formalize a compiler from untyped or simply typed lambda-calculus to Landin's SECD machine and prove it correct in Isabelle (for some suitable evaluation order). For material on the SECD machine use google.
Model your favourite algorithm and prove some interesting properties about it in Isabelle

General advice is to start as simple as possible and then gradually crank up the ambition level as you get familiar with the problem domain (and with Isabelle)..

Course material: This list will be added to as we move along. I have copies of most material below that can be borrowed for short periods of time.

The Isabelle site. Contains lots of material on Isabelle, including an electronic version of the following tutorial:
Local installation instructions here
T. Nipkow, L. C. Paulson, M. Wenzel: Isabelle/HOL - a Proof Assistant for Higher-Order Logic, LNCS 2283, Springer 2002
B. C. Pierce: Types and Programming Languages. The MIT Press, 2002
B. C. Pierce (ed.): Advanced Topics in Types and Programming Languages, The MIT Press, 2005
H. P. Barendregt: The Lambda Calculus, its Syntax and Semantics. North-Holland, 1994
Alan Robinson, A. Voronkov (eds.): Handbook of Automated Reasoning, Vol. 1 and 2. MIT Press 2001
J. R. Hindley, J. P. Seldin: Introduction to Combinators and Lambda-Calculus, CUP 1986
Demillo, Lipton, and Perlis, Social Processes and Proofs of Theorems and Programs, CACM 79
J Strother Moore, A Mechanized Program Verifier, talk at The Verification Grand Challenge Workshop, Zurich, October 10--13, 2005
The verifying compiler challenge, Tony Hoare, JACM
A. Avron, Gentzen-Type Systems, Resolution and Tableaux Journal of Automated Reasoning 10, 265-281 (1993)
K. Donelly, Hongwei Xi, A Formalization of Strong Normalization for Simply Typed Lambda-Calculus and System F, Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'06), Seattle, WA, August 2006, pdf