Weekly outline
 
Project Seminar Formal Methods in Computer Science (326.038, SS 2005)
Time: Wednesday, 10:30-12:00.
Place: Hagenberg Seminar Room (HA 105).
Start: March 9.

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 register in the KUSSS system. Please also register in Moodle ("Login" at the upper right corner) such that you will receive per email all announcements that we post in the News Forum below.

Forum News forum
 
1
March 9 - March 15
  • Presentation of Franz Lichtenberger: "Introduction to CASL cont'd: partial functions and subsorts"
  • March 14: Presentation of Prof. Armin Biere: "SAT & QBF in Formal Verification"
Resource Introduction to CASL - Basic Specifications
Resource SAT & QBF in Formal Verification

2
March 16 - March 22
  • Rebhi Baraka: A Web Registry for Publishing and Discovering Mathematical Web Services (short talk on a result of the RISC MathBroker project)
  • Andreas Duscher: State of the Art in Semantic Web standards and technologies.
Resource Semantic Web (PPT)
Resource A Web Registry for Publishing and Discovering Mathematical Web Services

6
April 13 - April 19
  • Rebhi Baraka: report on EEE 05 conference.
  • Laura Kovacs and Wolfgang Schreiner: report on VISSAS 05 workshop.
  • Wolfgang Schreiner: report on ETAPS 2005 conference.
Resource Overview on IEEE EEE05
Resource VISSAS 2005 and ETAPS 2005

7
April 20 - April 26
  • Temur Kutsia: Context Sequence Matching for XML
Abstract: Context and sequence variables allow matching to explore term-trees both in depth and in breadth. It makes context sequence matching a suitable computational mechanism for a rule-based language to query and transform XML, or to specify and verify web sites. Such a language would have advantages of both path-based and pattern-based languages. We develop a context sequence matching algorithm and its extension for regular expression matching, and prove their soundness, termination and completeness properties.
Resource Context Sequence Matching for XML

8
April 27 - May 3
  • Wolfgang Schreiner: An Introduction to the Model Checker Spin
Resource An Introduction to the Model Checker Spin

11
May 18 - May 24
  • Laura Kovacs: An Invariant Generation Algorithm for Imperative Program Verification in Theorema.
Resource An Invariant Generation Algorithm for Imperative Program Verification in Theorema

12
May 25 - May 31
  • Franz Lichtenberger:Introduction to CASL, Part 2: Structured Specifications and Libraries
Resource Introduction to CASL, Part 2: Structured Specifications and Libraries
Resource CASL Basic Libraries, copied from the CASL Reference Manual

13
June 1 - June 7
  • Wolfgang Schreiner: An Introduction to the PVS Verification System.
Resource The Prototype Verification System PVS

14
June 8 - June 14
  • Wolfgang Schreiner: An Introduction to the PVS Verification System (Continuation)

16
June 22 - June 28
  • Nikolaj Popov: Verification of Tail-Recursive Programs.