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:
- Programme Overview, Social Programme
- Main Conferences:
CC,
ESOP,
FASE,
FOSSACS,
TACAS
- Workshops:
ACCAT,
Bytecode,
COCV,
FESCA,
FinCo,
GT-VMT,
HAV,
HFL,
LDTA,
MBT,
MOMPES,
OpenCert,
QAPL,
SC,
SLA++P,
TERMGRAPH,
WITS
- Tutorials:
Stratego/XT,
SoftwGen,
Mobius
ETAPS 2007 |
Top |
HTML 4.01 |
Last Update: 2007-03-21