|
|
PROGRAM (Changes in the program for October 6th)
Wednesday, October 5
| | 09:15-09:30 |
Welcome |
|---|
| | 09:30-10:30 |
Session 1: Invited Talk (Chair: Cesare Tinelli) |
| | |
Size-Change Termination and Satisfiability
for Linear-Time Temporal Logics |
| | |
Martin Lange
|
| |
10:30-11:00 |
Coffee Break |
| | 11:00-12:30 |
Session 2 (Chair: Silvio Ghilardi) |
| | 11:00 |
The modal logic of equilibrium models
|
| | |
Luis Fariñas Del Cerro, Andreas Herzig
|
| |
11:30 |
The Complexity of Reversal-Bounded Model-Checking
|
| | |
Marcello Bersani, Stephane Demri
|
| |
12:00 |
A Semantic Account for Modularity in Multi-Language Modelling of Search Problems |
| | |
Shahab Tasharrofi, Eugenia Ternovska
|
| |
12:30-14:00 |
Lunch break |
| | 14:00-15:30 |
Session 3: Invited Tutorial (Chair: Roberto Sebastiani) |
| | 14:00 |
Logical Analysis of Hybrid Systems: The KeYmaera Approach |
| | |
André Platzer
|
| |
15:30-16:00 |
Coffee Break |
| | 16:00-17:00 |
Session 4 (Chair: Pascal Fontaine) |
| | 16:00 |
Sharing is Caring: Combination of Theories
|
| | |
Dejan Jovanovic, Clark Barrett
|
| |
16:30 |
Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT
|
| | |
Alberto Griggio, Quoc-Sang Phan, Roberto Sebastiani, Silvia Tomasi
|
| |
18:00 |
Reception |
Thursday, October 6
| | 09:00-10:30 |
Session 5 (Chair: Martin Lange) |
| | 9:00 | Invited talk |
| | |
Tailoring Temporal Description Logics for Reasoning
over Temporal Conceptual Models
|
| | |
Alessandro Artale |
| | 10:00 |
On the undecidability of fuzzy Description Logics with GCIs and product t-norm
|
| | |
Franz Baader, Rafael Peñaloza
|
| |
10:30-11:00 |
Coffee Break |
| | 11:00-12:00 |
Session 6 (Chair: Christoph Weidenbach) |
| | 11:00 |
Modular Termination and Combinability
for Superposition Modulo Counter Arithmetic
|
| | |
Christophe Ringeissen, Valerio Senni |
| |
11:30 |
Congruence Closure of Compressed Terms in Polynomial Time
|
| | |
Manfred Schmidt-Schauss, David Sabel, Altug Anis
|
| | 12:00-13:00 |
Business meeting |
| |
13:00-14:00 |
Lunch break |
| |
14:00 |
Meeting in front of Building E1 7(conference site) |
| | 15:00-18:30 |
Excursion |
| | 18:30 |
Conference Dinner |
|
|
Friday, October 7
| | 09:00-10:30 |
Session 7 (Chair: Philipp Rümmer) |
| | 09:00 |
Invited talk |
| | |
Automatic Proof and Disproof in Isabelle/HOL
|
| | |
Tobias Nipkow |
| | 10:00 |
Generalized and Formalized Uncurrying
|
| | |
Christian Sternagel, René Thiemann
|
| |
10:30-11:00 |
Coffee Break |
| | 11:00-12:30 |
Session 8 (Chair: Christophe Ringeissen) |
| | 11:00 |
Expressing Polymorphic Types in a Many-Sorted Language |
| | |
François Bobot, Andrei Paskevich |
| |
11:30 |
Harnessing First Order Termination Provers Using Higher Order Dependency Pairs
|
| | |
Carsten Fuhs, Cynthia Kop |
| |
12:00 |
Controlled Term Rewriting |
| | |
Florent Jacquemard, Yoshiharu Kojima, Masahiko Sakai
|
| |
12:30-14:00 |
Lunch break |
| | 14:00-15:30 |
Session 9 (Chair: Viorica Sofronie-Stokkermans) |
| | 14:00 |
Combining theories: the Ackerman and Guarded Fragments |
| | |
Carlos Areces, Pascal Fontaine |
| | 14:30 |
A Combination of Rewriting and Constraint Solving for the Quantifier-free
Interpolation of Arrays with Integer Difference Constraints |
| | |
Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise |
| |
15:00 |
SUP(NLA) -- Combining Superposition and Non-Linear Arithmetic |
| | |
Andreas Eggers, Evgeny Kruglov, Karsten Scheibler, Stefan Kupferschmid,
Tino Teige, Christoph Weidenbach
|
| |
15:30 |
Concluding Remarks |
|
Contact:
For further informations please send
an e-mail to sofronie@mpi-inf.mpg.de
|
|
