Program for LOPSTR 2003

Monday 25 August

9h00-10h00 ICFP invited talk

10h30-12h30 Specification and Synthesis

• Predicate synthesis from inductive proof attempt of faulty conjectures. Moussa Demba, Khaled Bsaïes and Francis Alexandre.
• Specification and Synthesis of Hybrid Automata for Physics-Based Animation. Thomas Ellman.
• Adding Concrete Syntax to a Prolog-Based Program Synthesis System. Bernd Fischer and Eelco Visser.
• Specifying Object-Oriented Systems in Computational Logic. Kung-Kiu Lau and Mario Ornaghi.

14h15-15h45 Verification

• Building Satisfiability Procedures for Verification: The Case Study of Sorting Algorithms. Abdessamad Imine and Silvio Ranise.
• Formal Development and Verification of Approximation Algorithms using Auxiliary Variables. Rudolf Berghammer and Markus Müller-Olm.
• Formal Reasoning About Efficient Data Structures: A Case Study in ACL2. José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo and Francisco-Jesús Martín Mateos.

16h15-17h45 Analysis

• A Program Transformation for Backwards Analysis of Logic Programs. John P. Gallagher.
• An Efficient Staging Algorithm for Binding-Time Analysis. Takuma Murakami, Zhenjiang Hu, Kazuhiko Kakehi and Masato Takeichi.
• Proving termination with adornments. Alexander Serebrenik and Danny De Schreye.

Tuesday August 26

9h00-10h00 ICFP Invited Talk

10h30-12h30 Transformation

• Constructively Characterizing Fold and Unfold. Tjark Weber and James Caldwell.
• Deterministic Second-order Patterns in Program Transformation Tetsuo Yokoyama, Zhenjiang Hu, and Masato Takeichi.
• From Interpreter to Logic Engine: A Functional Derivation. Dariusz Biernacki and Olivier Danvy.
• Linearization by Program Transformation. Sandra Alves and Mário Florido.

14h15-15h15 Invited Talk

Inductive Theorem Proving by Program Specialisation: Generating proofs for Isabelle using Ecce. Michael Leuschel (work with Helko Lehmann)

15h15-15h45 Specialisation

Provable Correct Code Generation: A Case Study. Qian Wang and Gopal Gupta.

Wednesday August 27

9h00-10h30 Constraints

• Simplification of database integrity constraints revisited: A transformational approach. Henning Christiansen and Davide Martinenghi.
• Integration and Optimization of Rule-based Constraint Solvers. Slim Abdennadher and Thom Frühwirth.
• Introducing ESRA, a Relational Language for Modelling Combinatorial Problems. Pierre Flener, Justin Pearson, and Magnus Ågren.

11h30-12h30 PLI Invited Talk

Understanding aspects. Mitchell Wand