From here you can download a pdf version of the program of ETAPS 2003 main conferences and ETAPS at a Glance.

Monday, April 7:

9.00 - 9.30:

9.30 - 10.30:

FOSSACS invited lecture
Session chair: Andrew Gordon

• Generic Theories and Theories of Genericity
  Samson Abramsky (Oxford University, UK)

10.30 - 11.00:

11.00 - 12.30:

FOSSACS: Probabilistic Models
Session chair: Roberto Gorrieri

• An Intrinsic Characterization of Approximate Probabilistic Bisimilarity
  Franck van Breugel (York University, CDN), Michael Mislove (Tulane University, USA), Joël Ouaknine (Carnegie Mellon University, USA), James Worrell (Tulane University, USA).
• The Converse of a Stochastic Relation
  Ernst-Erich Doberkat (University of Dortmund, D)
• Parameterized Verification by Probabilistic Abstraction
  Tamarah Arons, Amir Pnueli (Weizmann Institute of Science, IL), Lenore Zuck (New York University, USA).

CC: Register Allocation
Session chair: Uwe Assmann

• Combined Code Motion and Register Allocation using the Value State Dependence Graph
  Neil Johnson, Alan Mycroft (University of Cambridge, UK)
• Early Control of Register Pressure for Software Pipelined Loops
  Sid-Ahmed-Ali Touati, Christine Eisenbeis (INRIA Rocquencourt, F)
• Register Allocation by Optimal Graph Coloring
  Christian Andersson (Lund Institute of Technology, S)

TACAS: Bounded Model Checking and SAT-based Methods
Session chair: Moshe Vardi

• Automatic Abstraction without Counterexamples Kenneth McMillan
  Nina Amla (Cadence Design Systems, USA)
• Bounded Model Checking for Past LTL
  Marco Benedetti, Alessandro Cimatti (Istituto per la Ricerca Scientifica e Tecnologica, I)
• Experimental Analysis of Different Techniques for Bounded Model Checking
  Nina Amla, Robert Kurshan, Ken McMillan, Ricardo Medel (Cadence Design Systems & Cadence Berkeley Labs & Stevens Institute of Technology, USA)

12.30 - 14.30:

14.30 - 16.00:

FOSSACS: Process Calculi
Session chair: Uwe Nestmann

• Towards a Behavioural Theory of Access and Mobility Control in Distributed Systems
  Matthew Hennessy, Massimo Merro, Julian Rathke (University of Sussex, UK)
