Programme of Main Conferences at ETAPS 2007


Programme of Monday, March 26

09:00 - 10:30 SESSION 1 (Monday)

Welcome
FOSSACS - Invited Talk (Chair: Helmut Seidl, room: Enabler-Wipro)
Formal foundations for Aspects
Radha Jagadeesan (DePaul University, USA)

10:30 - 11:00 Coffee

11:00 - 12:30 SESSION 2 (Monday)

CC - Architecture (Chair: Martin Odersky, room: Cisco)
New Algorithms for SIMD Alignment
Liza Fireman (Technion), Erez Petrank (Microsoft Research), Ayal Zaks (IBM Haifa Research Laboratory)
Preprocessing Strategy for Effective Modulo Scheduling on Multi-Issue Digital Signal Processors
Doosan Cho (Seoul National University), Ravi Ayyagari (Boise State University), Gang-Ryung Uh (Bosie State University), Yunheung Paek (Seoul National University)
Compiler Directed Power Optimization for Partitioned Memory Architectures
K. Shyam, R. Govindarajan (Indian Institute of Science)
FOSSACS - Games and Mu Calculus (Chair: Helmut Seidl, room: Multicert)
Optimal Strategy Synthesis in Stochastic Müller Games
Krishnendu Chatterjee (Univ. of California, Berkeley)
Generalized Parity Games
Nir Piterman (EPFL Switzerland), Krishnendu Chatterjee (Univ. of Califonria, Berkeley), Thomas A. Henzinger (EPFL Switzerland)
Enriched mu-Calculi Module Checking
Aniello Murano (Univ. di Napoli), Alessandro Ferrante (Univ. di Salerno)
TACAS - Software Verification (Chair: Natasha Sharygina, room: Enabler-Wipro)
Shape Analysis by Graph Decomposition
Roman Manevich (Tel Aviv University), Joshua Berdine, Byron Cook (Microsoft Reasearch Cambridge), Ganesan Ramalingam (Microsoft Research India), and Mooly Sagiv (Tel Aviv University)
A reachability predicate for analyzing low-level software
Shaunak Chatterjee (Indian Institute of Technology at Kharagpur), Shuvendu K. Lahiri, Shaz Qadeer (Microsoft Research), and Zvonimir Rakamaric (University of British Columbia)
Generating Representation Invariants of Structurally Complex Data
Muhammad Zubair Malik, Aman Pervaiz, and Sarfraz Khurshid (University of Texas at Austin)

12:30 - 14:30 Lunch

14:30 - 16:30 SESSION 3 (Monday)

CC - Garbage Collection and Program Analysis (Chair: Reinhard Wilhelm, room: Cisco)
Using Prefetching to Improve Reference-Counting Garbage Collectors
Harel Paz (IBM Haifa Research Laboratory), Erez Petrank (Microsoft Research)
Accurate Garbage Collection in Uncooperative Environments with Lazy Pointer Stacks
Jason Baker, Antonio Cunei, Filip Pizlo, Jan Vitek (Purdue University)
Correcting the Dynamic Call Graph Using Control-Flow Constraints
Byeongcheol Lee, Kevin Resnick, Michael D. Bond, Kathryn S. McKinley (University of Texas at Austin)
Obfuscating Java: the Most Pain for the Least Gain
Michael Batchelder, Laurie Hendren (McGill University)
FOSSACS - Logic (Chair: Hubert Comon, room: Multicert)
The Complexity of Generalized Satisfiability for Linear Temporal Logic
Thomas Schneider (Univ. Jena), Henning Schnoor (Univ. Hannover), Ilka Schnoor (Univ. Hannover), Michael Bauland (Univ. Hannover), Heribert Vollmer (Univ. Hannover)
PDL with intersection and converse is 2EXP-complete
Markus Lohrey (Univ. Stuttgart), Carsten Lutz (TU Dresden), Stefan Göller (Univ. Stuttgart)
On the Expressiveness and Complexity of ATL
Nicolas Markey (ENS Cachan), Ghassan Oreiby (ENS Cachan), Francois Laroussinie (ENS Cachan)
Formalising the pi-calculus using Nominal Logic
Jesper Bengtson (Uppsala Univ.), Joachim Parrow (Uppsala Univ.)
TACAS - Probabilistic Model Checking and Markov Chains (Chair: Holger Hermanns, room: Enabler-Wipro)
Multi-Objective Model Checking of Markov Decision Processes
Kousha Etessami (University of Edinburgh), Marta Kwiatkowska (Birmingham University), Moshe Y. Vardi (Rice University), and Mihalis Yannakakis (Columbia University)
PReMo: an analyzer for Probabilistic Recursive Models
Dominik Wojtczak and Kousha Etessami (University of Edinburgh)
Counterexamples in Probabilistic Model Checking
Tingting Han and Joost-Pieter Katoen (RWTH Aachen and University of Twente)
Bisimulation minimisation mostly speeds up probabilistic model checking
Joost-Pieter Katoen (RWTH Aachen and University of Twente), Tim Kemna (University of Twente), Ivan Zapreev (RWTH Aachen and University of Twente), and David N. Jansen (University of Twente)

