CSDL - Proceedings L

Conference Organization (PDF)

pp. x

Organizing Committee (PDF)

pp. xi

Reviewers (PDF)

pp. xii

Plenary Talk

Formal Verification of Infinite State Systems Using Boolean Methods (PDF)

Randal E. Bryant, Carnegie Mellon University, USA

pp. 3-4

Session 1: Complexity and Decidability

Two-Variable Logic on Words with Data (Abstract)

Mikolaj Bojanczyk, Warsaw University

Anca Muscholl, LIAFA, Paris VII

Thomas Schwentick, Dortmund University

Luc Segoufin, INRIA, Paris XI

Claire David, LIAFA, Paris VII

pp. 7-16

PDF

LTL with the Freeze Quantifier and Register Automata (Abstract)

Stephane Demri, INRIA Futurs, France

Ranko Lazic, University of Warwick, UK

pp. 17-26

PDF

Fixed-Parameter Hierarchies inside PSPACE (Abstract)

Guoqiang Pan, Rice University, USA

Moshe Y. Vardi, Rice University, USA

pp. 27-36

PDF

The Boundedness Problem for Monadic Universal First-Order Logic (Abstract)

Martin Otto, Technische Universitat Darmstadt, Germany

pp. 37-48

PDF

Session 2: Concurrency

A Congruence Rule Format for Name-Passing Process Calculi from Mathematical Structural Operational Semantics (Abstract)

Marcelo Fiore, University of Cambridge

Sam Staton, University of Cambridge

pp. 49-58

PDF

On the Expressiveness of Linearity vs Persistence in the Asychronous Pi-Calculus (Abstract)

Catuscia Palamidessi, INRIA, France

Vijay Saraswat, IBM TJ Watson Research Lab, USA

Frank D. Valencia, CNRS, France

Bjorn Victor, Uppsala University, Sweden

pp. 59-68

PDF

Saturated Semantics for Reactive Systems (Abstract)

Filippo Bonchi, University of Pisa

Barbara Konig, University of Duisburg-Essen

Ugo Montanari, University of Pisa

pp. 69-80

PDF

Session 3: Pushdown Systems

On Model-Checking Trees Generated by Higher-Order Recursion Schemes (Abstract)

C.-H. L. Ong, Oxford University, UK

pp. 81-90

PDF

Monadic Chain Logic Over Iterations and Applications to Pushdown Systems (Abstract)

Dietrich Kuske, Universitat Leipzig, Germany

Markus Lohrey, Universitat Stuttgart, Germany

pp. 91-100

PDF

An Automata-Theoretic Approach for Model Checking Threads for LTL Propert (Abstract)

Vineet Kahlon, NEC Labs America, USA

Aarti Gupta, NEC Labs America, USA

pp. 101-110

PDF

On Typability for Rank-2 Intersection Types with Polymorphic Recursion (Abstract)

Tachio Terauchi, University of California, Berkeley, USA

Alex Aiken, Stanford University, USA

pp. 111-122

PDF

Invited Talk

Adapting Logics (PDF)

Andreas Blass, Microsoft Research, USA

pp. 123

Session 4: Logics of Program

Managing Digital Rights using Linear Logic (Abstract)

Adam Barth, Stanford University, USA

John C. Mitchell, Stanford University, USA

pp. 127-136

PDF

Variables as Resource in Hoare Logics (Abstract)

Matthew Parkinson, Middlesex University, UK

Richard Bornat, Middlesex University, UK

Cristiano Calcagno, University of London, UK

pp. 137-146

PDF

Independence and Concurrent Separation Logic (Abstract)

Jonathan Hayman, University of Cambridge

Glynn Winskel, University of Cambridge

pp. 147-156

PDF

Matching Explicit and Modal Reasoning about Programs: A Proof Theoretic Delineation of Dynamic Logic (Abstract)

Daniel Leivant, Indiana University, USA

pp. 157-168

PDF

Session 5: Proof Theory

Context Semantics, Linear Logic and Computational Complexity (Abstract)

Ugo Dal Lago, Universite Paris 13, France

pp. 169-178

PDF

Obsessional Cliques: A Semantic Characterization of Bounded Time Complexity (Abstract)

Olivier Laurent, CNRS - Paris 7, France

Lorenzo Tortora de Falco, Roma III, Italy

pp. 179-188

PDF

Conditional Lower Bound for a System of Constant-Depth Proofs with Modular Connectives (Abstract)

Alexis Maciel, Clarkson University, USA

Toniann Pitassi, University of Toronto, Canada

pp. 189-200

PDF

Session 6: Model Theory

A Characterisation of First-Order Constraint Satisfaction Problems (Abstract)

Benoit Larose, Concordia University, Canada

Cynthia Loten, Royal Military College of Canada, Canada

Claude Tardif, Royal Military College of Canada, Canada

pp. 201-210

PDF

First Order Formulas with Modular Ppredicates (Abstract)

Laura Chaubard, Universit?e Paris VII, France

Jean-Eric Pin, Universit?e Paris VII, France

