Automated Reasoning 2006/2007

This page is updated regularly. Always consult the most recent version.

General

This course is part of the Master programs Computing Science and Artificial Intelligence. It is given in the first half of the first semester (September to November). It is a 5 ECTS course.

Teachers

Wim H. Hesselink
Gerard R. Renardel de Lavalette

Prerequisites

Discrete Structures and Knowledge Representation (from the bachelor program Computing Science), or Introduction to Logic and Advanced Logic (from the bachelor program Artificial Intelligence).

Course description

Reasoning is the ability to make inferences, and automated reasoning is concerned with the design of computing systems that automate, support, or verify this process. This course gives an introduction into this active field of research. It consists of two parts: theorem proving and model checking. A theorem prover assists the user to construct and check proofs. A model checker allows the user to check whether certain properties hold in a model that the user defines. We shall use the theorem prover PVS and the model checker SPIN.

Students will be engaged with the practice of automated reasoning by assignments: providing proofs, designing models, and inferring, verifying and falsifying properties of those models.

Time and place

See the Course schedule.

Examination

Practical assignments and a written exam.

Links

Som useful links:

Week schedule (preliminary, consult the latest version!)

Week 1 (Monday 4 September 2006 - Friday 8 September 2006)

Lecture 1 (Monday): preliminaries. Naive set theory, relations and functions, predicate logic, sequent calculus, lambda calculus. See the handout.

Lecture 2 (Friday): first encounter with PVS. The logic of PVS (Chapter 3 of the PVS Prover guide, will be handed out during the lecture), and the PVS-theorie trans.pvs over the transitive closure of a relation (take a printout of this file to the lecture; assignment 1 is based on this file).

Assignment 1: deadline Friday, September 15, 2006, 17.00 h. It is strongly recommended to start this week with the assignment.

Week 2 (Monday 11 September 2006 - Friday 15 September 2006)

Lecture 3 (Monday): Examples of PVS proofs and proof commands (Chapter 4 of the PVS Prover guide). The handout contains an overview.

Computer lab session (Thursday): hands-on PVS experience with advice and help by Wim Hesselink.

Lecture 4 (Friday): Proving correctness of sequential programs in PVS. Binary Search, swapping array elements.
As a preparation, copy the binary search dump file to a new directory, call pvs, undump the file, print only the files binsearch.pvs and programs.pvs and take them with you to the lecture. Idem for the file pvs_help with contains a short PVS manual.

Assignment 2: deadline Wednesday, September 20, 2006, 17.00 h.

Week 3 (Monday 18 September 2006 - Friday 22 September 2006)

Lecture 5 (Monday): type conditions in PVS, and a crash course Program Correctness.

Computer lab session on Thursday.

No lecture on Friday.

Assignment 3: deadline Tuesday, October 3, 2006, 17.00 h.

Week 4 (Monday 25 September 20063 - Friday 29 September 2006)

Lecture 6 (Monday): proving correctness of concurrent programs in PVS. Peterson's mutual exclusion program: see the PVS file peterson.pvs and the gzipped dump file dumpPeterson.gz.
Mutual exclusion with one binary semaphore: see the PVS file semaMX.pvs and the dump file dumpSema.gz.

Computer lab session on Thursday.

No lecture on Friday.

Week 5 (Monday 2 October 2006 - Friday 6 October 2006)

Lecture 7 (Monday): temporal logic. Modal logic, Kripke models, the temporal logics CTL*, CTL, LTL: see the handout. There is also another handout with a few copies from Chapter 2 and 3 of the book Model Checking by Clarke, Grumberg and Peled.

Computer lab session on Thursday: finalizing assignment 3 (for those who did not make the deadline).

Lecture 8 (Friday): The model checking tool SPIN. See the Introduction to the Model Checker Spin, the Concise Promela reference by Rob Gerth, and the file with some introductory Promela scripts.

Assignment 4: deadline Friday, October 13, 2006, 17.00 h.

Week 6 (Monday 9 October 2006 - Friday 13 October 2006)

Lecture 9 (Monday): Berman and Garay's algorithm for fault-tolerant consensus. See Exercise 1.3 in the Exercise Series from Twente University.

Computer lab session on Thursday: first encounter with SPIN and the language Promela.

Lecture 10 (Friday, final lecture). Working with Spin: acceptance en progress (see the handout). LTL formulae interpreted as finite automata.
Queueing semaphore (NB: an earlier version contained an error: see the remark).

Assignment 5: deadline Friday, October 27, 2006, 17.00 h.

Week 7 (Monday 16 October 2006 - Friday 20 October 2006)

No lectures.

Exam: Tuesday, November 7, 9 - 12 h., Examenhal

See the exams of previous years (the first is in Dutch):October 2003, November 2004, November 2005.
Gerard Renardel (grl@cs.rug.nl)