16:30 - 17:00 Coffee

17:00 - 18:30 SESSION 4 (Monday)

CC - Register Allocation (Chair: Ganesan Ramalingam, room: Cisco)
A Fast Cutting-Plane Algorithm for Optimal Coalescing
Daniel Grund (Saarland University), Sebastian Hack (University of Karlsruhe)
Register Allocation and Optimal Spill code Scheduling in Software Pipelined Loops using 0-1 Integer Linear Programming Formulation
Santosh G. Nagarakatte, R. Govindarajan (Indian Institute of Science)
Extended Linear Scan: an Alternate Foundation for Global Register Allocation
Vivek Sarkar (IBM T.J. Watson Research Center), Rajkishore Barik (IBM India Research Laboratory)
FOSSACS - Formal Languages and Complexity (Chair: Igor Walukiewicz, room: Multicert)
Symbolic Reachability Analysis for Higher-Order Pushdown Systems
Matthew Hague (Oxford Univ.), Luke Ong (Oxford Univ.)
Complexity Results on Balanced Context-Free Languages
Akihiko Tozawa (IBM Research, Tokyo), Yasuhiko Minamide (Univ. of Tsukuba)
An Effective Algorithm for The Membership Problem for Extended Regular Expressions
Grigore Rosu (Univ. of Illinois, Urbana)
TACAS - Static Analysis (Chair: Tiziana Margaria, room: Enabler-Wipro)
Causal Concurrent Dataflow Analysis for Concurrent Programs
Azadeh Farzan and P. Madhusudan (University of Illinois at Urbana-Champaign)
Type-dependency Analysis and Program Transformation for Symbolic Execution
Saswat Anand, Alessandro Orso, and Mary Jean Harrold (Georgia Institute of Technology)
JPF--SE: A Symbolic Execution Extension to Java PathFinder
Saswat Anand (Georgia Institute of Technology), Corina S. Pasareanu, and Willem Visser (NASA Ames Research Center)

19:00 SOCIAL EVENT (Monday)

Welcome Reception (free admittance)
Largo do Paço (University Rectorate Building)
The Etaps Organization invites all ETAPS participants to the welcome reception

Programme of Tuesday, March 27

09:00 - 10:00 SESSION 1 (Tuesday)

CC - Invited Talk (Chair: Shriram Krishnamurthi, room: Enabler-Wipro)
On the Convergence of Program Refactoring, Program Synthesis, and Model Driven Development
Don Batory (U. Austin, USA)

10:00 - 10:30 Coffee

10:30 - 12:30 SESSION 2 (Tuesday)

