|
GALOP
|
HyLo
|
LCC
|
LICS
|
PAuL
|
PCC
|
RTA
|
RULE
|
SAT
|
SSPV
|
UNIF
|
WRS
|
| |
| |
08:55‑09:00 (Suite 2928)
Opening |
|
|
|
|
|
|
|
|
|
|
09:00‑10:00 (Suite 2928)
Patrick Blackburn
Hybrid Logic and Temporal Semantics
|
09:00‑09:05 (Suite 3002)
Welcome
|
09:00‑10:00 (Suite 2628)
Claude Kirchner
Rewriting (your) Calculus [pdf]
|
09:00‑10:00 (Suite 2628)
Claude Kirchner
Rewriting (your) Calculus [pdf]
|
09:05‑10:00 (Suite 3002)
Anatol Slissenko
Decidability of verification in predicate logics of probability [pdf]
|
09:15‑09:30 (Metropolitan B)
Welcoming Remarks
|
09:30‑10:30 (Suite 3102)
Madhusudan Parthasarathy
Automata theory for nested structures [pdf]
|
09:30‑10:30 (Suite 3128)
John C Mitchell
Computationally Sound Formal Logic for Network Security Protocols [ppt]
|
09:30‑10:30 (Metropolitan B)
Andrew Appel
A Very Modal Model of a Modern, Major, General Type System
|
09:45‑10:30 (Metropolitan A)
Orna Grumberg
Hybrid BDD and All-SAT Method for Model Checking [ppt]
|
10:00‑10:30 (Suite 2928)
Moritz Hardt
and Gert Smolka
Higher-Order Syntax and Saturation Algorithms for Hybrid Logic
|
10:00‑10:30 (Suite 3002)
Sandra Batista
A Note on Spaced Bounded Interactive Proof Systems and Martingales
|
10:00‑10:30 (Suite 2628)
Francisco Lopez-Fraguas and Jose Miguel Cleva
Semantic determinism and functional logic program properties
|
10:00‑10:30 (Suite 2828)
Naoki Nishida
, Tomohiro Mizutani and Masahiko Sakai
Transformation for Refining Unraveled Conditional Term Rewriting Systems
|
10:30‑11:00
Break |
11:00‑11:45 (Suite 3102)
Aleksandar Dimovski and Ranko Lazic
Compositional Software Model Checking using Game Semantics and Learning Assumptions
|
11:00‑12:00 (Suite 2928)
Valeria de Paiva
Constructive Hybrid Logics and Contexts [pdf]
|
11:00‑11:45 (Suite 3128)
Patrick Baillot
and Marco Pedicini
An Embedding of the BSS Model of Computation in Light Affine Lambda-Calculus
|
|
11:00‑11:30 (Suite 3002)
Sayan Mitra
and Nancy Lynch
Approximate Simulations for Task-Structured Probabilistic I/O Automata
|
11:00‑11:30 (Metropolitan B)
Amal Ahmed |
|
11:00‑11:30 (Suite 2628)
Victor Winter
Model-driven Transformation-based Generation of Java Stress Tests
|
|
11:00‑11:45 (Metropolitan A)
Aarti Gupta
Verifying C Programs using SAT-based model checking [pdf]
|
11:00‑11:30 (Suite 3228)
Max Tuengerthal, Ralf Kuesters
and Mathieu Turuani
Implementing a Unification Algorithm for Protocol Analysis with XOR
|
11:00‑11:30 (Suite 2828)
Horatiu Cirstea, Germain Faure, Maribel Fernández
, Ian Mackie and Francois-Regis Sinot
New Evaluation Strategies for Functional Languages
|
11:30‑12:00 (Suite 3002)
Celine Kuttler
, Cedric Lhoussaine
and Joachim Niehren
A Stochastic Pi-Calculus for Concurrent Objects
|
11:30‑12:00 (Metropolitan B)
Adriana Compagnoni
Information Flow Analysis for Low-Level Languages
|
11:30‑12:00 (Suite 2628)
Alcino Cunha
and Joost Visser
Strongly Typed Rewriting For Coupled Software Transformation
|
11:30‑12:00 (Suite 3228)
Pascal Lafourcade
, Denis Lugiez
and Ralf Treinen
ACUNh: Unification and Disunification Using Automata Theory
|
11:30‑12:00 (Suite 2828)
Mercedes Hidalgo-Herrero, Alberto Verdejo
and Yolanda Ortega-Mallen
Using Maude and its strategies for analyzing Eden semantics
|
11:45‑12:30 (Suite 3102)
Alexander Rabinovich and Amit Shomrat
Long Games and the Church Synthesis Problem
|
11:45‑12:30 (Suite 3128)
Yevgeniy Makarov
Comparing efficiency of functions provable in classical and constructive logics
|
11:45‑12:30 (Metropolitan A)
Ofer Strichman
Decision Heuristics based on an Abstraction/Refinement model [ppt]
|
12:00‑12:30 (Suite 2928)
Martin Mundhenk
and Thomas Schneider
Undecidability of Multi-modal Hybrid Logics
|
12:00‑12:30 (Suite 3002)
Alessandro Tiberi
Probabilistic Configuration Theories
|
12:00‑12:30 (Metropolitan B)
Dachuan Yu
Toward More Typed Assembly Languages for Confidentiality [ppt]
|
12:00‑12:30 (Suite 2628)
Emanuel Kitzelmann
and Ute Schmid
Inducing Constructor Systems from Example-Terms by Detecting Syntactical Regularities
|
12:00‑12:30 (Suite 3228)
Paliath Narendran
and Pavithra Ramarathnam
Unification modulo ACUI with collapsing homomorphisms
|
12:00‑12:30 (Suite 2828)
Muck van Weerdenburg
An account of implementing applicative term rewriting
|
12:30‑14:00
Lunch break |
14:00‑14:45 (Suite 3102)
Russ Harmer
An analysis of innocent interaction
|
14:00‑15:00 (Suite 2928)
Ian Horrocks
Hybrid Logics and Ontology Languages [ppt]
|
14:00‑14:45 (Suite 3128)
Johann A. Makowsky
Logical and Computational Aspects of Graph Polynomials: A Survey
|
|
14:00‑15:00 (Suite 3002)
Krishnendu Chatterjee
Simple Stochastic omega-Regular Games [pdf]
|
14:00‑15:00 (Metropolitan B)
Ian Stark
Resource Guarantees and PCC: 50 ways1 to say it with a proof [pdf]
|
|
14:00‑15:00 (Suite 2628)
Dick Kieburtz
Programmed Strategies for Program Verification [ppt]
|
|
14:00‑14:45 (Metropolitan A)
Sharad Malik
Optimization and Relaxation in SAT Search [pdf]
|
14:00‑14:30 (Suite 3228)
Sjaak Smetsers
and Arjen van Weelden
Bracket Abstraction Preserves Typability
|
14:00‑15:00 (Suite 2628)
Dick Kieburtz
Programmed Strategies for Program Verification [ppt]
|
14:30‑15:00 (Suite 3228)
Edwin Westbrook
Pattern Solutions to Higher-Order Unification Problems
|
14:45‑15:30 (Suite 3102)
Andrea Schalk
Composition via traces
|
|
14:45‑15:30 (Metropolitan A)
Alessandro Cimatti
Reasoning about Bit Vector programs with Decision Procedures [ppt]
|
15:00‑15:30 (Suite 2928)
Nicole Bidoit
and Dario Colazzo
Testing XML constraint satisfiability
|
15:00‑15:30 (Suite 3002)
Andrzej Murawski
and Joel Ouaknine
On Probabilistic Program Equivalence and Refinement
|
15:00‑15:30 (Cedar)
Session 4: Posters |
15:00‑15:30 (Suite 2628)
Florent Kirchner and Francois-Regis Sinot
Rule-Based Operational Semantics for an Imperative Language
|
15:00‑15:30 (Suite 3228)
Franz Baader
and Alexander Okhotin
Complexity of language equations with one-sided concatenation and all Boolean operations
|
15:00‑15:30 (Suite 2828)
Claudio Sacerdoti Coen
Reduction and conversion strategies for the Calculus of (co)Inductive Constructions: Part I
|
15:30‑16:00
Break |
16:00‑16:45 (Suite 3102)
Olivier Laurent
The anatomy of innocence revisited
|
16:00‑16:30 (Suite 2928)
Andre Platzer
Towards a Hybrid Dynamic Logic for Hybrid Dynamic Systems
|
|
|
16:00‑17:00 (Suite 3002)
Javier Esparza
Computing rewards for probabilistic pushdown systems [pdf]
|
16:00‑16:30 (Cedar)
Session 5: Posters (continued) |
|
16:00‑16:30 (Suite 2628)
Peter Olveczky
and Jose Meseguer
Recent Advances in Real-Time Maude
|
|
16:00‑16:45 (Metropolitan A)
Robert Nieuwenhuis
The new architecture and solvers in the Barcelogic tool for SAT modulo theories [pdf]
|
16:00‑16:30 (Suite 3228)
Jorge Coelho
and Mário Florido
Unification with Flexible Arity Symbols: a Typed Approach
|
16:00‑16:30 (Suite 2828)
Karl Trygve Kalleberg
and Eelco Visser
Strategic Graph Rewriting
|
16:30‑17:00 (Suite 2928)
Tadeusz Litak
and Balder ten Cate
Topological Perspective on the Hybrid Proof Rules
|
16:30‑17:00 (Metropolitan B)
Tamara Rezk
Certificate Translation [pdf]
|
16:30‑17:00 (Suite 2628)
Fernando Rosa-Velardo
Coding Mobile Synchronizing Petri Nets into Rewriting Logic
|
16:30‑17:00 (Suite 3228)
Temur Kutsia
and Mircea Marin
Solving Regular Constraints for Hedges and Contexts
|
16:30‑17:00 (Suite 2828)
Sandra Alves
, Maribel Fernández
, Mario Florido and Ian Mackie
The Power of Closed Reduction Strategies
|
| |
|
17:00‑17:30 (Suite 2928)
Katsuhiko Sano
A Hybridization of Irreflexive Modal Logics
|
17:00‑17:30 (Suite 3002)
Vaclav Brozek
On Decidability and Complexity of Stochastic Pushdown Games
|
17:00‑17:30 (Metropolitan B)
Zhong Shao
A Translation from Typed Assembly Languages to Certified Assembly Programming [ppt]
|
17:00‑17:30 (Suite 2628)
Session 5: Discussion: Rule-based programming -- what's next? |
17:00‑17:30 (Suite 3228)
Adel bouhoula and Florent Jacquemard
Automating Sufficient Completeness Check for Conditional and Constrained TRS
|
17:00‑17:30 (Suite 2828)
Session 5: WRS Business Meeting |
17:30‑18:00 (Suite 2928)
Thomas Bolander
, Jens Ulrik Hansen and Michael Reichhardt Hansen
Decidability of a Hybrid Duration Calculus
|
17:30‑18:00 (Suite 3002)
Vaclav Brozek, Tomas Brazdil, Vojtech Forejt and Antonin Kucera
Reachability in Recursive Markov Decision Processes
|
|
|
|
|
18:00‑18:30 (Suite 2928)
Jason Reed
Hybridizing a Logical Framework
|
|
| |
19:00‑21:00 (Grand Ballroom C)
LICS Reception |
19:00‑21:00 (Grand Ballroom A)
RTA Reception |
19:00‑21:00 (Grand Ballroom B)
SAT Reception |
