Symposium Program

Pre-proceedings are online.
Symposium photos.

Friday, July 23

08:30-09:00: Registration, opening (María Alpuente and Temur Kutsia)

9:00 Invited talk: Bruno Buchberger (Session chair: María Alpuente)

Coffee Break

Session 1 (10:30-12:00)

Chair: Temur Kutsia

  • Dean Voets and Danny De Schreye.
    Non-termination analysis of Logic Programs using Types. (Full paper)
  • Thomas Stroeder, Peter Schneider-Kamp and Jürgen Giesl.
    Dependency Triples for Improving Termination Analysis of Logic Programs with Cut. (Full paper)
  • German Vidal.
    A Hybrid Approach to Conjunctive Partial Deduction. (Extended abstract)

Lunch (12:00-14:00)

Session 2 (14:00-15:00)

Chair: Peter Schneider-Kamp

  • Giovanni Bacci and Marco Comini.
    Abstract Diagnosis of First Order Functional Logic Programs. (Full paper)
  • David Insa and Josep Silva.
    Debugging with Incomplete and Dynamically Generated Execution Trees. (Extended abstract)

Coffee Break

Session 3 (15:30-16:30)

Chair: Marco Comini

  • Elvira Albert, Miguel Gómez-Zamalloa, José Miguel Rojas Siles and Germán Puebla.
    Towards Compositional CLP-based Test Data Generation for Imperative Languages. (Extended abstract)
  • Ángel Herranz and Julio Mariño.
    Executable Specifications in an Object Oriented Formal Notation. (Extended abstract)

Saturday, July 24

9:00 Invited talk: Johann Schumann (Session chair: Fabio Fioravanti)

Coffee Break

Session 4 (10:30-12:30)

Chair: Alicia Villanueva

  • Mathieu Giorgino, Martin Strecker, Ralph Matthes and Marc Pantel.
    Verification of the Schorr-Waite algorithm - From trees to graphs. (Full paper)
  • Jónathan Heras, Vico Pascual and Julio Rubio.
    Proving with ACL2 the correctness of simplicial sets in the Kenzo system. (Full paper)
  • Sakurai Kanako and Kenichi Asai.
    MikiBeta: A General GUI Library for Visualizing Proof Trees. (Extended abstract)
  • Marisa Llorens, Javier Oliver, Josep Silva and Salvador Tamarit.
    A Semantics to Generate the Context-sensitive Synchronized Control-Flow Graph. (Full paper)

Lunch (12:30-13:30)

Trip to Freistadt and Conference Dinner (14:00-22:30)

Freistadt map indicating the social program locations.

Sunday, July 25

9:00 Invited talk: Olivier Danvy (Session chair: Bruno Buchberger)

Coffee Break

Session 5 (10:30-12:30)

Chair: Julio Mariño

  • Hirohisa Seki.
    On Inductive Proofs by Extended Unfold/fold Transformation Rules. (Full paper)
  • Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti and Valerio Senni.
    Program Specialization for Verifying Infinite State Systems: An Experimental Evaluation. (Full paper)
  • Christophe François Olivier Calvès and Maribel Fernández.
    The First-Order Nominal Link. (Extended abstract)
  • Rudolf Berghammer and Sebastian Fischer.
    Simple Functional Programs for Computing Reflexive-transitive Closures. (Extended abstract)

Lunch (12:30-14:00)