The Community for Technology Leaders
Logic in Computer Science, Symposium on (2001)
Boston, Massachusetts
June 16, 2001 to June 19, 2001
ISBN: 0-7695-1281-X
TABLE OF CONTENTS

Foreword (PDF)

pp. x
Invited Talk - Chair: Joseph Y. Halpern

Probabilistic Polynomial-Time Process Calculus and Security Protocol Analysis (Abstract)

J. Mitchell , Stanford University
A. Ramanathan , Stanford University
V. Teague , Stanford University
A. Scedrov , University of Pennsylvania
pp. 0003
Session 1 - Chair: Jean-Pierre Jouannaud

Deconstructing Shostak (Abstract)

Harald Rueß , SRI International
Natarajan Shankar , SRI International
pp. 0019

A Decision Procedure for an Extensional Theory of Arrays (Abstract)

Clark W. Barrett , Stanford University
Aaron Stump , Stanford University
Jeremy Levitt , 0-In Design Automation, Inc.
David L. Dill , Stanford University
pp. 0029

On Ordering Constraints for Deduction with Built-In Abelian Semigroups, Monoids and Groups (Abstract)

Guillem Godoy , Technical University of Catalonia
Robert Nieuwenhuis , Technical University of Catalonia
pp. 0038
Invited Talk - Chair: Jean-Pierre Jouannaud

Successive Approximation of Abstract Transition Relations (Abstract)

Satyaki Das , Stanford University
David L. Dill , Stanford University
pp. 0051
Session 2 - Chair: Pawel Urzyczyn

A Bound on Attacks on Payment Protocols (Abstract)

Scott D. Stoller , SUNY at Stony Brook
pp. 0061
Session 3 - Chair: Radha Jaghadeesan

Semantics of Name and Value Passing (Abstract)

Daniele Turi , University of Edinburgh
Marcelo Fiore , University of Cambridge
pp. 0093

A Fully Abstract Game Semantics of Local Exceptions (Abstract)

J. Laird , University of Sussex
pp. 0105

A Universal Characterization of the Closed Euclidean Interval (Abstract)

Martín H. Escardó , University of Birmingham
Alex K. Simpson , University of Edinburgh
pp. 0115
Invited Talk - Chair: Gordon Plotkin
Session 4 - Chair: Michel de Rougemont

On Definability of Order in Logic with Choice (Abstract)

Tapani Hyttinen , University of Helsinki
Taneli Huuskonen , University of Helsinki
pp. 0167
Invited Talk - Chair: Erich Graedel
Session 5 - Chair: Erich Graedel

A Second-Order System for Polytime Reasoning Using Gr?del's Theorem (Abstract)

Antonina Kolokolova , University of Toronto
Stephen Cook , University of Toronto
pp. 0177

The Crane Beach Conjecture (Abstract)

Nicole Schweikardt , Johannes Gutenberg-Universit?t Mainz
Clemens Lautemann , Johannes Gutenberg-Universit?t Mainz
David A. Mix Barrington , University of Massachusetts
Neil Immerman , University of Massachusetts
Denis Thérien , McGill University
pp. 0187

An n! Lower Bound on Formula Size (Abstract)

Micah Adler , UMass, Amherst
Neil Immerman , UMass, Amherst
pp. 0197
Session 6 - Chair: Nevin Heintze

Dependent Types for Program Termination Verification (Abstract)

Hongwei Xi , University of Cincinnati
pp. 0231
Short Paper Session - Chair: Joseph Y. Halpern
Invited Talk - Chair: Ron van der Meyden

Foundational Proof-Carrying Code (Abstract)

Andrew W. Appel , Princeton University
pp. 0247
Session 7 - Chair: Parosh Abdulla

Intuitionistic Linear Logic and Partial Correctness (Abstract)

Dexter Kozen , Cornell University
Jerzy Tiuryn , Warsaw University
pp. 0259

Perturbed Turing Machines and Hybrid Systems (Abstract)

Eugene Asarin , VERIMAG
Ahmed Bouajjani , LIAFA, University of Paris 7
pp. 0269

Deterministic Generators and Games for Ltl Fragments (Abstract)

Salvatore La Torre , University of Pennsylvania
Rajeev Alur , University of Pennsylvania
pp. 0291
Session 8 - Chair: Adolfo Piperno
Session 9 - Chair: Hubert Comon

Focus Games for Satisfiability and Completeness of Temporal Logic (Abstract)

Colin Stirling , University of Edinburgh
Martin Lange , University of Edinburgh
pp. 0357

Safety and Liveness in Branching Time (Abstract)

Richard Trefler , AT&T Labs-Research
Panagiotis Manolios , University of Texas, Austin
pp. 0366
Short Papers
Invited Talk - Chair: Michel de Rougemont
Session 10 - Chair: Rance Cleaveland

Synthesizing Distributed Systems (Abstract)

Moshe Y. Vardi , Rice University
Orna Kupferman , Hebrew University
pp. 0389

Permutation Rewriting and Algorithmic Verification (Abstract)

Tayssir Touili , LIAFA, Universit? Paris VII
Ahmed Bouajjani , LIAFA, Universit? Paris VII
Anca Muscholl , LIAFA, Universit? Paris VII
pp. 0399

Temporal Logic Query Checking (Abstract)

Patrice Godefroid , Bell Laboratories, Lucent Technologies
Glenn Bruns , Bell Laboratories, Lucent Technologies
pp. 0409
Session 11 - Chair: Ron van der Meyden

Typechecking XML Views of Relational Databases (Abstract)

Victor Vianu , U.C. San Diego
Tova Milo , Tel Aviv University
Dan Suciu , University of Washington
Noga Alon , Tel Aviv University
Frank Neven , Limburgs Universitair Centrum
pp. 0421

Author Index (PDF)

pp. 0441
113 ms
(Ver 3.1 (10032016))