FTP 2007 - International Workshop on First-Order Theorem Proving
Liverpool, UK, September 12-13 2007

Liverpool Waterfront at Night

The workshop takes place in the First Floor Lecture Theatre of the Ashton Building. See facilities for additional information.

Wednesday, 12 September 2007
From 9:00 Registration
9:25 - 9:30 Introduction to FTP 2007
Session 1 (Joint session with FroCoS'07) Chair: Ullrich Hustadt
9:30 - 10:30 Invited talk
Hierarchical and Modular Reasoning in Complex Theories: The Case of Local Theory Extension
Viorica Sofronie-Stokkermans
10:30 - 11:00 Coffee Break
Session 2 (Joint session with FroCoS'07)
11:00 - 11:35 Combining Proof-Producing Decision Procedures
Silvio Ranise, Christophe Ringeissen, and Duk Khanh Tran
11:35 - 12:10 Towards an Automatic Analysis of Web Service Security
Yannick Chevalier, Denis Lugiez, and Michael Rusinowitch
12:10 - 12:45 Certification of Automated Termination Proofs
Evelyne Contejan, Piere Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain
12:45 - 14:05 Lunch
14:05 - 14:15 Further Details for FTP 2007 Participant
Session 3 Chair: Christophe Ringeissen
14:15 - 14:50 Inductive Proof Search Modulo
Fabrice Nahon, Claude Kirchner and Helene Kirchner
14:50 - 15:25 Extending Poitín to Handle Explicit Quantification
Humayun Kabir and Geoff Hamilton
15:25 - 15:55 Coffee Break
Session 4 Chair: Michael Rusinovitch
15:55 - 16:30 Developing Modal Tableaux and Resolution Methods via First-Order Resolution
Renate Schmidt
16:30 - 17:05 Reasoning Automatically about Termination and Refinement
Georg Struth
17:05 - 17:35 Business Meeting
19:00 Conference Dinner
Racquet Club (Hargreaves Buildings, 5 Chapel Street, Liverpool L3 9AG)

Thursday, 13 September 2007
Session 5 Chair: Hans de Nivelle
9:00 - 10:00 Invited Talk
Aspects of First-order Reasoning in the KeY system
Martin Giese
10:00 - 10:30 ProofBuilder: An Interactive Prover for Students, with Extensive Capabilities
Hugh McGuire
10:30 - 11:00 Coffee Break
Session 6 Chair: Georg Struth
11:00 - 11:35 Labeled tableaux for distributed temporal logic
David Basin, Carlos Caleiro, Jaime Ramos and Luca Viganó
11:35 - 12:10 What First Order Theorem Provers Do For Monodic Temporal Reasoning
Ullrich Hustadt
12:10 - 13:45 Lunch
Session 7 Chair: Silvio Ranise
13:45 - 14:45 Invited Talk
Applying FTPs in Formal Software Safety Certification
Bernd Fischer
14:45 - 15:15 Coffee Break
Session 8 Chair: Renate Schmidt
15:15 - 15:50 A Graph-based Strategy for the Selection of Hypotheses
Jean-Francois Couchot and Thierry Hubert
15:50 - 16:25 Redundancy in the Geometric Resolution Calculus
Hans de Nivelle
16:25 - 17:00 Edit and Verify
Radu Grigore and Michal Moskal