The Castle of Hagenberg
General Submission Registration Program Location
  • 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.

Program: July 29, July 30.

Thursday, July 29.
09:00-09:30Opening and welcome.
Session 1. Chair: Bruno Buchberger
09:30-10:30 Invited Talk. Vampire: Past, Present and Future.
Andrei Voronkov
10:30-11:00Coffee 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:30Guessing a Conjecture in Enumerative Combinatorics and Proving It With a Computer Algebra System.
Alain Giorgetti.
11:00-12:30Satisfiability of Non-Linear Arithmetic over the Reals.
Harald Zankl, René Thiemann and Aart Middeldorp.
12:30-14:00Lunch at Hofwirt restaurant.
Session 3. Chair: Tudor Jebelean
14:00-14:30Automatic Correction of Firewall Mis-configurations.
Nihel Ben Youssef and Adel Bouhoula.
14:30-15:00Integrating Local Computation Models by Refinement.
Dominique Méry , Mohamed Mosbah, and Mohamed Tounsi.
15:00-15:30Static Verification of Basic Protocols Systems with Unbounded Number of Agents.
Stepan Potiyenko.
15:30-16:00Coffee break.
Session 4. Chair: Gabor Kusper
16:00-16:30From Program Verification to Automated Debugging.
Nikolaj Popov, Tudor Jebelean and Bruno Buchberger.
16:30-17:00Case Studies for Logic Based Synthesis in Theorema.
Alois Altendorfer and Tudor Jebelean.
17:00-17:30A Case Study in Systematic Exploration of Tuple Theory.
Isabela Dramnesc, Tudor Jebelean and Adrian Craciun.
18:00-21:00Conference 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:00Coffee break.
Session 6. Chair: Aart Middeldorp
10:00-10:30Simple Non-Deterministic Strategy in Rewriting and Its Application for Verification.
Alexander Letichevsky, Alexander Letichevsky Jr. and Vladimir Peschanenko.
10:30-11:00Multi-Domain Logic as a Tool for Program Verification.
Gabor Kusper and Tudor Jebelean.
11:00-11:30Coffee break.
Session 7. Chair: Tetsuo Ida
11:30-12:30 Invited Talk. Symbolic Verification for Scientific Discovery.
Wei Li.
12:30-14:00Lunch break.
Session 8. Chair: Nikolaj Popov
14:00-14:30Predicate transformers and system verification.
Oleksandr Letychevskyi and Alexander Letichevsky.
14:30-15:00The RISC ProgramExplorer: Reasoning about Programs as State Relations.
Wolfgang Schreiner.
15:00-15:30Extended Web Services for Computational Origami.
Asem Kasem and Tetsuo Ida.
15:30-16:00Closing Remarks.
16:00-16:30Coffee break.
16:30-17:30Business Meeting.


RISC Software GmBH