FroCoS 2011

FroCoS 2011: 8th International Symposium
Frontiers of Combining Systems

Saarbrücken, Germany, October 5 - 7, 2011


(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:00Invited 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