A. Bergeron, J. Manzoni (Univ. Quebec): Ping-pong interactions in e-mail services

D. Marchignoli, F. Martinelli (Univ. Pisa): Automatic verification of cryptographic protocols through compositional analysis techniques

G. Behrmann, K. Larsen (Aalborg University), H. Andersen, H. Hulgaard, J. Lind-Nielsen (Danish Technical University): Verification of hierarchical state/event systems using reusability and compositionality

V. Rusu, E. Singerman (SRI International, Menlo Park): On proving safety properties by integrating static analysis, theorem proving and abstraction

M. Norrish (Cambridge University): Deterministic expressions in C

A. Poetzsch-Heffter, P. M\"uller (Fernuniversit\"at Hagen): A programming logic for sequential Java

A. Podelski, W. Charatonik and M. M\"uller (Univ. Saarlandes, Saarbr\"ucken): Set-based error diagnosis of concurrent constraint programs

E. Moggi (Univ. Genova), W. Taha, Z. Benaissa, T. Sheard (Oregon Graduate Institute): An idealized MetaML: simpler, and more expressive

J. Knoop, O. R\"uthing, B. Steffen (Univ. Dortmund): Expansion-based removal of semantic partial redundancies )

R. Gupta and R. Bodik (Univ. Pittsburgh): Register pressure sensitive redundancy elimination

D. K\"astner, M. Langenbach (Univ. des Saarlandes, Saarbr\"ucken): Code optimization by integer linear programming

V. Liberatore (Univ. Maryland), M. Farach-Colton, U. Kremer (Rutgers University): Evaluation of algorithms for local register allocation

A. Biere, A. Cimatti, E. Clarke, Y. Zhu (Carnegie-Mellon University): Symbolic model checking without BDDs

P. Abdulla (Uppsala University), A. Annichni, A. Bouajjani (Verimag, Grenoble): Symbolic verification of lossy channel systems: Application to the bounded retransmission protocol

G. Delzanno, A. Podelski (Max-Planck-Institut, Saarbr\"ucken): Model checking in CLP

K. Heljanko (Helsinki Univ. of Technology): Using logic programs with stable model semantics to solve deadlock and reachability problems for 1-safe Petri nets

M. Benedikt (Bell Laboratories), T. Reps (Univ. of Wisconsin), M. Sagiv (Tel Aviv University):A decidable logic for describing linked data structures

F. Nielson, H. Riis Nielson (Aarhus University): Interprocedural control flow analysis

A. Sabelfeld, D. Sands (Chalmers, Gothenburg): A per model of secure information flow in sequential programs

A. King, J. Smaus, P. Hill (Univ. Kent at Canterbury): Quotienting share for dependency analysis

C. Zhang, S. Ryan and G. Gao (Univ. Delaware), R. Govindarajan (Indian Institute of Science, Bangalore): Efficient state-diagram construction methods for software pipelining

G. Rivera, C.-W. Tseng (Univ. Maryland): A comparison of compiler tiling algorithms

L. Rauchwerger (Texas A&M University): Implementation issues of loop-level speculative run-time parallelization

M. Anlauff (GMD Berlin), P. Kutter (ETH Z\"urich), A. Pierantonio (Univ. L'Aquila), tool demo: Generating programming environments from language definitions

18:00