Schedule:
- July 28: Arrival.
- July 29: Conference opening. Invited talk. Contributed talks. Conference dinner.
- July 30: Invited talks. Contributed talks. Closing. Business meeting
- July 31: Departure.
Thursday, July 29.
| 08:30-09:00 | Registration. |
| 09:00-09:30 | Opening and welcome. |
| Session 1. Chair: Bruno Buchberger | |
| 09:30-10:30 | Invited Talk. Vampire: Past, Present and Future. |
| Andrei Voronkov | |
| 10:30-11:00 | Coffee break. |
| Session 2. Chair: Wolfgang Schreiner | |
| 11:00-11:30 | A Formal Proof of Confluence for an Infinitely Generated Noncommutative Polynomial Ideal Parametrized over Integro-Differential Algebras. |
| Loredana Tec. | |
| 11:00-11:30 | Guessing a Conjecture in Enumerative Combinatorics and Proving It With a Computer Algebra System. |
| Alain Giorgetti. | |
| 11:00-12:30 | Satisfiability of Non-Linear Arithmetic over the Reals. |
| Harald Zankl, René Thiemann and Aart Middeldorp. | |
| 12:30-14:00 | Lunch at Hofwirt restaurant. |
| Session 3. Chair: Tudor Jebelean | |
| 14:00-14:30 | Automatic Correction of Firewall Mis-configurations. |
| Nihel Ben Youssef and Adel Bouhoula. | |
| 14:30-15:00 | Integrating Local Computation Models by Refinement. |
| Dominique Méry , Mohamed Mosbah, and Mohamed Tounsi. | |
| 15:00-15:30 | Static Verification of Basic Protocols Systems with Unbounded Number of Agents. |
| Stepan Potiyenko. | |
| 15:30-16:00 | Coffee break. |
| Session 4. Chair: Gabor Kusper | |
| 16:00-16:30 | From Program Verification to Automated Debugging. |
| Nikolaj Popov, Tudor Jebelean and Bruno Buchberger. | |
| 16:30-17:00 | Case Studies for Logic Based Synthesis in Theorema. |
| Alois Altendorfer and Tudor Jebelean. | |
| 17:00-17:30 | A Case Study in Systematic Exploration of Tuple Theory. |
| Isabela Dramnesc, Tudor Jebelean and Adrian Craciun. | |
| 18:00-21:00 | Conference Dinner at Ars Electronica Linz, Ars-Electronica-Straße 1. |
Friday, July 30.
| Session 5. Chair: Tudor Jebelean | |
| 08:30-09:30 | Invited Talk. Challenges in Formalizing Geometric Reasoning: A Case Study of Pick's Theorem. |
| John Harrison. | |
| 09:30-10:00 | Coffee break. |
| Session 6. Chair: Aart Middeldorp | |
| 10:00-10:30 | Simple Non-Deterministic Strategy in Rewriting and Its Application for Verification. |
| Alexander Letichevsky, Alexander Letichevsky Jr. and Vladimir Peschanenko. | |
| 10:30-11:00 | Multi-Domain Logic as a Tool for Program Verification. |
| Gabor Kusper and Tudor Jebelean. | |
| 11:00-11:30 | Coffee break. |
| Session 7. Chair: Tetsuo Ida | |
| 11:30-12:30 | Invited Talk. Symbolic Verification for Scientific Discovery. |
| Wei Li. | |
| 12:30-14:00 | Lunch break. |
| Session 8. Chair: Nikolaj Popov | |
| 14:00-14:30 | Predicate transformers and system verification. |
| Oleksandr Letychevskyi and Alexander Letichevsky. | |
| 14:30-15:00 | The RISC ProgramExplorer: Reasoning about Programs as State Relations. |
| Wolfgang Schreiner. | |
| 15:00-15:30 | Extended Web Services for Computational Origami. |
| Asem Kasem and Tetsuo Ida. | |
| 15:30-16:00 | Closing Remarks. |
| 16:00-16:30 | Coffee break. |
| 16:30-17:30 | Business Meeting. |