• When Ambients Cannot be Opened
  Iovka Boneva, Jean-Marc Talbot (Laboratoire d'Informatique Fondamentale de Lille, F)
• Genericity and the Pi-Calculus
  Martin Berger, Kohei Honda (Queen Mary, University of London, UK) Nobuko Yoshida (Imperial College, UK)

CC: Language Constructs and their Implementation
Session chair: Oege de Moor

• A Compilation and Optimization Model for Aspect-Oriented Programs
  Hidehiko Masuhara (University of Tokyo, J) Gregor Kiczales (Intentional Software Incorporate and University of British Columbia, CDN) Chris Dutchyn (University of British Columbia, CDN)
• A Pattern Matching Compiler for Multiple Target Languages
  Pierre-Etienne Moreau, Christophe Ringeissen (LORIA-INRIA, F) Marian Vittek (Institut of Informatica Mlynska Dolina, SK)
• A New One-Pass Transformation into Monadic Normal Form
  Olivier Danvy (University of Aarhus, DK)

TACAS: Mu-calculus and Temporal Logics
Session chair: Amir Pnueli

• On the Universal and Existential Fragments of the Mu Calculus
  Thomas A. Henzinger, Orna Kupferman, Rupak Majumdar (University of California, USA & Hebrew University, IL)
• Aborts vs Resets in Linear Temporal Logic
  Roy Armoni, Doron Bustan, Orna Kupferman, Moshe Y. Vardi (Inter Israel Development Center, IL & Rice University, USA & Hebrew University, IL)
• A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems
  Radu Mateescu (INRIA Rhone-Alpes, F)

16.00 - 16.30:

16.30 - 18.30:

FOSSACS: Categorical Models
Session chair: Dusko Pavlovic

• Deriving Bisimulation Congruences: 2-categories vs Precategories
  Vladimiro Sassone (University of Sussex, UK), Pawel Sobocinski (University of Aarhus, DK)
• Abstraction in Reasoning about Higraph-based Systems
  John Power, Konstantinos Tourlas (University of Edinburgh, UK)
• Categories of Containers
  Michael Abbott (Leicester University, UK), Thorsten Altenkirch (Nottingham University, UK), Neil Ghani (Leicester University, UK)

CC: Type Analysis
Session chair: Isabelle Attali

• Run-Time Type Checking for Binary Programs
  Michael Burrows (Microsoft Corporation, USA) Stephen N. Freund (Williams College, USA) Janet L. Wiener (HP Labs, USA)
• Precision in Practice: A Type-Preserving Java Compiler
  Christopher League (Long Island University, USA) Zhong Shao, Valery Trifonov (Yale University, USA)
• Tool demo: The MAGICA Type Inference Engine for MATLAB
  Pramod G. Joisha, Prithviray Banerjee (Northwestern University, USA)

TACAS: Verification of Parameterized Systems
Session chair: Alain Finkel

• Decidability of Invariant Validation for Paramaterized Systems
  Pascal Fontaine, Pascal Gribomont (University of Liege, B)
• Verification and Improvement of the Sliding Window Protocol
  Dmitri Chkliaev, Jozef Hooman, Erik de Vink (Eindhoven University of Technology, NL & University of Nijmegen, NL)
• Simple Representative Instantiations for Multicast Protocols
  Javier Esparza, Monika Maidl (University of Edinburgh, UK)
• Rapid Parameterized Model Checking of Snoopy Cache Coherence Protocols
  Allen Emerson, Vineet Kahlon (University of Texas, USA)

Evening: Reception

Tuesday, April 8:

9.00 - 10.00:

CC invited lecture:
Session chair: Görel Hedin

• Dimensions of Precision in Flow Analysis of OOPLs
  Barbara Ryder (Rutgers University, USA)

10.00 - 10.30:

10.30 - 12.30:

FOSSACS: Syntax and Semantics of Programming Languages
Session chair: Andrew Gordon

• Multi-Level Meta-Reasoning with Higher-Order Abstract Syntax
  Alberto Momigliano, Simon Ambler (University of Leicester, UK)
• A Normalisation Result for Higher-Order Calculi with Explicit Substitutions
  Eduardo Bonelli (Universidad Nacional de La Plata, RA, and Stevens Institute of Technology, USA)
• A Game Semantics of Linearly Used Continuations
  James Laird (University of Sussex, UK)
• A Monadic Multi-stage Metalanguage
  Eugenio Moggi, Sonia Fagorzi (University of Genova, I)

CC: Java
Session chair: Pierluigi San Pietro

• Polyglot: An Extensible Compiler Framework for Java
  Nathaniel Nystrom, Michael R. Clarkson, Andrew C. Myers (Cornell University, USA)
• Scaling Java Points-To Analysis Using Spark
  Ondřej Lhoták, Laurie Hendren (McGill University, CDN)
• Effective Inline-Threaded Interpretation of Java Bytecode Using Preparation Sequences
  Etienne Gagnon, Laurie Hendren (Université du Québec à Montréal and McGill University, CDN)
• Integrating Generations with Advanced Reference Counting Garbage Collectors
  Hezi Azatchi (IBM Haifa, IL), Erez Petrank (Technion, IL)

TACAS: Abstractions and Counter-examples
Session chair: Kim Larsen

• Proof-like Counter-Examples
  Arie Gurfinkel, Marsha Chechik (University of Toronto, CDN)
• Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation
  Marcelo Glusman, Gila Kamhi, Sela Mador-Haim, Ranan Fraer, Moshe Y. Vardi (The Technion, IL & Intel Corporation, IL & Rice University, USA)
• Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement
  Edmund Clarke, Ansgar Fehnker, Zhi Han, Bruce Krogh, Olaf Stursberg, Michael Theobald (Carnegie Mellon University, USA & Universitat Dortmund, D)
• Counter-example Guided Predicate Abstraction of Hybrid Systems
  Rajeev Alur, Thao Dang, Franjo Ivancic (University of Pennsylvania, USA & CNRS, Verimag, F)

12.30 - 14.30:

14.30 - 16.30:

FOSSACS: From Trees to Types
Session chair: Eugenio Moggi

• Counting and Equality Constraints for Multitree Automata
  Denis Lugiez (CNRS and Université de Provence, F)
• Manipulating Trees with Hidden Labels
  Luca Cardelli (Microsoft Research, UK) Philippa Gardner (Imperial College, UK) Giorgio Ghelli (Università di Pisa, I)
• Type Assignment for Intersections and Unions in Call-by-Value Languages
  Joshua Dunfield, Frank Pfenning (Carnegie Mellon University, USA)
• Generalized Iteration and Coiteration for Higher-Order Nested Datatypes
  Andreas Abel (University of Munich, D) Ralph Matthes (Université de Paris VII, F, and University of Munich, D) Tarmo Uustalu (Tallinn Technical University, EST)

CC: Pot Pourri
Session chair: Mark van den Brand

• The Interprocedural Express-lane Transformation
  David Melski (GrammaTech Inc., USA), Thomas Reps (University of Wisconsin, USA)
• Automatic Detection of Uninitialized Variables
  Thi Viet Nga Nguyen, François Irigoin, Corinne Ancourt, Fabien Coelho (École des Mines de Paris, F)
• Generalised Regular Parsers
  Adrian Johnstone, Elizabeth Scott (University of London, UK)
• Rapid and Robust Compiler Construction Using Template-Based Metacompilation
  C. van Reeuwijk (Delft University of Technology, NL)

TACAS: Real-Time and Scheduling
Session chair: Rajeev Alur

• Schedulability Analysis Using Two Clocks
  Elena Fersman, Leonid Mokrushin, Paul Pettersson, Wang Yi (Uppsala University, S)
• On Optimal Scheduling under Uncertainty
  Yasmina Abdeddaim, Eugene Asarin, Oded Maler (VERIMAG, F)
• Static Guard Analysis in Timed Automata Verification
  Gerd Behrmann, Patricia Bouyer, Emmanuel Fleury, Kim G. Larsen (Aalborg University, DK & ENS de Cachan, F)
• Tool demo: Moby/DC - A Tool for Model-Checking Parametric Real-Time Specifications
  Henning Dierks, Josef Tapken (University of Oldenburg, D)
• Tool demo:VERICS: A Tool for Verifying Timed Automata and Estelle Specifications
  Piotr Dembinski, Agata Janowska, Pawel Janowski, Wojciech Penczek, Agata Polrola, Maciej Szreter, Bozena Wozna, Andrzej Zbrzezny (Institute of Comp. Science PAS, PL)

16.30 - 17.00:

17.00 - 18.00:

Microsoft lecture:
Session chair: Pawel Urzyczyn

• Programming language support for data and XML
  Erik Meijer (Microsoft Corporation, USA)

Wednesday, April 9:

9.00 - 10.00:

ETAPS invited lecture:
Session chair: José Luiz Fiadeiro

• The Verifying Compiler: still a Grand Challenge for Computing Research
  Tony Hoare (Microsoft Research, UK)

10.00 - 10.30:

10.30 - 12.30:

FOSSACS: Logic and Verification
Session chair: Witold Charatonik

• Cones and Foci for Protocol Verification Revisited
  Wan Fokkink (CWI and Vrije Universiteit Amsterdam, NL), Jun Pang (CWI, NL)
• Compositional Circular Assume-Guarantee Rules Cannot Be Sound and Complete
  Patrick Maier (Max-Planck-Institut für Informatik, D)
• The Two-Variable Guarded Fragment with Transitive Guards is 2EXPTIME-Hard
  Emanuel Kieronski (University of Wroclaw, PL)
• Verification of Cryptographic Protocols: Tagging Enforces Termination
  Bruno Blanchet (ENS Paris, F, and Max-Planck-Institut für Informatik, D), Andreas Podelski (Max-Planck-Institut für Informatik, D)

CC: Optimization
Session chair: Stefano Crespi Reghizzi

• Address Register Assignment for Reducing Code Size
  M. Kandemir, M. J. Irwin, G. Chen (Pennsylvania State University, USA), J. Ramanujam (Louisiana State University, USA)
• Offset Assignment Showdown: Evaluation of DSP Address Code Optimization Algorithms
  Rainer Leupers (RWTH Aachen, D)
• Integrating High-Level Optimizations in a Production Compiler: Design and Implementation Experience
  Somnath Ghosh, Abhay Kanhere, Rakesh Krishnaiyer, Dattatraya Kulkarni, Wei Li, Chu-Cheow Lim, John Ng (Intel Corporation, USA)
• Improving Data Locality by Chunking
  Cédric Bastoul (Université de Versailles Saint Quentin, F), Paul Feautrier (École Normale Supérieure de Lyon, F)

FASE: Software Components
Session chair: Luigi Lavazza

• An Ontology for Software Component Matching
  Claus Pahl (Dublin City University, IRL)
• A Description Language For Composable Components
  Ioana Sora, Pierre Verbaeten, Yolande Berbers (Katholieke Universiteit Leuven, B)
• A Logic Basis for the Specification of Reconfigurable Component-Based Systems
  Nazareno Aguirre, Tom Maibaum (King's College, London, UK)
• An Overall System Design Approach doing Object-Oriented Modeling to Code-Generation for Embedded Electronic Systems
  Clemens Reichmann (University of Karlsruhe, D), Markus Kühl (Research Center for Information Technology, Karlsruhe, D), Klaus D. Müller-Glaser (University of Karlsruhe, D)

12.30 - 14.30:

14.30 - 15.30:

ETAPS invited lecture:
Session chair: Andrzej Tarlecki

• Computer Security from a Programming Language and Static Analysis Perspective
  Xavier Leroy (INRIA and Trusted Logic, F)

15.45 - 16.45:

TACAS: Security and Cryptography
Session chair: Kurt Jensen

• A New Knowledge Representation Strategy for Cryptographic Protocol Analysis
  Ivan Cibrario Bertolotti, Luca Durante, Riccardo Sisto, Adriano Valenzano (Istituto di Elettronica e di Ingegneria dell'Informazione e delle Telecomunicazioni, I & Politecnico di Torino, I)
• Pattern-based Abstraction for Verifying Secrecy in Protocols
  Liana Bozga, Lakhnech Yassine, Michael Perin (Verimag, F)

FOSSACS: Probabilistic Lossy Channels
Session chair: Igor Walukiewicz

• Verification of Probabilistic Systems with Faulty Communication
  Parosh Aziz Abdulla (Uppsala University, S), Alexander Rabinovich (Tel Aviv University, IL)
• Model Checking Lossy Channels Systems is Probably Decidable
  Nathalie Bertrand, Philippe Schnoebelen (ENS Cachan and CNRS, F)

ESOP: Techniques & Methods
Session chair: Alan Mycroft

• A Tail-Recursive Semantics for Stack Inspections
  John Clements, Matthias Felleisen (Northeastern University, USA)
• Flexible Models for Dynamic Linking
  Sophia Drossopoulou (Imperial College, UK), Giovanni Lagorio (University of Genova, I), Susan Eisenbach (Imperial College, UK)

16.45 - 17.15:

17.15 - 18.45:

FOSSACS: Recursion
Session chair: Igor Walukiewicz

• Ambiguous Classes in the Games Mu-Calculus Hierarchy
  André Arnold, Luigi Santocanale (Université de Bordeaux, F)
• On the Geometry of Inductive Reasoning: Circular and Tree-Shaped Proofs in the Mu-Calculus
  Christoph Sprenger (Swedish Institute of Computer Science, S), Mads Dam (Royal Institute of Technology, S)
• Computability over an Arbitrary Structure. Sequential and Parallel Polynomial Time
  Olivier Bournez, Felipe Cucker, Paulin Jacobé de Naurois, Jean-Yves Marion (LORIA/INRIA, F)

FASE: Mobile Computing
Session chair: Henry Muccini

• Composing Specifications of Event Based Applications?
  Pascal Fenkam, Harald Gall, Mehdi Jazayeri (Technical University of Vienna, A)
• A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems
  Stephan Merz (INRIA Lorraine, F), Martin Wirsing, Julia Zappe (Universität München, D)
• Spatial Security Policies for Mobile Agents in a Sentient Computing Environment
  David Scott, Alastair Beresford, Alan Mycroft (University of Cambridge,UK)

ESOP: Logic Programming
Session chair: Helmut Seidl

• Automated Correction of Functional Logic Programs
  Maria Alpuente (Univ. Politecnica de Valencia, E), Demis Ballis (Università di Udine, I), Francisco Correa (Univ. Eafit, CO), Moreno Falaschi (Università di Udine, I)
• Approximate Pruning in Tabled Logic Programming
  Luis F. Castro, David S. Warren (SUNY at Stony Brook, USA)
• Goal-Independent Suspension Analysis of Logic Programs with Dynamic Scheduling
  Samir Genaim (Ben-Gurion University of the Negev, IL), Andy King (University of Kent at Canterbury, UK)

Evening:

Thursday, April 10:

9.00 - 10.00:

ESOP invited lecture:
Session chair: Pierpaolo Degano

• What Makes a Cryptographic Protocol Secure? The Evolution of Requirements Specification in Formal Cryptographic Protocol Analysis
  Catherine Meadows (Naval Research Laboratory, USA)

10.00 - 10.30:

10.30 - 12.30:

TACAS: Modules and Compositional Verification
Session chair: Bernhard Steffen

• Compositional Analysis for Verification of Parameterized Systems
  Samik Basu, C.R. Ramakrishnan (SUNY at Stony Brook, USA)
• Learning Assumptions for Compositional Verification
  Jamieson M. Cobleigh, Dimitra Giannakopoulou, Corina S. Pasareanu (University of Massachusets, USA & NASA Ames Research Center, USA)
• Automated Module Composition
  Stavros Tripakis (VERIMAG, F)
• Modular Strategies for Recursive Game Graphs
  Rajeev Alur, Salvatore La Torre, P. Madhusudan (University of Pennsylvania, USA & University of Salerno, I)

FASE: Aspect and Object Oriented Programming
Session chair: Luciano Baresi

• Towards UML-based Formal Specifications of Component Based Real-Time Software
  Vieri Del Bianco, Luigi Lavazza (Politecnico di Milano and CEFRIEL, I), Marco Mauri, Giuseppe Occorso (Politecnico di Milano, I)
• Modelling Recursive Calls with UML State Diagrams
  Jennifer Tenzer, Perdita Stevens (University of Edinburgh, UK)
• Pipa: A Behavioral Specification Language for AspectJ
  Jianjun Zhao, Martin Rinard (Massachusetts Institute of Technology, USA)
• Tool demo: PacoSuite & JAsCo: A Visual Component Composition Environment with Advanced Aspect Separation Features
  Wim Vanderperren, Davy Suvée, Bart Wydaeghe (Vrije Universiteit Brussel, B)

ESOP: Security 1
Session chair: Joshua Guttman

• Security Properties: Two Agents Are Sufficient
  Hubert Comon-Lundh and Veronique Cortier (LSV, ENS Cachan and CNRS, F)
• A Simple Language for Real-time Cryptographic Protocol Analysis
  Roberto Gorrieri, Enrico Locatelli (University of Bologna, I), Fabio Martinelli (IIT-CNR, I)
• Rule Formats for Non Interference
  Simone Tini (Universita dell'Insubria, I)
• On the Secure Implementation of Security Protocols
  Pablo Giambiagi, Mads Dam (Swedish Institute of Computer Science, S)

12.30 - 13.30:

EASST General Assembly

12.30 - 14.30:

14.30 - 15.30:

TACAS invited lecture
Session chair: John Hatcliff

• What Are We Trying to Prove? Lessons from our Experiences with Proof-Carrying Code
  Peter Lee (Carnegie Mellon University, USA)

15.45 - 16.45:

TACAS: Symbolic State Spaces and Decision Diagrams
Session chair: Jan Friso Groote

• Saturation Unbound
  Gianfranco Ciardo, Robert Marmorstein, Radu Siminiceanu (College of William and Mary, USA)
• Construction of Efficient BDDs for Bounded Arithmetic Constraints
  Constantinos Bartzis, Tevfik Bultan (University of California, USA)

FASE: Distributed and Web Applications
Session chair: Hartmut Ehring

• Model-Based Development of Web Applications Using Graphical Reaction Rules
  Reiko Heckel, Marc Lohmann (University of Paderborn, D)
• Modular Analysis of Dataflow Process Networks
  Yan Jin, Robert Esser, Charles Lakos (Adelaide University, USA), Jörn W. Janneck (University of California at Berkeley, USA)

ESOP: Security 2
Session chair: Catherine Meadows

• Handling Encryption in an Analysis for Secure Information Flow
  Peeter Laud (Tartu University and Cybernetica AS, EST)
• Using Controller Synthesis to Build Property-Enforcing Layers
  Karine Altisen (VERIMAG/INPG, F), Aurelie Clodic (LAAS/CNRS, F), Florence Maraninchi (VERIMAG/INPG, F), Eric Rutten (INRIA Rhone-Alpes, F)

16.45 - 17.15:

17.15 - 18.45:

TACAS: Performance and Mobility
Session chair: Joost-Pieter Katoen

• Modeling and Analysis of Power-Aware Systems
  Kyriakos Christou, Insup Lee, Anna Philippou, Oleg Sokolsky (University of Pennsylvania, USA & University of Cyprus, CY)
• Tool demo: A Set of Performance and Dependability Analysis Components for CADP
  Holger Hermanns, Christophe Joubert (INRIA Rhone-Alpes, Montbonnot Saint-Martin, F)
• Tool demo: The Integrated CWB-NC/PIOATool for Functional Verification and Performance Analysis of Concurrent Systems
  Dezhuang Zhang, Rance Cleaveland, Eugene Stark (State University of New York at Stony Brook, USA)
• Tool demo: BANANA: A Tool for Boundary Ambients Nesting ANAlysis
  Chiara Braghin, Agostino Cortesi, Stefano Filippone, Riccardo Focardi, Flaminia L. Luccio, Carla Piazza (University de Venezia, I)

FASE: Sofware Measurements
Session chair: Jan Madey

• Foundations of a Weak Measurement-Theoretic Approach to Software Measurement
  Sandro Morasca (Università degli Studi dell'Insubria, I)
• An Information-Based View of Representational Coupling in Object-Oriented Systems
  Pierre Kelsen (Luxembourg University of Applied Sciences, L)

ESOP: Program Correctness
Session chair: David Schmidt

• Automatic Software Model Checking using CLP
  Cormac Flanagan (Systems Research Center, Hewlett Packard, USA)
• Verifying Temporal Heap Properties Specified via Evolution Logic
  Eran Yahav (Tel Aviv University, IL), Thomas Reps (University of Wisconsin, USA), Mooly Sagiv (Tel Aviv University, IL), Reinhard Wilhelm (Universitat des Saarlandes, D)
• Correctness of Data Representations Involving Heap Data Structures
  Uday Reddy (University of Birmingham, UK), Hongseok Yang (Korean Advanced Institute of Science and Technology, Korea)

Friday, April 11:

9.00 - 10.00:

FASE invited lecture
Session chair: Mauro Pezzč

• Symbiosis of Static Analysis and Program Testing
  Michal Young (Oregon University, USA)

10.00 - 10.30:

10.30 - 12.30:

TACAS: State Space Reductions
Session chair: Hubert Garavel

• State Class Constructions for Branching Analysis of Time Petri Nets
  Bernard Berthomieu, Francois Vernadat (LAAS-CNRS, F)
• Branching Processes of High-Level Petri Nets
  Victor Khomenko, Maciej Koutny (University of Newcastle, UK)
• Using Petri Net Invariants in State Space Construction
  Karsten Schmidt (Humboldt-Universitat zu Berlin, D)
• Optimistic Synchronization-Based State-Space Reduction
  Scott Stoller, Ernie Cohen (State University of New York at Stony Brook, USA & Cambridge, UK)

FASE: Formal Verification
Session chair: Reiko Heckel

• A Temporal Approach to Specification and Verification of Pointer Data-Structures
  Marcin Kubica (Warsaw University, PL)
• A Program Logic for Handling JAVACARD's Transaction Mechanism
  Bernhard Beckert (Universität Karlsruhe, D), Wojciech Mostowski (Chalmers University of Technology, S)
• Monad Independent Computational Reasoning in HasCasl
  Lutz Schröder, Till Mossakowski (University of Bremen, D)
• Visual Specifications of Policies and their Verification
  Manuel Koch (Frei Universität Berlin, D), Francesco Parisi-Presicce (Università di Roma, I, and George Mason University, USA)

ESOP: Types
Session chair: Mariangiola Dezani Ciancaglini

• Modeling Web Interactions
  Paul Graunke (Northeastern University, USA), Robert Bruce Findler (University of Chicago, USA), Shriram Krishnamurthi (Brown University, USA), Matthias Felleisen (Northeastern University, USA)
• Type Inference for a Distributed Pi-Calculus
  Cedric Lhoussaine (University of Sussex, UK)
• Type-Safe Update Programming
  Martin Erwig, Deling Ren (Oregon State University, USA)
• Type Error Slicing in Implicitly Typed, Higher-Order Languages
  Christian Haack, J. B. Wells (Heriot-Watt University, UK)

12.30 - 14.30:

14.30 - 16.00:

TACAS: Constraint-Solving and Decision Procedures
Session chair: Andreas Podelski

• Checking Properties of Heap-Manipulating Procedures with a Constraint Solver
  Mandana Vaziri, Daniel Jackson (Massachusetts Institute of Technology, USA)
• Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic
  Sergey Berezin, Vijay Ganesh, David L. Dill (Stanford University, USA)
• Strategies for Combining Decision Procedures
  Sylvain Conchon, Sava Krstic (Oregon Health & Sciences University, USA)

FASE: Model Checking
Session chair: Chairç Giovanni Denaro

• Automatic Model Driven Animation of SCR Specifications
  Angelo Gargantini, Elvinia Riccobene (Università di Catania, I)
• Probe Mechanism for Object-Oriented Software Testing
  Anita Goel, (University of Delhi, IND), S. C. Gupta (National Informatics Center, IND), S. K. Wasan (Jamia Millia Islamia, IND)
• Model Checking Software via Abstraction of Loop Transitions
  Natasha Sharygina (Carnegie Mellon University, USA), James C. Browne (The University of Texas, USA)

ESOP: Techniques & Applications
Session chair: Perdita Stevens

• Core Formal Molecular Biology
  Vincent Danos (CNRS University of Paris 7, F), Cosimo Laneve (University of Bologna, I)
• Requirements on the Execution of Kahn Process Networks
  Marc Geilen, Twan Basten (Eindhoven University of Technology, NL)
• Tagging, Encoding, and Jones Optimality
  Olivier Danvy (University of Aarhus, DK), Pablo E. Martínez López (UNLP, AR)

16.00 - 16.30:

16.30 - 18.30:

TACAS: Testing and Verification
Session chair: Alessandro Fantechi

• Generalized Symbolic Execution for Model Checking and Testing
  Sarfraz Khurshid, Corina Pasareanu, and Willem Visser (Massachusets Institute of Technology, USA & NASA Ames Research Center, USA)
• Code-based Test Generation for Validation of Functional Processor Descriptions
  Fabrice Barray, Philippe Codognet, Daniel Diaz, Henri Michel (ST-Microelectronics, F & University of Paris, F)
• Tool demo: State Space Visualization
  Jan Friso Groote, Frank van Ham (Technische Universiteit Eindhoven, NL)
• Tool demo: Automatic Test Generation with AGATHA
  Céline Bigot, Alain Faivre, Jean-Pierre Gallois, Arnaud Lapitre, David Lugato, Jean-Yves Pierron, Nicolas Rapin (CEA - SACLAY, DRT/LIST/DTSI/SLA, Gif-sur-Yvette, F)
• Tool demo: LTSA-MSC: Tool Support for Behaviour Model Elaboration Using Implied Scenarios
  Sebastian Uchitel, Robert Chatley, Jeff Kramer, Jeff Magee (Imperial College, UK)

FASE: Model Integrations and Extensions
Session chair: José Luiz Fiadeiro

• Integration of Formal Data Types within State Diagrams
  Christian Attiogbe, Pascal Poizat, Gwen Salaiin (Universite de Nantes, F)
• Xere: Towards a Natural Interoperability between XML and ER Diagrams
  G. Della Penna, A. Di Marco, B. Intrigila, I. Melatti, A. Pierantonio (Universita' degli Studi dell'Aquila, I)
• Detecting Implied Scenarios Analyzing Non-Local Branching Choices
  Henry Muccini (Università degli Studi dell'Aquila, I)
• Capturing Overlapping, Triggered and Preemptive Collaborations Using MSCs
  Ingolf H. Krüger (University of California, San Diego, USA)

ESOP: Reasoning
Session chair: Cedric Fournet

• The Rely-Guarantee Method in Isabelle/HOL
  Leonor Prensa Nieto (INRIA Sophia Antipolis, F)
• Building Certified Libraries for PCC: Dynamic Storage Allocation
  Dachuan Yu, Nadeem Hamid, Zhong Shao (Yale University, USA)
• Finite Differencing of Logical Formulas for Static Analysis
  Thomas Reps (University of Wisconsin, USA), Mooly Sagiv (Tel-Aviv University, IL), Alexey Loginov (University of Wisconsin, USA)
• Register Allocation by Proof Transformation
  Atsushi Ohori (Japan Advanced Institute of Science and Technology, J)

18.30 - 18.45: