Workshop Program
Gemeindesaal, Castle of Hagenberg
Download schedule.
The proceedings have been published as the RISC Technical Report 08-08
Please note that the order of invited talks has been changes.
Saturday, July 12.
09:00-09:20 | Registration. |
09:20-09:30 | Opening, welcome speech. Bruno Buchberger |
Invited Talk. Session chair: Tetsuo Ida | |
09:30-10:30 | Some Challenges for Automated Theorem Proving. |
Dana Scott. | |
10:30-11:00 | Coffee break. |
Session 1. Chair: Aart Middeldorp | |
11:00-11:30 | A Computer Verified Theory of Compact Sets. |
Russell O'Connor. | |
11:30-12:00 | Designing a Rewriting Induction Prover with an Increased Capability of Non-Orientable Theorems. |
Takahito Aoto. | |
12:00-12:30 | Productivity of Algorithmic Systems. |
Ariya Isihara. | |
12:00-14:00 | Lunch. |
Session 2. Chair: Yukiyoshi Kameyama | |
14:00-14:30 | Aligator for Software Verification. |
Laura Kovacs. | |
14:30-15:00 | Verification of Functional Programs Containing Nested Recursion. |
Nikolaj Popov and Tudor Jebelean. | |
15:00-15:30 | Practical Program Verification by Forward Symbolic Execution: Correctness and Examples |
Madalina Erascu and Tudor Jebelean. | |
15:30-16:00 | Coffee break. |
Session 3. Chair: Tudor Jebelean | |
16:00-16:30 | Lazy Thinking Synthesis of a Groebner Bases Algorithm in Theorema. |
Adrian Craciun. | |
16:30-17:00 | An Automated Tableau Theorem Prover for FO(ID). |
Stephen Bond and Marc Denecker. | |
19:00-22:00 | Workshop dinner. |
Sunday, July 13.
Invited Talk.Session chair: Masahiko Sato | |
09:30-10:30 | Symbolic Computation in Software Science. |
Hoon Hong. | |
10:30-11:00 | Coffee break. |
Session 4. Chair: Mircea Marin | |
11:00-11:30 | External and internal syntax of lambda calculus. |
Masahiko Sato. | |
11:30-12:00 | Strong Normalization of Polymorphic Calculus for Delimited Continuations. |
Yukiyoshi Kameyama and Kenichi Asai. | |
12:00-12:30 | Approximation of String Operations in the PHP String Analyzer. |
Yasuhiko Minamide. | |
12:30-14:00 | Lunch. |
Session 5. Chair: Yasuhiko Minamide. | |
14:00-14:30 | Computational Origami of Angle Quintisection. |
Fadoua Ghourabi, Tetsuo Ida and Hidekazu Takahashi. | |
14:30-15:00 | Experiences with Web Environment Origamium: Examples and Applications. |
Asem Kasem and Tetsuo Ida. | |
15:00-15:30 | Graph rewriting in computational origami. |
Tetsuo Ida and Hidekazu Takahashi. | |
15:30-16:00 | Coffee break. |
16:00-16:30 | SCSS Business meeting. |