Symposium Program (tentative)

13:55: Opening of the Symposium

14:00 - 15:30: Session 1 (chair: German Vidal)

• Thomas Stroeder, Peter Schneider-Kamp, Jürgen Giesl, Fabian Emmes and Carsten Fuhs. A Linear Operational Semantics for Termination and Complexity Analysis of ISO Prolog
• Olivier Namet, Maribel Fernandez and Helene Kirchner. A strategy language for graph rewriting
• Céline Dandois and Wim Vanhoof. Clones in logic programs and how to detect them

16:00 - 17:30: Session 2 (chair: Wim Vanhoof)

• Paulo Moura. Meta-Predicate Semantics
• Jose F. Morales, Manuel Hermenegildo and Rémy Haemmerlé. Modular Extensions for Modular (Logic) Languages
• Nik Sultana. Work in progress: A prototype refactoring tool based on a mechanically-verified core

9:00 - 10:00: LOPSTR Invited Talk (chair: German Vidal)

• John Gallagher. Program Analysis With Regular Types

  Finite Tree Automata (FTAs) are mathematical "machines" that define recognisable sets of tree-structured terms; they provide a foundation for describing a variety of computational structures such as data, computation states and computation traces. The field of finite tree automata attracts growing attention from researchers in automatic program analysis and verification; there have been promising applications using FTAs in program specialisation, data flow analysis for a variety of languages, term-rewriting systems, shape analysis of pointer-based data structures, polymorphic type inference, binding time analysis, termination analysis, infinite state model checking and cryptographic protocol analysis. The study of FTAs originated in formal language theory and logic, but unlike string automata, which have been widely applied in computer science, especially in compiler theory, tree automata have not yet entered the mainstream of computing theory. In this talk, frameworks for designing static analyses based on tree automata are outlined. They can be used both prescriptively, for expressing and checking intended properties of programs, or descriptively, for capturing approximations of the actual states arising from computations. Computational techniques for handling FTAs efficiently are covered. Finally we look at extensions that go beyond the expressiveness of tree automata, as well as integrating arithmetic constraints.

10:30 - 12:30: Session 3 (chair: Danny De Schreye)

• Wim Vanhoof. On the partial deduction of non-ground meta-interpreters
• Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti and Valerio Senni. Using Real Relaxations During Program Specialization
• Hirohisa Seki. Proving Properties of  Co-logic Programs by Unfold/Fold Transformations
• Rafael Caballero, Adrian Riesco, Alberto Verdejo and Narciso Marti-Oliet. Simplifying Questions in Maude Declarative Debugger by Transforming Proof Trees

14:00 - 15:30: Session 4 (chair: Hiroisha Seki)

• Giovanni Bacci, Marco Comini, Marco A. Feliú and Alicia Villanueva. Automatic Synthesis of Specifications for Curry Programs - Extended Abstract
• Jesus Almendros-Jimenez, Rafael Caballero, Yolanda García-Ruiz and Fernando Saenz-Perez. A Declarative Embedding of XQuery  in a Functional-Logic Language
• Soichiro Hidaka, Zhenjiang Hu, Kazuhiro Inaba, Hiroyuki Kato, Kazutaka Matsuda, Keisuke Nakano and Isao Sasano. Marker-directed optimization of UnCAL graph transformations

16:00 - 17:30: Session 5 (chair: Alberto Pettorossi)

• Elvira Albert, Miguel Gomez-Zamalloa and José Miguel Rojas Siles. Resource-driven CLP-based Test Case Generation
• Jon Sneyers and Daniel De Schreye. Probabilistic Termination of CHRiSM Programs
• Paolo Pilozzi and Daniel De Schreye. Improved termination analysis of CHR using self-sustainability analysis

9:00 - 10:00: PPDP/LOPSTR Invited Talk (chair: Peter Schneider-Kamp)

• Fritz Henglein. Dynamic Symbolic Computation for Domain-Specific Language Implementation

  A domain-specific language (DSL) is a specification language designed to facilitate programming in a certain application domain. A well-designed DSL reflects the natural structure of the modeled domain, enforces abstraction, and its implementation exploits domain-specific properties for safety and performance. Expounding on the latter, in this talk we describe a method for opportunis- tically adding symbolic computation at run-time to a base implementation that employs a general-purpose data structure, so as to improve asymptotic perfor- mance without changing the compositional structure of the language.

10:30 - 11:30: PPDP/LOPSTR Invited Talk

• Vitaly Lagoon. The Challenges of Constraint-Based Test Generation

11:30 - 12:30: Session 6 (chair: Kazutaka Matsuda)

• Pedro Cabalar and Stephane Demri. Automata-based Computation of Temporal Equilibrium Models
• Romain Demeyer and Wim Vanhoof. Proper Granularity for Atomic Sections in Concurrent Programs

Lunch

Excursion and Banquet