|
CAV
|
ICLP
|
IJCAR
|
| |
08:45‑09:00 (Metropolitan A/B)
Introduction and Welcome
|
09:00‑10:00 (Metropolitan A/B)
David Dill
I Think I Voted: E-voting vs. Democracy [ppt]
|
10:00‑10:30
Break |
10:30‑11:00 (Metropolitan A)
Martin De Wulf, Laurent Doyen, Tom Henzinger and Jean-Francois Raskin
Antichains: A New Algorithm for Checking Universality of Finite Automata
|
10:30‑11:00 (Cirrus)
Martin Gebser
and Torsten Schaub
Tableau Calculi for Answer Set Programming
|
10:30‑11:00 (Metropolitan B)
Tobias Nipkow
and Gertrud Bauer
Flyspeck I: Tame Graphs
|
11:00‑11:30 (Metropolitan A)
Orna Kupferman
, Moshe Y. Vardi and Nir Piterman
Safraless Compositional Synthesis
|
11:00‑11:30 (Cirrus)
Luciano Caroprese, Sergio Greco, Cristina Sirangelo and Ester Zumpano
Declarative Semantics of Production Rules for Integrity Maintenance
|
11:00‑11:30 (Metropolitan B)
Volker Sorge
, Andreas Meier, Roy McCasland
and Simon Colton
The Automatic Construction of Isotopy Invariants
|
11:30‑12:00 (Metropolitan A)
Sudeep Juvekar
and Nir Piterman
Minimizing Generalized Buchi Automata
|
11:30‑12:00 (Cirrus)
Remy Haemmerle
and Francois Fages
Modules for Prolog Revisited
|
11:30‑12:00 (Metropolitan B)
Sylvie Boldo
Pitfalls of a full floating-point proof: example on the formal proof of the Veltkamp/Dekker algorithms
|
12:00‑12:15 (Metropolitan A)
Luca de Alfaro
, Marco Faella, B. Thomas Adler, Leandro Dias Da Silva, Axel Legay, Vishwanath Raman
and Pritam Roy
Ticc: A Tool for Interface Compatibility and Composition
|
12:00‑12:30 (Cirrus)
Diptikalyan Saha
and C.R. Ramakrishnan
A Local Algorithm for Incremental Evaluation of Tabled Logic Programs
|
12:00‑12:30 (Metropolitan B)
Geoff Sutcliffe
, Stephan Schulz
, Koen Claessen
and Allen Van Gelder
Using the TPTP Language for Writing Derivations and Finite Interpretations
|
12:15‑12:30 (Metropolitan A)
Sébastien Bardin
, Jerome Leroux
and Gérald Point
FAST Extended Release
|
12:30‑14:00
Lunch break |
14:00‑14:30 (Metropolitan A)
Jochen Eisinger
and Felix Klaedtke
Don't Care Words with Application to the Automata-based Approach for Real Addition
|
14:00‑14:30 (Cirrus)
Jon Sneyers
, Tom Schrijvers
and Bart Demoen
Memory reuse for CHR
|
14:00‑14:30 (Metropolitan B)
Jordi Levy
, Manfred Schmidt-Schauss
and Mateu Villaret
Stratified Context Unification is NP-complete
|
14:30‑15:00 (Metropolitan A)
Bruno Dutertre
and Leonardo de Moura
A Fast Linear-Arithmetic Solver for DPLL(T)
|
14:30‑15:00 (Cirrus)
Sergio Antoy
and Michael Hanus
Overlapping Rules and Logic Variables in Functional Logic Programs
|
14:30‑15:00 (Metropolitan B)
Kaustuv Chaudhuri
, Frank Pfenning
and Greg Price
A logical characterization of forward and backward chaining in the inverse method
|
15:00‑15:30 (Metropolitan A)
Keijo Heljanko
, Tommi Junttila
, Misa Keinänen
, Martin Lange
and Timo Latvala
Bounded Model Checking for Weak Alternating Buchi Automata
|
15:00‑15:30 (Cirrus)
Sebastian Brand and Roland H.C. Yap
Towards "Propagation = Logic + Control"
|
15:00‑15:30 (Metropolitan B)
Andrei Paskevich
Connection Tableaux with Lazy Paramodulation
|
15:30‑16:00 (Metropolitan A)
Roman Gershman, Maya Koifman and Ofer Strichman
Deriving small unsatisfiable cores with dominators
|
15:30‑16:00 (Cirrus)
Gregory James Duck
, Sebastian Brand
and Peter Stuckey
ACD Term Rewriting
|
15:30‑16:00 (Metropolitan B)
Peter Baumgartner
and Renate Schmidt
Blocking and Other Enhancements for Bottom-Up Model Generation Methods
|
16:00‑16:30
Break |
16:30‑17:30 (Metropolitan A)
Manuvir Das
Formal Specifications on Industrial-Strength Code - From Myth to Reality [ppt]
|
16:30‑19:00 (Cirrus)
Prolog Contest |
16:30‑17:30 (Metropolitan B)
Bruno Buchberger
Mathematical Theory Exploration [pdf]
|
| |
|