CC - Program Analysis (Chair: Shriram Krishnamurthi, room: Cisco)
A Practical Escape and Effect Analysis for Building Lightweight Method Summaries
Sigmund Cherem, Radu Rugina (Cornell University)
Layout Transformations for Heap Objects Using Static Access Patterns
Jinseong Jeon, Keoncheol Shin, Hwansoo Han (Korea Advanced Institute of Science and Technology)
A New Elimination-Based Data Flow Analysis Framework
Bernhard Scholz (University of Sydney), Johann Blieberger (Technische Universit\"at Wien)
A declarative framework for analysis and optimization components
Henry Falconer, Paul H. J. Kelly, David M. Ingram, Michael R. Mellor, Tony Field, Olav Beckmann (Imperial College)
FOSSACS - Process Calculi (Chair: Pierpaolo Degano, room: Multicert)
A Distribution Law for CCS and a New Congruence Result for the Pi-calculus
Daniel Hirschkoff (ENS Lyon), Damien Pous (ENS Lyon)
Semantic barbs and biorthogonality
Pawel Sobocinski (Univ. of Cambridge), Vladimiro Sassone (Univ. of Southampton), Julian Rathke (Univ. of Sussex)
Logical Characterizations of Bisimulations for Discrete Probabilistic Systems
Augusto Parma (Univ. di Verona), Roberto Segala (Univ. di Verona)
Approximating a Behavioural Pseudometric without Discount for Probabilistic Systems
Franck van Breugel (York Univ.), James Worrell (Oxford Univ.), Babita Sharma (York Univ.)
TACAS - Markov Chains and Real-Time Systems (Chair: Joost-Pieter Katoen, room: Enabler-Wipro)
A Symbolic Algorithm for Optimal Markov Chain Lumping
Salem Derisavi (Carleton University at Ottawa)
Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations
Lijun Zhang, Holger Hermanns (Saarland University), Friedrich Eisenbrand (University of Paderborn), and David N. Jansen(University of Twente)
Model Checking Probabilistic Timed Automata with One or Two Clocks
Marcin Jurdzinski (University of Warwick), Francois Laroussinie (ENS Cachan), and Jeremy Sproston (Universita di Torino)
Adaptor synthesis for real-time components
Massimo Tivoli (University of L'Aquila), Pascal Fradet, Alain Girault, Gregor Goessler (INRIA Rhone-Alpes)

12:30 - 14:30 Lunch

14:30 - 16:30 SESSION 3 (Tuesday)

FOSSACS - Verification and Program Analysis (Chair: Cristiano Calcagno, room: Enabler-Wipro)
Logical Reasoning for Higher-Order Functions with Local State
Nobuko Yoshida (Imperial College London), Kohei Honda (Queen Mary), and Martin Berger (Imperial College London)
Types and Effects for Resource Usage Analysis
Massimo Bartoletti (Univ. di Pisa), Gian Luigi Ferrari (Univ. di Pisa), Pierpaolo Degano (Univ. di Pisa), Roberto Zunino (Univ. di Pisa)
Relational Parametricity and Separation Logic
Hongseok Yang (Univ. of London), Lars Birkedal (IT Univ. of Copenhagen)
Polynomial Constraints for Sets with Cardinality Bounds
Bruno Marnette (ENS Cachan), Martin Rinard (MIT, Cambridge, USA), Viktor Kuncak (MIT, Cambridge, USA)
TACAS (I) - Timed Automata and Duration Calculus (Chair: Joel Ouaknine, room: Cisco)
Deciding an Interval Logic with Accumulated Durations
Martin Fraenzle (Universitat Oldenburg) and Michael R. Hansen (Technical University of Denmark)
From Time Petri Nets to Timed Automata: an Untimed Approach
Davide D'Aprile, Susanna Donatelli (Universita di Torino), Arnaud Sangnier (LSV-ENS Cachan), and Jeremy Sproston (Universita di Torino)
Complexity in Simplicity: Flexible Agent-based State Space Exploration
Jacob Illum Rasmussen, Gerd Behrmann, and Kim G. Larsen (Aalborg University)
On Sampling Abstraction of Continuous Time Logic with Durations
Paritosh K. Pandya (Tata Institute of Fundamental Research), Shankara Narayanan Krishna, and Kuntal Loya (Indian Institute of Technology at Bombay)
TACAS (II) - Assume-Guarantee Reasoning (Chair: Moshe Vardi, room: Multicert)
Assume Guarantee Synthesis
Krishnendu Chatterjee (University of California, Berkeley) and Thomas A. Henzinger (EPFL)
Optimized L* for Assume-Guarantee Reasoning
Sagar Chaki (Software Engineering Institute) and Ofer Strichman (The Technion, Haifa)
Refining Interface Alphabets for Compositional Verification
Mihaela Gheorghiu (University of Toronto), Dimitra Giannakopoulou, and Corina S. Pasareanu NASA Ames Research Center)
MAVEN: Modular Aspect Verification
Max Goldman and Shmuel Katz (The Technion, Haifa)

16:30 - 17:00 Coffee

17:00 - 18:30 SESSION 4 (Tuesday)

FASE - Evolution and Agents (Chair: Matt Dwyer, room: Unicre)
EQ-Mine: Predicting Short-Term Defects for Software Evolution
Jacek Ratzinger (Vienna University of Technology, Austria), Martin Pinzger (University of Zurich, Switzerland), and Harald C. Gall (University of Zurich, Switzerland)
An Approach to Software Evolution Based on Semantic Change
Romain Robbes (University of Lugano, Switzerland), Michele Lanza (University of Lugano, Switzerland), and Mircea Lungu (University of Lugano, Switzerland)
A Simulation-Oriented Formalization for a Psycholgical Theory
Paulo Salem da Silva (University of São Paulo, Brazil), Ana C. V. de Melo (University of São Paulo, Brazil)
FOSSACS - Calculi (Chair: Antoine Mine, room: Multicert)
The Rewriting Calculus as a Combinatory Reduction System
Clara Bertolissi (Univ. de Provence), Claude Kirchner (INRIA/LORIA, Nancy)
Iterator Types
Ian Mackie (King's College, London), Sandra Alves (Univ. of Porto), Maribel Fernandez (King's College, London), Mario Florido (Univ. of Porto)
On the Stability by Union of Reducibiliy Candidates
Colin Riba (INPL/LORIA, Nancy)
TACAS - Biological Systems (Chair: Radha Jagadeesan, room: Enabler-Wipro)
Model Checking Liveness Properties of Genetic Regulatory Networks
Gregory Batt and Calin Belta (Boston University), and Ron Weiss (Princeton University)
Checking Pedigree Consistency with SAT
Panagiotis Manolios, Marc Galceran Oms, and Sergi Oliva Valls (Georgia Institute of Technology, Atlanta)
Don't Care Modeling: A logical framework for developing predictive system models
Hillel Kugler (New York University), Amir Pnueli (New York University and the Weizmann Institute of Science), Michael Stern (Yale University), and E. Jane Albert Hubbard (New York University)

19:00 SOCIAL EVENT (Tuesday)

10th Anniversary Celebration (free admittance)
Theatro Circo
Cocktail/Buffet
Tales of ETAPS past (room: Enabler-Wipro)
Anniversary Cake + Port Wine + Fado Concert

Programme of Wednesday, March 28

09:00 - 10:10 SESSION 1 (Wednesday)

Unifying Invited Talk (Chair: Perdita Stevens, room: Enabler-Wipro)
There and Back Again: Lessons Learned on the Way to the Market
Rance Cleaveland (University of Maryland/Fraunhofer USA Center for Experimental Software Engineering and Reactive Systems Inc., USA)

10:10 - 10:30 Coffee

10:30 - 12:30 SESSION 2 (Wednesday)

ESOP - Models and Languages for Web Services (Chair: Matthew Hennessy, room: Multicert)
Structured Communication-Centred Programming for Web Services
Marco Carbone (Imperial College London), Kohei Honda (Queen Mary, University of London) and Nobuko Yoshida (Imperial College London).
CC-Pi: A Constraint-Based Language for Specifying Service Level Agreements
Maria Grazia Buscemi (IMT Lucca ) and Ugo Montanari (University of Pisa).
A Calculus for Orchestration of Web Services
Alessandro Lapadula (University of Florence), Rosario Pugliese (University of Florence) and Francesco Tiezzi (University of Florence).
A Concurrent Calculus with Atomic Transactions
Lucia Acciai (Laboratoire d'Informatique Fondamentale, Marseille), Silvano Dal Zilio (Laboratoire d'Informatique Fondamentale, Marseille) and Michele Boreale (University of Florence).
FASE - Model Driven Development (Chair: Maura Cerioli, room: Unicre)
Integrating performance and reliability analysis in a Non-Functional MDA framework
Vittorio Cortellessa (Universita degli Studi di L'Aquila, Italy) Antinisca Di Marco (Universita degli Studi di L'Aquila, Italy), and Paola Inverardi (Universita degli Studi di L'Aquila, Italy)
Information Preserving Bidirectional Model Transformations
Hartmut Ehrig (Technical University Berlin, Germany), Karsten Ehrig (University of Leicester, U.K.), Claudia Ermel (Technical University Berlin, Germany), Frank Hermann (Technical University Berlin, Germany), Gabriele Taentzer (Technical University Berlin, Germany)
Activity-Driven Synthesis of State Machines
Rolf Hennicker (Ludwig-Maximilians-Universitat Munchen,Germany), Alexander Knapp (Ludwig-Maximilians-Universitat Munchen, Germany)
Flexible and Extensible Notations for Modeling
Jimin Gao (University of Minnesota, USA), Mats Heimdahl (University of Minnesota, USA), Eric Van Wyk (University of Minnesota, USA)
FOSSACS - Automata (Chair: Markus Mueller-Olm, room: Cisco)
Tree Automata with Memory, Visibility and Structural Constraints
Hubert Comon (ENS Cachan), Florent Jacquemard (INRIA/ENS Cachan), Nicolas Perrin (ENS Lyon)
Model-Checking One-Clock Priced Timed Automata
Patricia Bouyer (ENS Cachan), Nicolas Markey (ENS Cachan), Kim G. Larsen (Aalborg Univ.)
Sampled Universality of Timed Automata
Pavel Krcal (Uppsala Univ.), Wang Yi (Uppsala Univ.), Parosh Abdulla (Uppsala Univ.)
A Lower Bound on Web Services Composition
Anca Muscholl (LABRI, Bordeaux), Igor Walukiewiczi (LABRI, Bordeaux)
TACAS - Abstraction Refinement (Chair: Shmuel Katz, room: Enabler-Wipro)
Deciding Bit-Vector Arithmetic with Abstraction
Randal E. Bryant (Carnegie Mellon University), Daniel Kroening (ETH Zuerich), Joel Ouaknine (Oxford University), Sanjit A. Seshia (University of California, Berkeley), Ofer Strichman (The Technion, Haifa), and Bryan Brady (University of California, Berkeley)
Abstraction Refinement of Linear Programs with Arrays
Alessandro Armando (Universita di Genova), Massimo Benerecetti (Universita di Napoli), and Jacopo Mantovani (Universita di Genova)
Property-Driven Partitioning for Abstraction Refinement
Roberto Sebastiani (Universita di Trento), Stefano Tonetta (University of Lugano), and Moshe Y. Vardi (Rice University)
Combining Abstraction Refinement and SAT-based Model Checking
Nina Amla and Kenneth McMillan (Cadence Design Systems)

12:30 - 14:30 Lunch

14:30 - 15:40 SESSION 3A (Wednesday)

TACAS - Invited Talk (Chair: Rance Cleaveland, room: Enabler-Wipro)
Verifying object-oriented software: lessons and challenges
K. Rustan M. Leino (Microsoft Research, Redmond, USA)

15:40 - 15:50 Break

15:50 - 16:50 SESSION 3B (Wednesday)

ESOP - Verification (Chair: Pierpaolo Degano, room: Multicert)
Modal I/O Automata for Interface and Product Line Theories
Kim G. Larsen (Aalborg University), Ulrik Nyman (Aalborg University) and Andrzej Wasowski (IT University of Copenhagen)
Using history invariants to verify observers
Rustan Leino (Microsoft Research) and Wolfram Schulte (Microsoft Research)
ESOP - Term Rewriting (Chair: Don Sannella, room: Unicre)
On the implementation of construction functions for non-free concrete data types
Frederic Blanqui (INRIA), Therese Hardin (Universite Paris 6) and Pierre Weis (INRIA)
Anti-Pattern Matching
Claude Kirchner (INRIA-LORIA Nancy), Radu Kopetz (INRIA-LORIA Nancy) and Pierre-Etienne Moreau (INRIA-LORIA Nancy)
FASE - Tool Demonstrations (Chair: José Nuno Oliveira, room: Cisco)
Declared Type Generalization Checker: An Eclipse Plug-In for Programming with More General Types
Markus Bach (University of Hagen, Germany)
Florian Forster (University of Hagen, Germany)
Friedrich Steimann (University of Hagen, Germany)
S2A: A Compiler for Multi-Modal UML Sequence Diagrams
David Harel (The Weizmann Institute of Science, Israel), Asaf Kleinbort (The Weizmann Institute of Science, Israel), Shahar Maoz (The Weizmann Institute of Science, Israel)
TACAS - Message Sequence Charts (Chair: Nina Amla, room: Enabler-Wipro)
Detecting Races in Ensembles of Message Sequence Charts
Edith Elkind (University of Liverpool), Blaise Genest (CNRS/IRISA), and Doron Peled (Bar Ilan University)
Replaying Play in and Play out: Synthesis of Design Models from Scenarios by Learning
Benedikt Bollig (LSV CNRS Cachan), Joost-Pieter Katoen, Carsten Kern (RWTH Aachen University), and Martin Leucker (TU Munich)

16:50 - 17:15 Coffee

17:15 - 18:45 SESSION 4 (Wednesday)

ESOP - Language Based Security (Chair: Joshua Guttman, room: Multicert)
A Certified Lightweight Non-Interference Java Bytecode Verifier
Gilles Barthe (INRIA Sophia Antipolis), David Pichardie (INRIA/IRISA) and Tamara Rezk (INRIA Sophia Antipolis)
Controlling the What and Where of Declassification in Language-Based Security
Heiko Mantel (RWTH Aachen University) and Alexander Reinhard (RWTH Aachen University)
Cost Analysis of Java Bytecode
Elvira Albert (Complutense University of Madrid), Puri Arenas (Complutense University of Madrid), Samir Genaim (Technical University of Madrid), German Puebla (Technical University of Madrid) and Damiano Zanardini (Technical University of Madrid)
ESOP - Logics and Correctness Proofs (Chair: Walid Taha, room: Unicre)
On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning
Xinyu Feng (Yale University), Rodrigo Ferreira (Yale University) and Zhong Shao (Yale University)
Abstract Predicates and Mutable ADTs in Hoare Type Theory
Aleksandar Nanevski (Harvard University), Amal Ahmed (Toyota Technological Institute, Chicago), Greg Morrisett (Harvard University) and Lars Birkedal (IT University, Copenhagen)
A Proof-producing Compiler for a Subset of Higher Order Logic
Guodong Li (University of Utah) and Konrad Slind (University of Utah)
FASE - Distributed Systems (Chair: Holger Giese, room: Cisco)
Scenario-Driven Dynamic Analysis of Distributed Architectures
George Edwards (University of Southern California, USA), Sam Malek (University of Southern California, USA), Nenad Medvidovic (University of Southern California, USA)
Enforcing Architecture and Deployment Constraints of Distributed Component-based Software
Chouki Tibermacine (University of South Brittany, France), Didier Hoareau (University of South Brittany, France), Reda Kadri (Alkante/University of South Brittany, France)
A Family of Distributed Deadlock Avoidance Protocols and their Reachable State Spaces
César Sanchez (Stanford University, USA), Henny B. Sipma (Stanford University, USA), Zohar Manna (Stanford University, USA)
TACAS - Automata-Based Model Checking (Chair: Daniel Kroening, room: Enabler-Wipro)
Improved algorithms for the automata based approach to model-checking
Laurent Doyen (EPFL) and Jean-Francois Raskin (Universitat Libre de Bruxelles)
GOAL: A Graphical Tool for Manipulating Buechi Automata and Temporal Formulae
Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Kang-Nien Wu, and Wen-Chin Chan (National Taiwan University)
Faster Algorithms for Finitary Games
Florian Horn (LIAFA, Universite Paris 7)

19:00 SOCIAL EVENT (Wednesday)

Conference Banquet (tickets needed)
Paço dos Duques, Guimarães
Shuttle departure from Theatro Circo

Programme of Thursday, March 29

09:00 - 10:00 SESSION 1 (Thursday)

FASE - Invited Talk (Chair: Matt Dwyer, room: Enabler-Wipro)
Software Product Families: Towards Compositionality
Jan Bosch (Nokia, Finland)

10:00 - 10:30 Coffee

10:30 - 12:30 SESSION 2 (Thursday)

ESOP - Static Analysis and Abstract Interpretation I (Chair: Sophia Drossopulou, room: Multicert)
Modular Shape Analysis for Dynamically Encapsulated Programs
Noam Rinetzky (Tel Aviv University), Arnd Poetzsch-Heffter (Universitat Kaiserslautern), Ganesan Ramalingam (Microsoft Research), Mooly Sagiv (Tel Aviv University) and Eran Yahav (IBM T.J. Watson Research Center)
Static Analysis by Policy Interation on Relational Domains
Stephane Gaubert (INRIA), Eric Goubault (CEA/Saclay), Ankur Taly (IIT Bombay) and Sarah Zennou (CEA/Saclay)
Computing Procedure Summaries for Interprocedural Analysis
Sumit Gulwani (Microsoft Research) and Ashish Tiwari (SRI International)
Small witnesses for abstract interpreation based proofs
Frédéric Besson (Irisa/Inria), Thomas Jensen (Irisa/CNRS) and Tiphaine Turpin (Irisa/Université de Rennes 1)
FASE - Specification (Chair: Marsha Chechik, room: Cisco)
Precise Specification of Use Case Scenarios
Jon Whittle (George Mason University, USA)
Joint Structural and Temporal Property Specification using Timed Story Sequence Diagrams
Florian Klein (University of Paderborn, Germany), Holger Giese (University of Paderborn, Germany)
SDL Profiles - Formal Semantics and Tool Support
Rüdiger Grammes (University of Kaiserslautern, Germany), Reinhard Gotzhein (University of Kaiserslautern, Germany)
Preliminary design of BML: A Behavioural Interface Specification Language for java bytecode
Lilian Burdy (INRIA Sophia Antipolis, France), Marieke Huisman (INRIA Sophia Antipolis, France), Mariele Pavlova (INRIA Sophia Antipolis, France)
TACAS - Specification Languages (Chair: Marsha Chechik, room: Enabler-Wipro)
Planned and Traversable Play-Out: A Flexible Method for Executing Scenario-Based Programs
David Harel and Itai Segall (The Weizmann Institute of Science)
MoToR: The MoDeST Tool Environment
Henrik Bohnenkamp (RWTH Aachen University), Holger Hermanns (Saarland University), and Joost-Pieter Katoen (RWTH Aachen University and University of Twente)
Syntactic Optimizations for PSL Verification
Alessandro Cimatti, Marco Roveri (ITC-irst Trento), and Stefano Tonetta (University of Lugano)
The Heterogeneous Tool Set
Till Mossakowski, Christian Maeder (DFKI Lab and University of Bremen), and Klaus Luettich (SFB/TR 8 and University of Bremen)

12:30 - 14:30 Lunch

14:30 - 15:40 SESSION 3A (Thursday)

Unifying Invited Talk (Chair: João Saraiva, room: Enabler-Wipro)
Contract-Driven Development
Bertrand Meyer (ETH Zürich, Switzerland)

15:40 - 15:50 Break

15:50 - 16:50 SESSION 3B (Thursday)

ESOP - Static Analysis and Abstract Interpretation II (Chair: Sophia Drossopulou, room: Multicert)
Interprocedurally analyzing linear inequality relations
Hemut Seidl (Lehrstuhl Seidl, TUM) , Andrea Flexeder (TU Munich) and Michael Petter. (TU Munich)
Precise Fixpoint Computation Through Strategy Iteration
Thomas Gawlitza (Lehrstuhl Seidl, TUM) and Hemut Seidl (Lehrstuhl Seidl, TUM)
TACAS - Security (Chair: Michael Huth, room: Enabler-Wipro)
Searching for Shapes in Cryptographic Protocols
Shaddin F. Doghmi, Joshua D. Guttman, and F. Javier Thayer (The MITRE Corporation)
Automatic Analysis of the Security of XOR-based Key Management Schemes
Veronique Cortier (Loria and CNRS and INRIA), Gavin Keighren, and Graham Steel (University of Edinburgh)

16:50 - 17:15 Coffee

17:15 - 18:45 SESSION 4 (Thursday)

ESOP - Semantic Theories for OO Languages (Chair: Gerard Boudol, room: Multicert)
A Complete Guide to the Future
Frank S. de Boer (CWI), Dave Clarke (CWI) and Einar Broch Johnsen (University of Oslo)
The Java Memory Model: Operationally, Denotationally, Axiomatically
Pietro Cenciarelli (University of Rome - "La Sapienza"), Alexander Knapp (Ludwig-Maximilians University Munich) and Eleonora Sibilio (University of Rome - "La Sapienza")
Immutable Objects for a Java-like Language
Christian Haack (Radboud Universiteit, Nijmegen), Erik Poll (Radboud Universiteit, Nijmegen), Jan Schaefer (TU Kaiserslautern) and Aleksy Schubert (Radboud Universiteit, Nijmegen)
FASE - Services (Chair: José Fiadeiro, room: Cisco)
A Service Composition Construct to Support Iterative Development
Roy Gronmo (SINTEF, Norway), Michael C. Jaeger (Technical University Berlin, Germany), Andreas Wombacher (University Twente, The Netherlands)
Correlation Patterns in Service-Oriented Architectures
Alistair Barros (SAP Research Centre, Australia), Gero Decker (University of Potsdam, Germany), Marlon Dumas (Queensland University of Technology, Australia), Franz Weber (SAP AG, Germany)
Dynamic Characterization of Web Application Interfaces
Marc Fisher II (University of Nebraska-Lincoln, USA), Sebastian Elbaum (University of Nebraska-Lincoln, USA), Gregg Rothermel (University of Nebraska-Lincoln, USA)
TACAS - Software and Hardware Verification (Chair: Orna Grumberg, room: Enabler-Wipro)
State of the Union: Type Inference via Craig Interpolation
Ranjit Jhala (UC San Diego), Rupak Majumdar, and Ru-Gang Xu (UC Los Angeles)
Hoare Logic for Realistically Modelled Machine Code
Magnus O. Myreen and Michael J. C. Gordon (University of Cambridge)
VCEGAR: Verilog CounterExample Guided Abstraction Refinement
Himanshu Jain (Carnegie Mellon University), Daniel Kroening (ETH Zuerich), Natasha Sharygina (Carnegie Mellon University and University of Lugano), and Edmund Clarke (Carnegie Mellon University)

Programme of Friday, March 30

09:00 - 10:00 SESSION 1 (Friday)

ESOP - Invited Talk (Chair: Rocco De Nicola, room: Enabler-Wipro)
Techniques for Contextual Equivalence in Higher-Order, Typed Languages
Andrew Pitts (University of Cambridge, UK)

10:00 - 10:30 Coffee

10:30 - 12:30 SESSION 2 (Friday)

ESOP - Process Algebraic Techniques (Chair: Rocco De Nicola, room: Enabler-Wipro)
Scalar Outcomes Suffice for Finitary Probabilistic Testing
Yuxin Deng (University of New South Wales), Rob van Glabbeek (National ICT Australia), Carroll Morgan (University of New South Wales) and Chenyi Zhang (National ICT Australia)
Probabilistic Anonymity via Coalgebraic Simulations
Ichiro Hasuo (Radboud University Nijmegen) and Yoshinobu Kawabe (NTT Corporation)
Proving Distributed Algorithm Correctness using Fault Tolerance Bisimulations
Adrian Francalanza (Imperial College) and Matthew Hennessy (University of Sussex)
A core calculus for a comparative analysis of bio-inspired calculi
Cristian Versari (University of Bologna)
FASE - Testing (Chair: Reiko Heckel, room: Cisco)
A Prioritization Approach for Software Test Cases Based on Bayesian Networks
Siavash Mirarab (University of Waterloo, Canada), Ladan Tahvildari (University of Waterloo, Canada)
Redundancy Based Test-Suite Reduction
Gordon Fraser (Graz University of Technology, Austria), Franz Wotawa (Graz University of Technology, Austria)
Testing Scenario-Based Models
Hillel Kugler (New York University, USA), Michael J. Stern (Yale University, USA), E. Jane Albert Hubbard (New York University, USA)
Integration Testing in Software Product Line Engineering: A Model-based Technique
Sacha Reis (University of Duisburg-Essen, Germany), Andreas Metzger (University of Duisburg-Essen, Germany), Klaus Pohl (Lero, Ireland and University of Limerick, Ireland and University of Duisburg-Essen, Germany)
TACAS - Decision Procedures and Theorem Provers (Chair: Parosh Abdulla, room: Multicert)
Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications
Marcelo F. Frias, Carlos G. Lopez Pombo, and Mariano M. Moscato (Universidad de Buenos Aires and CONICET)
Combined Satisfiability Modulo Parametric Theories
Sava Krstic, Amit Goel, Jim Grundy (Intel Corporation), and Cesare Tinelli (The University of Iowa)
A Groebner Basis Approach to CNF-formulae Preprocessing
Christopher Condrat and Priyank Kalla (University of Utah)
Kodkod: A Relational Model Finder
Emina Torlak and Daniel Jackson (Massachusetts Institute of Technology)

12:30 - 14:30 Lunch

14:30 - 16:30 SESSION 3 (Friday)

ESOP - Applicative Programming (Chair: Matthew Hennessy, room: Cisco)
A Rewriting Semantics for Type Inference
George Kuan (University of Chicago), David MacQueen (University of Chicago) and Robert Bruce Findler (University of Chicago)
Principal Type Schemes for Modular Programs
Derek Dreyer (Toyota Technological Institute at Chicago) and Matthias Blume (Toyota Technological Institute at Chicago)
A Consistent Semantics of Self-Adjusting Computation
Umut Acar (Toyota Technological Institute at Chicago), Matthias Blume (Toyota Technological Institute at Chicago) and Jacob Donham (Carnegie Mellon University)
Multi-Language Synchronization
Robert Ennals (Intel Research, Berkeley) and David Gay (Intel Research, Berkeley)
FASE - Analysis (Chair: Tom Maibaum, room: Unicre)
Practical reasoning about invocations and implementations of pure methods
Ádám Darvas (ETH Zurich, Switzerland), K. Rustan M. Leino (Microsoft Research, USA)
Finding Environment Guarantees
Marsha Chechik (University of Toronto, Canada), Mihaela Gheorghiu (University of Toronto, Canada), Arie Gurfinkel (University of Toronto, Canada)
Ensuring Consistency within Distributed Graph Transformation Systems
Ulrike Ranger (RWTH Aachen University, Germany), Thorsten Hermes (RWTH Aachen University, Germany)
Maintaining Consistency in Layered Architectures of Mobile Ad-hoc Networks
Julia Padberg (Technical University Berlin, Germany), Kathrin Hoffmann (Technical University Berlin, Germany), Hartmut Ehrig (Technical University Berlin, Germany), Tony Modica (Technical University Berlin, Germany), Enrico Biermann (Technical University Berlin, Germany), Claudia Ermel (Technical University Berlin, Germany)
TACAS - Model Checking (Chair: Orna Grumberg, room: Multicert)
Bounded Reachability Checking of Asynchronous Systems Using Decision Diagrams
Jinqing Yu, Gianfranco Ciardo (University of California, Riverside), and Gerald Luettgen (University of York)
Model Checking of Tree Logics with Path Equivalences
Rajeev Alur, Pavol Cerny, and Swarat Chaudhuri (University of Pennsylvania)
Uppaal/DMC - Abstraction-based Heuristics for Directed Model Checking
Sebastian Kupferschmid (University of Freiburg), Klaus Drager (Universitat des Saarlandes), Jorg Hoffmann (Digital Enterprise Research Institute, Innsbruck), Berd Finkbeiner (Universitat des Saarlandes), Henning Dierks (OFFIS, Oldenburg), Andreas Podelski (University of Freiburg), Gerd Behrmann (Aalborg University)
mCRL Distributed State Space Generation in Practice
Stefan Blom (Universitat Innsbruck), Jens R. Calame, Bert Lisser (CWI, Amsterdam), Simona Orzan (TU/e, Eindhoven), Jun Pang (Carl von Ossietzky Universitat, Oldenburg), Jaco van de Pol (CWI, Amsterdam and TU/e, Eindhoven), Mohammad Torabi Dashti, and Anton J. Wijs (CWI, Amsterdam)

16:30 - 17:00 Coffee

17:00 - 18:30 SESSION 4 (Friday)

ESOP - Types for Systems Properties (Chair: Walid Taha, room: Cisco)
Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts
Kohei Suenaga (University of Tokyo) and Naoki Kobayashi (Tohoku University)
Type Reconstruction for an Undecidable System of Refinement Types
Kenneth Knowles (University of California, Santa Cruz) and Cormac Flanagan (University of California, Santa Cruz)
Dependent Types for Low-Level Programming
Jeremy Condit (University of California, Berkeley), Matthew Harren (University of California, Berkeley), Zachary Anderson (University of California, Berkeley), David Gay (Intel Research, Berkeley) and George C. Necula (University of California, Berkeley)
FASE - Design (Chair: Antónia Lopes, room: Unicre)
Towards Normal Design for Safety-Critical Systems
Derek Mannering (General Dynamics, UK), Jon G. Hall (The Open University, UK), Lucia Rapanotti (The Open University, UK)
A Clustering-based Approach for Tracing Object-Oriented Design to Requirement
Xin Zhou (IBM China Research Lab, China), Hui Yu (Peking University, China)
Measuring and Characterizing Crosscutting in Aspect-Based Programs: Basic Metrics and Case Studies
Roberto E. Lopez-Herrejon (University of Oxford, England), Sven Apel (University of Magdeburg, Germany)
TACAS - Infinite-State Systems (Chair: Michael Huth, room: Multicert)
A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes
Ahmed Bouajjani, Yan Jurski, and Mihaela Sighireanu (LIAFA, University of Paris 7)
Unfolding Concurrent Well-Structured Transition Systems
Frederic Herbreteau, Gregoire Sutre, and The Quang Tran (LaBRI, Bordeaux)
Regular Model Checking without Transducers (On Efficient Verification of Parameterized Systems)
Parosh Aziz Abdulla (Uppsala University), Giorgio Delzanno (Universita di Genova), Noomene Ben Henda, and Ahmed Rezine (Uppsala University)

Further ETAPS 2007 Programme Information:

ETAPS 2007 | Top | HTML 4.01 | Last Update: 2007-03-21