Project Seminar Formal Methods in Computer Science (326.038, SS 2005)
Hagenberg Seminar Room (HA 105).
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.
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"
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.
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.
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.
April 27 - May 3
- Wolfgang Schreiner: An Introduction to the Model Checker Spin
May 18 - May 24
- Laura Kovacs: An Invariant Generation Algorithm for Imperative Program Verification in Theorema.
May 25 - May 31
- Franz Lichtenberger:Introduction to CASL, Part 2: Structured Specifications and Libraries
June 1 - June 7
- Wolfgang Schreiner: An Introduction to the PVS Verification System.
June 8 - June 14
- Wolfgang Schreiner: An Introduction to the PVS Verification System (Continuation)
June 22 - June 28
- Nikolaj Popov: Verification of Tail-Recursive Programs.