| | 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 |
|
| | 11 |
: | 30 |
- | 12 |
: | 00 |
Deciding Satisfiability of Positive Second Order
Joinability Formulae |
| | |
Sébastien Limet and Pierre Pillot |
|
| | 12 |
: | 00 |
- | 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 |
| | 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 |
| | 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 |
| | 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 |