Venue
Takeshima is a small island next to Nagoya. The venue Hotel Takeshima (faced to but not inside the island) is located 15 minutes walk or 5 minutes by taxi from JR Gamagori Station. The station is about 1 hour from Nagoya Chubu-Kokusai Airport (Centrair).
-
Hotel Takeshima
(map)
- Takeshima Kaigan, Gamagori, Aichi, 443-0031, Japan
Accommodation
- The accommodation fee is 9000 JPY per night. The fee includes breakfast and dinner. Each room will be shared among 3-4 persons.
- Banquet fee: 5,000 yen.
- Wine fee: tba.
Schedule
| 2 (Mon) | 3 (Tue) | 4 (Wed) | 5 (Thu) | 6 (Fri) | |
|---|---|---|---|---|---|
| 9:00 – 12:00 | free discussion | plenary meeting | plenary meeting | free discussion | |
| 12:00 – 13:30 | lunch | ||||
| 13:30 – 17:30 | free discussion | free discussion | plenary meeting | free discussion | |
| 18:30 – | dinner | banquet | dinner | ||
| 20:00 – 21:30 | free discussion | free discussion | free discussion | free discussion | |
Monday
Tuesday
| 13:30 - 14:30 | Cops Meeting (Confluence Problems) (off topic) Hirokawa, Middeldorp, Thiemann, Zankl |
Wednesday
| 9:00 - 12:00 | – Overview and Constrained Rewriting – |
| FWF-JSPS Project: Overview and Expectations from
Austrian Side Aart Middeldorp | |
| CRISYS: Constrained-system Rewriting
Induction System Naoki Nishida | |
| New Ideas on Transformations of
CTRSs Karl Gmeiner | |
| SMT for Polynomial Constraints over Real
Numbers Van Khanh To | |
| 12:00 - 13:30 | – Lunch – |
| 13:30 - 17:30 | – SMT and Completion – |
| TBA: To Beat
Arithmetic Harald Zankl | |
| Ideas on SAT Solvers for Enhancing Efficiency of SMT Solvers Masahiko Sakai | |
| GlueMiniSat 2.2.5: A Fast SAT Solver with
An Aggressive Acquiring Strategy of Glue Clauses Hidetomo Nabeshima | |
| Completion-like Procedures Based on
Constrained Equations Sarah Winkler | |
| 18:30 - 20:00 | – Banquet – |
Thursday
| 9:00 - 12:00 | – Complexity, Certification, and Business Meeting – |
| Short Report on Complexity Nao Hirokawa | |
| Certification of Constrained
Rewriting René Thiemann | |
| Formalizing Kruskal's Tree Theorem in
Isabelle/HOL Christian Sternagel | |
| Business Meeting | |
| 12:00 - 13:30 | – Lunch – |
Friday
Participants
- Hidetomo Nabeshima (University of Yamanashi)
- Nao Hirokawa (JAIST)
- Koji Iwanuma (Yamanashi University)
- Karl Gmeiner (Vienna University of Technology)
- Yoshiharu Kojima (Nagoya University)
- Cynthia Kop (University of Innsbruck)
- Aart Middeldorp (University of Innsbruck)
- Naoki Nishida (Nagoya University)
- Mizuhito Ogawa (JAIST)
- Masahiko Sakai (Nagoya University)
- Haruhiko Sato (Hokkaido University)
- Christian Sternagel (JAIST)
- René Thiemann (University of Innsbruck)
- Van Khanh To (JAIST)
- Sarah Winkler (University of Innsbruck)
- Akihisa Yamada (Nagoya University)
- Harald Zankl (University of Innsbruck)
Attendance
| Kop, Middeldorp, Winkler | 1 | 2 | 3 | 4 | 5 | 6 | 7 |
| Gmeiner, Thiemann | 1 | 2 | 3 | 4 | 5 | 6 | - |
| Nishida | - | 2 | 3 | 4 | 5 | 6 | 7 |
| Kojima, Hirokawa, Sato Sternagel, Yamada, Zankl | - | 2 | 3 | 4 | 5 | 6 | - |
| Sakai | - | 2 | 3 | 4 | 5 | 6m | - |
| To | - | - | 3 | 4 | 5n | - | - |
| Ogawa | - | - | 3 | 4l | - | - | - |
| Nabeshima | - | - | - | 4 | 5 | 6 | - |
| Gramlich, Iwanuma, Kurihara, Moser, Sakata | - | - | - | - | - | - | - |
m: leave early in morning. l: leave lunch time. n: leave night.
Organising Committee
- Nao Hirokawa (JAIST)
- Masahiko Sakai (Nagoya University)
Sponsors