Howard Straubing, Boston College, USA

pp. 211-220

PDF

On Tractability and Congruence Distributivity (Abstract)

Emil Kiss, Eotvos University, Hungary

Matthew Valeriote, McMaster University, Canada

pp. 221-230

PDF

PSPACE Bounds for Rank-1 Modal Logics (Abstract)

Lutz Schroder, Universitat Bremen

Dirk Pattinson, University of Leicester

pp. 231-242

PDF

Avoiding Determinization (Abstract)

Orna Kupferman, Hebrew University, Israel

pp. 243-254

PDF

Session 7: Temporal Logics and Automata

From Nondeterministic Buchi and Streett Automata to Deterministic Parity Automata (Abstract)

Nir Piterman, Ecole Polytechnique F?ed?eral de Lausanne (EPFL)

pp. 255-264

PDF

Memoryful Branching-Time Logic (Abstract)

Orna Kupferman, Hebrew University, Israel

Moshe Y. Vardi, Rice University, USA

pp. 265-274

PDF

Faster Solutions of Rabin and Streett Games (Abstract)

Nir Piterman, EPFL, Switzerland

Amir Pnueli, Weizmann Institute of Science, Israel

pp. 275-284

PDF

Bounds in w-Regularity (Abstract)

Mikolaj Bojanczyk, LIAFA, France

Thomas Colcombet, CNRS/IRISA, France

pp. 285-296

PDF

Session 8: Lambda Calculus

Head Normal Form Bisimulation for Pairs and the \lambda\mu-Calculus (Abstract)

Soren B. Lassen, Google, Inc.

pp. 297-306

PDF

A Proof of Strong Normalisation using Domain Theory (Abstract)

Thierry Coquand, Chalmers Tekniska Hijgskola, Sweden

Arnaud Spiwack, Ecole Norrnale SupCrieure de Cachan, France

pp. 307-316

PDF

Boolean Algebras for Lambda Calculus (Abstract)

G. Manzonetto, Universite Paris 7, France

A. Salibra, Universita Ca?Foscari di Venezia, Italy

pp. 317-326

PDF

Normalisation is Insensible to \lambda-Term Identity or Difference (Abstract)

Makoto Tatsuta, National Institute of Informatics, Japan

Mariangiola Dezani-Ciancaglini, Dipartimento di Informatica, Italy

pp. 327-338

PDF

Shaken Foundations or Groundbreaking Realignment? A Centennial Assessment of Kurt G?del?s Impact on Logic, Mathematics, and Computer Science (Abstract)

Keynote Session: Celebrating Birth Centennial of Kurt Godel

John W. Dawson, Jr., Penn State York

pp. 339-341

PDF

Provable Implementations of Security Protocols (PDF)

Andrew D. Gordon, Microsoft Research

pp. 345-346

Session 9: Timed and Stochastic Systems

Stochastic Games with Branching-Time Winning Objectives (Abstract)

Tomas Brazdil, Masaryk University, Czech Republic

Vaclav Bro?zek, Masaryk University, Czech Republic

Vojtech Forejt, Masaryk University, Czech Republic

Antonin Kucera, Masaryk University, Czech Republic

pp. 349-358

PDF

Coinductive Proof Principles for Stochastic Processes (Abstract)

Dexter Kozen, Cornell University, USA

pp. 359-366

PDF

Control in o-minimal Hybrid Systems (Abstract)

Patricia Bouyer, LSV - CNRS & ENS de Cachan, France

Thomas Brihaye, Universite de Mons-Hainaut, Belguim

Fabrice Chevalier, LSV - CNRS & ENS de Cachan, France

pp. 367-378

PDF

Session 10: Verification

An Abstraction-Refinement Framework for Multi-Agent Systems (Abstract)

Thomas Ball, Microsoft Research, USA

Orna Kupferman, Hebrew University, Israel

pp. 379-388

PDF

Temporal Logics and Model Checking for Fairly Correct Systems (Abstract)

Daniele Varacca, Imperial College London, UK

Hagen V?lzer, Universit?t zu L?beck, Germany

pp. 389-398

PDF

3-Valued Abstraction: More Precision at Less Cost (Abstract)

Sharon Shoham, Technion, Israel

Orna Grumberg, Technion, Israel

pp. 399-410

PDF

Session 11: Approximations

Approximation Schemes for First-Order Definable Optimisation Problems (Abstract)

Anuj Dawar, University of Cambridge, U.K.

Martin Grohe, Humboldt-Universitat zu Berlin, Germany

Stephan Kreutzer, Humboldt-Universitat zu Berlin, Germany

Nicole Schweikardt, Humboldt-Universitat zu Berlin, Germany

pp. 411-420

PDF

Approximate Satisfiability and Equivalence (Abstract)

Eldar Fischer, Technion, Israel

Frederic Magniez, Universite Paris-Sud, France

Michel de Rougemont, Universite Paris II, France

pp. 421-430

PDF

Author Index

Author Index (PDF)

pp. 431