Weekly outline
 
Project Seminar Formal Methods in Computer Science
(326.038, WS 2005/06)
Time: Wednesday, 10:30-12:00.
Place: Hagenberg Seminar Room (HA 105).
Start: October 5.

In this seminar, we explore current research and systems for specifying and verifying computer programs (specification languages, program verifiers, model checkers, ...). This continues the seminar of the previous semester.

To take part in the seminar, you have to enrol in the KUSSS system. Please also register for this Moodle course (link "Login" on the upper right corner), then you will automatically receive per email all messages posted in the "News" forum below.

Forum News forum
 
1
5 October - 11 October
  1. Wolfgang Schreiner: The Theorem Proving Environments Isabelle and Coq: A Personal Experience (Part 1).
  2. Organization of the Seminar.
Resource The Theorem Proving Environments Isabelle and Coq: A Personal Experience

2
12 October - 18 October
  • Wolfgang Schreiner: The Theorem Proving Environments Isabelle and Coq: A Personal Experience (Part 2).
  • Wolfgang Schreiner: Proceedings of FM 2005 and CAV 2005.

October 17 (RISC Forum):

  • Carsten Sinz: Practical Applications of SAT.
Resource Practical Applications of SAT

3
19 October - 25 October
  • Rebhi Baraka: Querying Mathematical Service Descriptions.
Resource Querying Mathematical Service Descriptions

6
9 November - 15 November
  • Franz Lichtenberger: Introduction to category theory (part 1).
Resource Transparencies 1 to 4 (1368 KB)
Resource Transparencies 5 to 8 (1513 KB)
Resource Transparencies 9 to 12 (1579 KB)

7
16 November - 22 November
  • Andreas Duscher: Stateful Services & Service Orchestration - Technology Overview & PhD Status report.
Resource Stateful services & Service Orchestration

8
23 November - 29 November
  • Franz Lichtenberger: Introduction to category theory (part 2).
Resource Transparencies 13 and 14 (1244 KB)
Resource Transparencies 15 and 16 (1024 KB)
Resource Transparencies 17 to 20 (1831 KB)
Resource Transparencies 21 to 24 (1312 KB)
Resource Transparencies 25 to 28 (1750 KB)
Resource Transparancies 29 to 32 (1569 KB)
Resource Transparencies 33 to 36 (1658 KB)

9
30 November - 6 December
  • Franz Lichtenberger: Introduction to category theory (part 2 continued).
  • Wolfgang Schreiner: The RISC ProofNavigator - A First Status Report.
Resource The RISC Proof Navigator - A First Status Report

10
7 December - 13 December
  • Nikolaj Popov, Laura Kovacs: Report on Formal Methods Workshop.
  • Wolfgang Schreiner: The RISC ProofNavigator - A First Status Report (continued).

15
11 January - 17 January
  • Franz Lichtenberger: Introduction to category theory (part 3).
Resource Transparencies 37 to 40 (2016 KB)
Resource Transparencies 41 to 44 (1765 KB)
Resource Transparencies 45 to 48 (1859 KB)
Resource Transparencies 49 to 52 (2163 KB)

16
18 January - 24 January
  • Weifeng Jiang: Bounded Model Checking
Resource Bounded Model Checking

17
25 January - 31 January
  • Hongping Tao: Counterexample-guided Abstraction Refinement with Lazy Abstraction
Resource Counterexample-guided Abstraction Refinement