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. |