Schedule of LPAR 2006

Schedule in printable form (PDF)

[ Sunday | Monday | Tuesday | Wednesday | Thursday | Friday ]


Sunday, 12 November

 9 :00  - 17 :00 Workshops
     6th International Workshop on the Implementation of Logics (IWIL-6)
     2nd International Workshop on Analytic Proof Systems
 17 :00  - 19 :00 Registration
 19 :00  - 21 :00 LPARty

Monday, 13 November

 9 :00  - 10 :00 Registration
 10 :00  - 10 :15 Opening
 10 :15  - 11 :15 Invited Lecture: Higher-Order Termination
   Jean-Pierre Jouannaud
 11 :15  - 11 :30 Coffee Break
 <˘d elign="right">11 :30  - 12 :00 Deciding Satisfiability of Positive Second Order Joinability Formulae
   Sébastien Limet and Pierre Pillot
 12 :00  ╗-&nb3p;>/td>12 :30 SAT Solving for Argument Filterings
   Michael Codish, Peter Schneider-Kamp, Vitaly Lagoon, René Thiemann, and Jürgen Giesl
 12 :30  - 14 :00 Lunch
 14 :00  - 14 :30 Inductive Decidability using Implicit Induction
   Stephan Falke and Deepak Kapur
 14 :30  - 15 :00 Matching Modulo Superdevelopments. Application to Second-Order Matching
   Germain Faure
 15 :00  - 15 :30 Derivational Complexity of Knuth-Bendix Orders Revisited
   Georg Moser
 15 :30  - 16 :00 Coffee Break
 16 :00  - 16 :30 Characterization of ALogtIme by First Order Functional Programs
   Guillaume Bonfante, Jean-Yves Marion, and Romain Péchoux
 16 :30  - 17 :00 Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems
   Frédéric Blanqui and Colin Riba
 17 :00  - 18 :00 Presentation of short papers

Tuesday, 14 November

 9 :00  - 10 :00 Invited Lecture: Disjunctive Logic Programming for Knowledge Representation and Reasoning
   Nicola Leone
 10 :00  - 10 :30 On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus
   Kentaro Kikuchi
 10 :30  - 11 :00 Coffee Break
 11 :00  - 11 :30 Modular Cut-Elimination: Finding Proofs or Counterexamples
   Agata Ciabattoni and Kazushige Terui
 11 :30  - 12 :00 A Semantic Completeness Proof for Tableaux Modulo
   Richard Bonichon and Olivier Hermant
 12 :00  - 12 :30 Saturation up to Redundancy for Tableau and Sequent Calculi
   Martin Giese
 12 :30  - 14 :00 Lunch
 14 :00  - 14 :30 Branching Time Temporal Logic Extended with Presburger Constraints
   Régis Gascon and Laura Bozzelli
 14 :30  - 15 :00 Combining Supervaluation and Degree Based Reasoning under Vagueness
   Christian Fermüller and Robert Kosik
 15 :00  - 15 :30 A Comparison of Techniques for Querying Large Description Logic ABoxes
   Boris Motik and Ulrike Sattler
 15 :30  - 16 :00 A Local System for Intuitionistic Logic
   Alwen Tiu
 16 :00  - 16 :30 Coffee Break
 16 :30  - 17 :00 Reducing Nondeterminism in the Calculus of Structures
   Ozan Kahramanogullari
 17 :00  - 17 :30 A Relaxed Approach to Integrity and Inconsistency in Databases
   Hendrik Decker and Davide Martinenghi
 17 :30  - 18 :00 Automata for Positive Core XPath Queries on Compressed Documents
   Barbara Fila and Siva Anantharaman
 18 :00  - 18 :30 Presentation of short papers

Wednesday, 15 November

 9 :00  - 18 :00 Excursion
 19 :00  - 22 :00 Conference Banquet

Thursday, 16 November

 9 :00  - 9 :30 On Locally Checkable Properties
   Orna Kupferman, Yoad Lustig, and Moshe Vardi
 9 :30  - 10 :00 Deciding Key Cycles for Security Protocols
   Véronique Cortier and Eugen Zalinescu
 10 :00  - 10 :30 Automating Verification of Loops by Parallelization
   Tobias Gedell and Reiner Hähnle
 10 :30  - 11 :00 Coffee Break
 11 :00  - 11 :30 On Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel Systems
   Christel Baier, Nathalie Bertrand, and Philippe Schnoebelen
 11 :30  - 12 :00 Verification Condition Generation via Theorem Proving
   John Matthews, J Moore, Sandip Ray, and Daron Vroon
 12 :00  - 12 :30 An Incremental Approach to Abstraction-Carrying Code
   Elvira Albert, Puri Arenas and German Puebla
 12 :30  - 14 :00 Lunch
 14 :00  - 14 :30 Context-Sensitive Multivariant Assertion Checking in Modular Programs
   Pawel Pietrzak, Jesús Correas, German Puebla, and Manuel Hermenegildo
 14 :30  - 15 :00 Representation of Partial Knowledge and Query Answering in Locally Complete Databases
   Álvaro Cortés-Calabuig, Marc Denecker, Ofer Arieli, and Maurice Bruynooghe
 15 :00  - 15 :30 Sequential, Parallel and Quantified Updates of First-Order Structures
   Philipp Rümmer
 15 :30  - 16 :00 Coffee Break
 16 :00  - 16 :30 Representing Defaults and Negative Information without Negation-as-Failure
   Pablo Fillottrani and Guillermo Simari
 16 :30  - 17 :00 Constructing Camin-Sokal Phylogenies Via Answer Set Programming
   Jonathan Kavanagh, David Mitchell, Eugenia Ternovska, Ján Manuch, Xiaohong Zhao, and Arvind Gupta
 17 :00  - 17 :30 Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
   Gilles Barthe, Benjamin Grégoire, and Fernando Pastawski
 17 :30  - 18 :00 Presentation of short papers

Friday, 17 November

 9 :00  - 9 :30 Boolean Rings for Intersection-Based Satisfiability
   Nachum Dershowitz, Jieh Hsiang, Guan-Shieng Huang, and Daher Kaiss
 9 :30  - 10 :00 Theory Instantiation
   Harald Ganzinger and Konstantin Korovin
 10 :00  - 10 :30 Splitting on Demand in Satisfiability Modulo Theories
   Clark Barrett, Robert Nieuwenhuis, Albert Oliveras and Cesare Tinelli
 10 :30  - 11 :00 Coffee Break
 11 :00  - 11 :30 Delayed Theory Combination vs Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis
   Roberto Bruttomesso, Alessandro Cimatti, Anders Franzen, Alberto Griggio, and Roberto Sebastiani
 11 :30  - 12 :00 Automatic Combinability of Rewriting Based Satisfiability Procedures
   Hélène Kirchner, Silvio Ranise, Christophe Ringeissen, and Duc-Khanh Tran
 12 :00  - 12 :30 To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT(EUF U T)
   Roberto Bruttomesso, Alessandro Cimatti, Anders Franzen, Alberto Griggio, Alessandro Santuari, and Roberto Sebastiani
 12 :30  - 13 :00 Lemma Learning in the Model Evolution Calculus
   Peter Baumgartner, Alexander Fuchs, and Cesare Tinelli
 13 :00  - 14 :30 Lunch

End of LPAR