Ruurd Kuiper

Ruurd Kuiper

Address

Formal Methods Group
Computing Science Department
Eindhoven University of Technology
P.O. Box 513, NL-5600 MB Eindhoven
The Netherlands

Phone: +31 40 2474122
Email: wsinruur@win.tue.nl
Room: HG 7.13

Information Java

Voor de Java cursussen 2IP65 en 2IP70 (voorheen 2Z820) zie 2IP65, 2IP70

Het tentamen is open boek, dwz Schaum en andere informatie mag meegebracht en gebruikt worden, geen netwerk uiteraard.

Puur, opportunistisch, voor het tentamen is van belang uit Schaum voornamelijk hoofdstuk 2, (bv tiling dus niet) en dan:

Voor het doel van 2IP70 van belang uit Schaum, per hoofdstuk: Een overzicht van wat op het college is behandeld, met verwijzingen naar Schaum (globale verwijzing: "cf", gedetailleerder verwijzing via pagina's) is onder:
  • Notes
  • Information 2IF25

    The exam results are available on the web now. Preferred time for questions is friday 5/2, 12.30 - 13.30, HG 7.13.
    Note: following a remark by several students, a correction to some of te results has been made - those whose marks have changed have been informed, the corrected results are on the web now.

    NB The exam is open book, i.e., books, lecture notes etc. are allowed to be used - a computer isn't allowed!

    The material to be studied is provided below as links, and in part as handouts at the lectures. For those that didn't attend (all) lectures: copies-to-be-copied of the handouts (some material already provided in multiple copies) can be found next to the secretary's office, HG 7.22.

    Part 1 Automated Program Verification with Propositional Modal Model Checking - Ruurd Kuiper. Material: under links below.

    Outline of contents

    The system

    Propositional /modal /linear time) logic

    Propositional branching time logic

    Model checking for modal/branching logic

    Model checking for linear time logic

    LTL Model check example: Mutual Exclusion

    The SMV system manual


    Part 2 Propositional and First order Theorem Proving - Erik de Vink. Material as described under the following links.

    NB The most important topic is from Logic for Computer Science: Foundations of Automatic Theorem Proving, Gallier, J., (available on-line), chapter 5, and from that section 5.4. The book is available on-line at:

    Logic for Computer Science, Gallier, J.

    Propositional Logic

    First Order Logic

    First Order theorem proving example (2IF55 of course should be 2IF25, sorry)


    Intermediate example exam about first two parts of IF25


    Part 3 (Automated) Program Verification with First order Logic - Kees Huizing. Material: Handouts and slides on studyweb.


    Part 4 Program Verification with First Order Linear Time Temporal Logic - Ruurd Kuiper. Material: Handouts Manna/Pnueli.

    Encore, not necessary for the exam: Handout about the incompleteness/undecidability of First Order Logic with Arithmatic.


    Exam January 19, 2010

    Answers for Assignment 1

    Answers for Assignment 2

    Answers for Assignment 3

    Answers for Assignment 4

    Back to the Formal Methods Group home page.