Programme of Main Conferences at ETAPS 2008

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

Welcome
FASE - Invited Talk (room: Europa)
On the Utility of Formal Methods in Building Software: A Panacea or Academic Poppycock?
Connie Heitmeyer (Naval Research Laboratory Washington, USA)

10:30 - 11:00 Coffee

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

ESOP - SEMANTICS, PARAMETRICITY AND TYPES (room: Magnolia)
A Sound Semantics for OCaml light
Scott Owens (University of Cambridge, UK)
Parametric polymorphism through run-time sealing, or Theorems for low, low prices!
Jacob Matthews (University of Chicago, USA) and Amal Ahmed (Toyota Technological Institute at Chicago, USA)
Regular Expression Subtyping for XML Query and Update Languages
James Cheney (University of Edinburgh, UK)
FASE - REQUIREMENTS AND ARCHITECTURES (room: Ybl)
Deriving Non-Zeno Behavior Models from Goal Models using ILP
Dalal Alrajeh, Alessandra Russo (Imperial College London, UK). Uchitel, Sebastian (University of Buenos Aires, Argentina)
What's in a Feature: A Requirements Engineering Perspective
Andreas Classen,Patrick Heymans and Pierre-Yves Schobbens (University of Namur, Belgium)
Formal Approach to Integrating Feature and Architecture Models
MikolአJanota (University College Dublin, Ireland) and Goetz Botterweck (University of Limerick, Ireland)
TACAS - PARAMETERIZED SYSTEMS (room: Star)
Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages
Azadeh Farzan (Carnegie Mellon University, USA), Yu-Fang Chen (National Taiwan University), Edmund Clarke (Carnegie Mellon University, USA), Yih-Kuen Tsay (National Taiwan University) and Bow-Yaw Wang (Academia Sinica, Taiwan)
Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols
Mayank Saksena, Oskar Wibling and Bengt Jonsson (Uppsala University, Sweden)
Proving Ptolemy Right: The Environment Abstraction Principle for Model Checking Concurrent Systems
Edmund Clarke, Muralidhar Talupur (Carnegie Mellon University, USA) and Helmut Veith (Technical University of München, Germany)

12:30 - 14:30 Lunch

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

ESOP - SEMANTICS (room: Magnolia)
A Theory of Hygienic Macros
David Herman and Mitchell Wand (Northeastern University, USA)
A Hybrid Denotational Semantics for Hybrid Systems
Olivier Bouissou (CEA - Atomic Energy Commission, France) and Matthieu Martel (The University of Perpignan Via Domitia, France)
Full Abstraction for Linda
Cinzia Di Giusto and Maurizio Gabbrielli (University of Bologna, Italy)
Practical Programming with Higher-Order Encodings and Dependent Types
Adam Poswolsky (Yale University, USA) and Carsten Schürmann (IT University of Copenhagen, Denmark)
FASE - MODELS, MODEL TRANSFORMATIONS I (room: Ybl)
Correctness-Preserving Configuration of Business Process Model
Wil M.P. van der Aalst, Gottschalk, Florian (Eindhoven University of Technology, The Netherlands) Marlon Dumas, Arthur H.M. Hofstede, Marcello La Rosa and Jan Mendling (Queensland University of Technology, Australia)
Consistent Integration of Models Based on Views of Visual Languages
Claudia Ermel, Hartmit Ehrig, Ulrike Prange (Technical University Berlin, Germany) and Karsten Ehrig (University of Leicester, UK)
Translating Model Simulators to Analysis Models
Juan de Lara(Universidad Autónoma Madrid, Spain) and Hans Vangheluwe (McGill University, Canada)
Language-based optimisation of sensor-driven distributed computing applications
Jonathan Davies, Alastair Beresford, Alan Mycroft (University of Cambridge, UK)
TACAS - MODEL CHECKING I (room: Star)
Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking
Jiri Barnat, Lubos Brim, Pavel Simecek (Masaryk University Brno, Czech Republic) and Michael Weber (University of Twente, The Netherlands)
Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
Martin De Wulf (Université Libre de Bruxelles, Belgium), Laurent Doyen (Ecole Polytechnique Fédérale de Lausanne, Switzerland), Nicolas Maquet and Jean-Francois Raskin (Université Libre de Bruxelles, Belgium)
On-the-Fly Techniques for Games-Based Software Model Checking
Adam Bakewell and Dan Ghica (University of Birmingham, UK)
Computing Simulations over Tree Automata
Parosh Abdulla (Uppsala University, Sweden) , Ahmed Bouajjani (University of Paris 7, France), Lukas Holik (Brno University of Technology, Czech Republic), Lisa Kaati (Uppsala University, Sweden) and Tomas Vojnar (Brno University of Technology, Czech Republic)

16:30 - 17:00 Coffee

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

ESOP - SEMANTICS (room: Magnolia)
Programming in JoCaml
Louis Mandel and Luc Maranget (INRIA Rocquencourt, France)
Playing with Toy: Constraints and Domain Cooperation
Sonia Estévez (Universidad Complutense de Madrid, Spain), Antonio J. Fernández (Universidad de Málaga, Spain) and Fernando Saenz-Perez (Universidad Complutense de Madrid, Spain)
Typing safe deallocation
Gerard Boudol (INRIA Sophia-Antipolis Méditérranée, France)
Iterative Specialisation of Horn Clauses
Christoffer Rosenkilde Nielsen, Flemming Nielson and Hanne Riis Nielson (Technical University of Denmark, Denmark)
FASE - CONCEPTUAL MODELS, UML (room: Ybl)
Orthographic Software Modeling Environment (TOOL DEMO)
Dietmar Stoll and Colin Atkinson (University of Mannheim, Germany)
HOL-OCL: A Formal Proof Environment for UML/OCL (TOOL DEMO)
Achim Brucker, Burkhart Wolff (ETH Zurich, Switzerland)
Towards Faithful Model Extraction Based on Contexts
Lucio Mauro Duarte, Jeff Kramer (Imperial College London, UK) and Sebastian Uchitel (University of Buenos Aires, Argentina)
Leveraging Patterns On Domain Models To improve UML Profile Definition
François Lagarde, Huascar Espinoza, François Terrier (CEA - Atomic Energy Commission, France) and Charles Andre (I3S Laboratory, France)
TACAS - APPLICATIONS (room: Star)
Formal Pervasive Verification of a Paging Mechanism
Eyad Alkassar (Saarland University, Germany), Norbert Schirmer (Technical University of München, Germany) and Artem Starostin (Saarland University, Germany)
Analyzing Stripped Device-Driver Executables
Gogul Balakrishnan (NEC Laboratories America, USA) and Thomas Reps (University of Wisconsin-Madison, USA)
Model Checking-Based Genetic Programming with Application to Mutual Exclusion
Gal Katz (Bar-Ilan University, Israel) and Doron Peled (University of Warwick, UK)

Programme of Tuesday, April 1

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

ESOP - Invited Talk (room: Europa)
Constructive Mathematics and Functional Programming
Thierry Coquand (Göteborg University, Sweden)

10:00 - 10:30 Coffee

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

ESOP - STATIC ANALYSIS (room: Magnolia)
Ranking Abstractions
Aziem Chawdhary (Queen Mary, University of London, UK), Byron Cook (Microsoft Research, UK), Sumit Gulwani (Microsoft Research, UK), Mooly Sagiv (Tel-Aviv University, Israel) and Hongseok Yang (Queen Mary, University of London, UK)
Non-disjunctive Numerical Domain for Array Predicate Abstraction
Xavier Allamigeon (EADS Innovation Works / CEA-LIST MeASI, France)
Upper Adjoints for Fast Inter-procedural Variable Equalities
Markus Müller-Olm (Westfälische Wilhelms-Universität Münster, Germany) and Helmut Seidl (Technische Universität München, Germany)
Cover Algorithms and their Combination
Sumit Gulwani (Microsoft Research, UK) and Madanlal Musuvathi (Microsoft Research, US)
FASE - SERVICE ENGINEERING / ADAPTABLE SERVICES (room: Ybl)
When things go wrong: Interrupting conversations
Juliana Bowles (University of St Andrews, UK) and Sotiris Moschoyiannis (University of Surrey, UK)
Distributed Behavioural Adaptation for the Automatic Composition of Semantic Services
Tarekm Melliti (Université d' Evry Val d'Essonne, France) Pascal Poizat and Sonia Ben Mokhtar (INRIA/ALPES, France)
Engineering Service Oriented Applications: From StPowla Processes to SRML Models
Laura Bocchi (University of Leicester, UK), Stephan Reiff-Marganiec (University of Leicester, UK) and Stephen Gorton (ATX Technologies, UK)
Formal Framework for the Iterative Model/Driven Development of Adaptable Service-Based Applications
Leen Lambers (Technical University Berlin, Germany), Harmut Ehrig (Technical University Berlin, Germany), Leonardo Mariani (University of Milano-Bicocca, Italy), Mauro Pezze (University of Milano-Bicocca, Italy)
TACAS - MODEL CHECKING II (room: Star)
Conditional probabilities over probabilistic and nondeterministic systems
Miguel Andres (University of Nijmegen, The Netherlands) and Peter van Rossum (University of Nijmegen, The Netherlands)
On Automated Verification of Probabilistic Programs
Axel Legay (University of Ličge, Belgium), Andrzej Murawski (Oxford University Computing Laboratory, UK), Joel Ouaknine (Oxford University Computing Laboratory, UK) and James Worrell (Oxford University Computing Laboratory, UK)
Symbolic Model Checking of Hybrid Systems using Template Polyhedra
Sriram Sankaranarayanan (NEC Laboratories, US), Thao Dang (CNRS, France), Franjo Ivancic (NEC Laboratories, US)
Fast Directed Model Checking via Russian Doll Abstraction
Sebastian Kupferschmid (Albert-Ludwigs-Universität Freiburg, Germany), Joerg Hoffmann (University of Innsbruck, Austria) and Kim Larsen (Aalborg University, Denmark)

12:30 - 14:30 Lunch

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

ESOP - SECURITY I (room: Magnolia)
Trust and Authorization via Provenance and Integrity in Distributed Objects
Andrew Cirillo (DePaul University, US), Radha Jagadeesan (DePaul University, US), Corin Pitcher (DePaul University, US) and James Riely (DePaul University, US)
Linear Declassification
Yuta Kaneko (Tohoku University, Japan) and Naoki Kobayashi (Tohoku University, Japan)
Just Forget It - The Semantics of Enforcement of Information Erasure
Sebastian Hunt (City University London, UK) and David Sands (Chalmers university of Technology, Sweden)
FASE - VERIFICATION AND TESTING I (room: Ybl)
A Logic of Graph Constraints
Fernando Orejas (Universitat Politecnica de Catalunya, Spain), Harmut Ehrig (Technical University Berlin, Germany) and Ulrike Prange (Technical University Berlin, Germany)
A generic complete dynamic logic for reasoning about purity and effects
Till Mossakowski (DFKI Laboratory Bremen, Germany), Lutz Schröder (DFKI Laboratory Bremen, Germany) and Sergey Goncharov (University of Bremen, Germany)
Modelling and Verification of Timed Interaction and Migration
Gabriel Ciobanu (A.I.Cuza University of Iasi, Romania) and Maciej Koutny (Newcastle University, UK)
A model checking approach for verifying COWS specifications
Alessandro Fantechi (University of Florence and ISTI-CNR, Italy), Alessandro Lapadula (University of Florence, Italy), Rosario Pugliese (University of Florence, Italy), Francesco Tiezzi (University of Florence, Italy), Stefania Gnesi (ISTI-CNR, Italy) and Franco Mazzanti (ISTI-CNR, Italy)
TACAS - STATIC ANALYSIS (room: Star)
A SAT based approach to size change termination with global ranking functions
Amir Ben-Amram (The Academic College of Tel-Aviv Yaffo, Israel) and Michael Codish (Ben-Gurion University of the Negev, Israel)
Efficient Automatic STE Refinement Using Responsibility
Hana Chockler (IBM HRL, Israel), Orna Grumberg (Israel Institute of Technology, Israel) and Avi Yadgar (Israel Institute of Technology, Israel)
Reasoning Algebraically About P-solvable Loops
Laura Kovacs ( École Polytechnique Fédérale de Lausanne, Switzerland)
On local reasoning in verification
Carsten Ihlemann (Max-Planck-Institut für Informatik, Germany), Swen Jacobs (Max-Planck-Institut für Informatik, Germany) and Viorica Sofronie-Stokkermans (Max-Planck-Institut für Informatik, Germany)

16:30 - 17:00 Coffee

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

ESOP - CONCURRENCY (room: Magnolia)
Open Bisimulation for the Concurrent Constraint Pi-Calculus
Maria Grazia Buscemi and Ugo Montanari (Universita di Pisa, Italy)
The Conversation Calculus: A Model of Service Oriented Computation
Hugo Vieira (New University of Lisbon, Portugal), Luis Caires (New University of Lisbon, Portugal) and Joao Seco (New University of Lisbon, Portugal)
Inferring Channel Buffer Bounds via Linear Programming
Tachio Terauchi (Graduate School of Information Sciences, Tohoku University, Japan) and Adam Megacz (UC Berkeley, USA)
FASE (17:00 - 18:45) - VERIFICATION AND TESTING II (room: Ybl)
Contextual Integration Testing of Classes
Giovanni Denaro (University of Milano-Bicocca, Italy) Alessandra Gorla and Mauro Pezze (University of Lugano, Switzerland)
An Automatic Verifier for Java-like Programs Based on Dynamic Frames
Jan Smans, Bart Jacobs, Frank Piessens (Katholieke Universiteit Leuven, Belgium) and Wolfram Schulte (Microsoft Research Redmond, USA)
A Domain Analysis to Specify Design Defects and Generate Detection Algorithms
Naouel Moha, Yann-Gaël Guéhéneuc, (University of Montreal Quebec, Canada) Laurence Duchien and Anne-Françoise Le Meur (Université des Sciences et Technologies de Lille, France)
Automated Analysis of Permission-Based Security using UMLsec (TOOL DEMO)
Jan Jurjens (The Open University, UK), Jorg Schreck (O2 Munich, Germany) and Yijun Yu (The Open University, UK)
TACAS - CONCURRENT / DISTRIBUTED SYSTEMS (room: Star)
Interprocedural Analysis of Concurrent Programs Under a Context Bound
Akash Lal (University of Wisconsin-Madison), Tayssir Touili (LIAFA, France), Nicholas Kidd (University of Wisconsin-Madison) and Thomas Reps (University of Wisconsin-Madison)
Context-bounded analysis of concurrent queue systems
Salvatore La Torre (Universita degli Studi di Salerno, Italy), Madhusudan Parthasarathy (University of Illinois at Urbana-Champaign, USA) and Gennaro Parlato (Universita degli Studi di Salerno, Italy)
On Verifying Fault Tolerance of Distributed Protocols
Dana Fisman (The Weizmann Institute of Science, Israel), Orna Kupferman (Hebrew University of Jerusalem, Israel) and Yoad Lustig (Hebrew University of Jerusalem, Israel)

Programme of Wednesday, April 2

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

Unifying Invited Talk (room: Europa)
Verification of higher-order computation: a game-semantic approach
Luke Ong (University of Oxford, United Kingdom)

10:00 - 10:30 Coffee

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

ESOP - PROGRAM VERIFICATION (room: Magnolia)
Verification of Equivalent-Results Methods
Rustan Leino and Peter Müller (Microsoft Research, USA)
Semi-Persistent Data Structures
Sylvain Conchon and Jean-Christophe Filliatre (Université Paris Sud, France)
A Realizability Model for Impredicative Hoare Type Theory
Rasmus L. Petersen, Lars Birkedal (IT University of Copenhagen, Denmark), Aleksandar Nanevski and Greg Morrisett (Harvard University, USA)
Oracle Semantics for Concurrent Separation Logic
Aquinas Hobor, Andrew Appel (Princeton University, USA) and Francesco Zappa Nardelli (INRIA Rocquencourt, France)
FASE - OBJECTS AND COMPONENTS (room: Ybl)
Clint: A Composition Language Interpreter (TOOL DEMO)
Javier Camára, Gwen Salaün and Carlos Canal (Universidad de Málaga, Spain)
Software quality improvement via pattern matching (TOOL DEMO)
Radu Kopetz and Pierre-Etienne Moreau (INRIA & LORIA, France)
Object Composition in Scenario-Based Programming
Yoram Atir, David Harel, Asaf Kleinbort and Shahar Maoz (The Weizmann Institute of Science, Israel)
Regular Inference for State Machines using Domains with Equality Tests
Therese Berg, Bengt Jonsson (Uppsala University, Sweden) and Harald Raffelt (University of Dortmund, Germany)
COMP-REF: A Technique to Guide the Delegation of Responsibilities to Components in Software Systems
Subhajit Datta, and Robert van Engelen (Florida State University, USA)
FOSSACS - GAMES (room: Star)
Simple Stochastic Games with Few Random Vertices are Easy to Solve
Hugo Gimbert (LABRI Bordeaux, France) and Florian Horn (Paris 7 University, France)
The Complexity of Nash Equilibria in Infinite Multiplayer Games
Michael Ummels (RWTH Aachen, Germany)
Stochastic Games with Lossy Channels
Noomene Ben Henda, Parosh Abdulla (Uppsala University, Sweden) Richard Mayr (North Carolina State University, USA) Luca de Alfaro (University of California at Santa Cruz, USA) and Sven Sandberg (Uppsala University, Sweden)
Simulation Hemi-Metrics Between Infinite-State Stochastic Games
Jean Goubault-Larrecq (ENS Cachan, France)

12:30 - 14:30 Lunch

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

Unifying Invited Talk (room: Europa)
WYSINWYX: What You See Is Not What You eXecute
Tom Reps (University of Wisconsin-Madison, USA)

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

ESOP - SECURITY II (room: Ybl)
Certificate~Translation in Abstract Interpretation
Gilles Barthe and César Kunz (INRIA Sophia Antipolis-Méditerranée, France)
A formal implementation of value commitment
Cédric Fournet (Microsoft Research, USA), Nataliya Guts (INRIA-Microsoft Research Joint Centre, France) and Francesco Zappa Nardelli (INRIA Rocquencourt, France)
FOSSACS - ALGEBRAIC MODELS I (room: Jazmin II.)
Beyond Rank 1: Algebraic Semantics and Finite Models for Coalgebraic Logics
Dirk Pattinson (Imperial College London, United Kingdom) and Lutz Schroeder (Bremen University, Germany)
Linear-non-linear model for a computational call-by-value lambda calculus
Benoit Valiron (University of Ottawa, Canada) and Peter Selinger (Dalhousie University, Canada)
FOSSACS - DECISION PROBLEMS I (room: Jazmin I.)
The Omega-Regular Post Embedding Problem
Pierre Chambart and Philippe Schnoebelen (ENS Cachan, France)
Complexity of decision problems for mixed and modal specifications
Adam Antonik, Michael Huth (Imperial College London, United Kingdom) Kim G. Larsen, Ulrik Nyman and Andrzej Wasowski (Aalborg University, Denmark)
TACAS - TOOLS I (room: Star)
The Real-Time Maude Tool
Peter Olveczky (University of Oslo, Norway) and Jose Meseguer (University of Illinois at Urbana-Champaign, USA)
Z3: An Efficient SMT Solver
Leonardo de Moura and Nikolaj Bjorner (Microsoft Research, USA)
Computation and visualisation of phase portraits for model checking SPDIs
Gordon Pace (University of Malta, Malta) and Gerardo Schneider (University of Oslo, Norway)
GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic
Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Wen-Chin Chan and Chi-Jian Luo (National Taiwan University, Taiwan)

16:30 - 17:00 Coffee

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

FASE - MODELS, MODEL TRANSFORMATIONS II (room: Ybl)
Verification of Architectural Refactorings by Rule Extraction
Dénes Bisztray, Reiko Heckel (University of Leicester, United Kingdom) and Hartmut Ehrig (Technical University Berlin, Germany)
Formal Model-driven Program Refactoring
Tiago Massoni (University of Pernambuco, Brazil) Rhit Gheyi and Paulo Borba (Federal University of Pernambuco, Brazil)
An Algebraic Semantics for MOF
Artur Boronat (University of Leicester, United Kingdom) and José Meseguer (University of Illinois at Urbana-Champaign, USA)
FOSSACS - AUTOMATA AND TIMED SYSTEMS (room: Jazmin I.)
Classes of Tree Homomorphisms with Decidable Preservation of Regularity
Guillem Godoy (Technical University Catalonia, Spain) Sebastian Maneth (New South Wales University, Australia) and Sophie Tison (Lille 1 University, France)
A Kleene-Schűtzenberger Theorem for Weighted Timed Automata
Manfred Droste and Karin Quaas (Leipzig University, Germany)
Robust Analysis of Timed Automata via Channel Machines
Patricia Bouyer (Oxford University, United Kingdom), Nicolas Markey (ENS Cachan, France) and Pierre-Alain Reynier (Brussels Free University, Belgium)
TACAS - SYMBOLIC EXECUTION (room: Star)
RWset: Attacking Path Explosion in Constraint-Based Test Generation
Peter Boonstoppel, Cristian Cadar and Dawson Engler (Stanford University, USA)
Demand-Driven Compositional Symbolic Execution
Saswat Anand (Georgia Institute of Technology, USA), Patrice Godefroid and Nikolai Tillmann (Microsoft Research, USA)
Peephole Partial Order Reduction
Chao Wang, Zijiang Yang , Vineet Kahlon and Aarti Gupta (NEC Laboratories America, USA)

Programme of Thursday, April 3

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

TACAS- Invited Talk (room: Europa)
Hardware Verification: Techniques, Methodology and Solutions
Sharad Malik (Princeton University, USA)

10:00 - 10:30 Coffee

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

CC - ANALYSIS AND TRANSFORMATIONS (room: Ybl)
A System for Generating Static Analyzers for Machine Instructions
Junghee Lim and Thomas Reps (University of Wisconsin-Madison, USA)
IDE Dataflow Analysis in the Presence of Large Object-Oriented Libraries
Atanas Rountev, Mariana Sharp and Guoqing Xu (The Ohio State University, USA)
An Adaptive Strategy for Inline Substitution
Keith D. Cooper, Timothy J. Harvey and Todd Waterman (Rice University, USA)
Automatic Transformation of Bit-Level C Code to Support Multiple Equivalent Data Layouts
Marius Nita and Dan Grossman (University of Washington, USA)
FOSSACS - LOGICS (room: Jazmin I.)
The common fragment of ACTL and LTL
Mikolaj Bojanczyk (Warsaw University, Poland)
The complexity of CTL* + linear past
Laura Bozzelli (Naples University, Italy)
Footprints in Local Reasoning
Mohammad Raza and Philippa Gardner (Imperial College, London, UK)
A Modal Deconstruction of Access Control Logics
Deepak Garg (CMU, Pittsburgh, USA) and Martin Abadi (University of California at Santa Cruz, USA)
TACAS - ABSTRACTION, INTERPOLATION (room: Star)
Efficient Interpolant Generation in Satisfiability Modulo Theories
Alessandro Cimatti (IRST, Trento, Italy), Alberto Griggio and Roberto Sebastiani (University di Trento, Italy)
Generating Quantified Invariants with an Interpolating Saturation Prover
Kenneth McMillan (Cadence Berkeley Labs, USA)
Accelerating Interpolation-based Model-Checking
Nicolas Caniart,Emmanuel Fleury, Jerome Leroux and Marc Zeitoun (University Bordeaux, France)
Automatically Refining Abstract Interpretations
Bhargav Gulavani, Supratik Chakraborty (Indian Institute of Technology, Bombay), Aditya Nori and Sriram Rajamani (Microsoft Research India)

12:30 - 14:30 Lunch

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

FOSSACS - Invited Talk (room: Europa)
Finding your way in a forest: on different types of trees and their properties
Igor Walukiewicz (LaBRI, Université Bordeaux-1, France)

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

FOSSACS - ALGEBRAIC MODELS II (room: Jazmin II.)
Coalgebraic Logic and Synthesis of Mealy Machines
Alexandra Silva (CWI Amsterdam, Netherlands), Marcello Bonsangue (Leiden University, Netherlands) and Jan Rutten (CWI Amsterdam, Netherlands)
The Microcosm Principle and Concurrency in Coalgebra
Ichiro Hasuo (Kyoto University, Japan), Bart Jacobs (Radboud University Nijmegen, Netherlands) and Ana Sokolova (Salzburg University, Austria)
FOSSACS - DECISION PROBLEMS II (room: Jazmin I.)
Systems of Equations Satisfied in All Commutative Finite Semigroups
Pawel Parys (Warsaw University, Poland)
Optimal Lower Bounds on Regular Expression Size using Communication Complexity
Hermann Gruber and Jan Johannsen (LMU University München, Germany)
TACAS - TOOLS II (room: Star)
SVISS: Symbolic Verification of Symmetric Systems
Thomas Wahl, Nicolas Blanc (ETH Zürich, Switzerland) and Allen Emerson (University of Texas at Austin, USA)
RESY: Requirement Synthesis for Compositional Model Checking
Bernd Finkbeiner, Hans-Jorg Peter and Sven Schewe (Saarland University, Germany)
Scoot: A tool for static analysis of SystemC models
Nicolas Blanc, Daniel Kroening (ETH Zürich, Switzerland) and Natasha Sharygina (University of Lugano, Switzerland)

16:30 - 17:00 Coffee

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

CC - COMPILING FOR PARALLEL ARCHITECTURES (room: Ybl)
Control Flow Emulation on Tiled SIMD Architectures
Ghulam Lashari, Ondrej Lhoták and Michael McCool (University of Waterloo, Canada)
Generating SIMD Vectorized Permutations
Franz Franchetti and Markus Püschel (Carnegie Mellon University, USA)
Automatic Transformations for Communication-Minimized Parallelization and Locality Optimization in the Polyhedral Model
Uday Kumar Bondhugula, Muthu Baskaran, Sriram Krishnamoorthy, J Ramanujam, Atanas Rountev and P Sadayappan (Ohio State University, USA)
FOSSACS - PROBABILISTIC SYSTEMS (room: Jazmin I.)
On Decision Problems for Probabilistic Buechi Automata
Christel Baier (Dresden Technical University, Germany), Nathalie Bertrand (IRISA Rennes, France) and Marcus Groesser (Dresden Technical University, Germany)
Model-Checking ω-Regular Properties of Interval Markov Chain
Krishnendu Chatterjee, Koushik Sen (University of California at Berkeley, USA) and Thomas Henzinger (EPFL Lausanne, Switzerland)
Prevision Domains and Convex Powercones
Jean Goubault-Larrecq (ENS de Cachan, France)
TACAS - TRUST, REPUTATION (room: Star)
Trusted Source Translation of a Total Function Language
Guodong Li and Konrad Slind (University of Utah, USA)
Rocket-fast Proof Checking For SMT Solvers
Michal Moskal (University of Wroclaw, Poland)
SDSIrep: A Reputation System based on SDSI
Javier Esparza (TU München, Germany), Ahmed Bouajjani (University of Paris, France), Stefan Schwoon (University of Stuttgart, Germany) and Dejvuth Suwimonteerabuth (TU München, Germany)
 

Programme of Friday, April 4

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

CC - Invited Talk (room: Star)
Design Choices in a Compiler Course - or - How to Make Undergraduates Love Formal Notation
Michael Schwartzbach (University of Aarhus, Denmark)

10:00 - 10:30 Coffee

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

CC - RUNTIME TECHNIQUES AND TOOLS (room: Ybl)
How to do a million watchpoints: Efficient Debugging using Dynamic Instrumentation
Qin Zhao (National University of Singapore, Singapore), Rodric Rabbah (IBM Research, USA), Saman Amarasinghe (Massachusetts Institute of Technology, USA), Larry Rudolph (VMware Inc., USA) and Weng-Fai Wong (National University of Singapore, Singapore)
Compiler-guaranteed Safety in Code-copying Virtual Machines
Gregory B. Prokopski and Clark Verbrugge (McGill University, Canada)
Hardware JIT compilation for off-the-shelf dynamically reconfigurable FPGAs
Etienne Bergeron, Marc Feeley and Jean Pierre David (Université de Montréal, Canada)
Visualization of Program Dependence Graphs (TOOL DEMO)
Thomas Würthinger, Christian Wimmer and Hanspeter Mössenböck (Johannes Kepler University, Germany)
FOSSACS - TYPES AND LAMBDA CALCULUS (room: Star)
RPO, Second Order Contexts, and lambda-calculus
Pietro Di Gianantonio, Furio Honsell and Marina Lenisa (Udine University, France)
An Erasure Semantics for Pure Type Systems
Nathan Mishra Linger and Tim Sheard (Portland State University, USA)
The Implicit Calculus of Constructions as a Programming Language with Dependent Types
Bruno Barras and Bruno Bernardo (INRIA, France)
Strong Normalisation of Cut-Elimination that Simulates Beta-Reduction
Kentaro Kikuchi (Tohoku University, Japan) and Stephane Lengrand (CNRS, France)

12:30 - 14:30 Lunch

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

CC - ANALYSES (room: Ybl)
On the Relative Completeness of Bytecode Analysis versus Source Code Analysis
Francesco Logozzo and Manuel Fähndrich (Microsoft Research, USA)
Efficiency, Precision, Simplicity, and Generality in Interprocedural Data Flow Analysis: Resurrecting the Classical Call Strings Method
Uday P. Khedker and Bageshri Karkare (Indian Institute of Technology, India)
Java Bytecode Verification for @NonNull Types
Chris Male, David Pearce, Alex Potanin and Constantine Dymnikov (Victoria University of Wellington, New Zealand)
Efficient Context-Sensitive Shape Analysis with Graph Based Heap Models
Mark Marron, Manuel Hermenegildo, Deepak Kapur and Darko Stefanovic (The University of New Mexico, USA)
FOSSACS - PROCESS CALCULI (room: Star)
Symbolic Semantics Revisited
Filippo Bonchi and Ugo Montanari (Pisa University, Italy)
Deriving Bisimulation Congruences in the Presence of Negative Application Conditions
Guilherme Rangel (Berlin Technical University, Germany) Barbara Koenig (Duisburg-Essen University, Germany) and Hartmut Ehrig (Berlin Technical University, Germany)
Structural operational semantics for stochastic process calculi
Bartek Klin (Edinburgh University, UK) and Vladimiro Sassone (Southampton University, UK)
Compositional Methods for Information-Hiding
Christelle Braun, Konstantinos Chatzikokolakis and Catuscia Palamidessi (INRIA, France)

16:30 - 17:00 Coffee

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

CC - ATOMICITY AND TRANSACTIONS (room: Ybl)
Coqa: Concurrent Objects with Quantized Atomicity
Yu David Liu, Xiaoqi Lu and Scott F. Smith (Johns Hopkins University, USA)
Keep Off The Grass: Locking the Right Path for Atomicity
Dave Cunningham, Khilan Gudka and Susan Eisenbach (Imperial College London, UK)
Supporting Legacy Binary Code in a Software Transaction Compiler with Dynamic Binary Translation and Optimization
Cheng Wang, Victor Ying and Youfeng Wu (Intel MTL, USA).
FOSSACS - VERIFICATION (room: Star)
Products of Message Sequence Charts
Philippe Darondeau, Blaise Genest and Loic Helouet (IRISA, France)
What else is decidable about arrays?
Radu Iosif (CNRS, France), Peter Habermehl (ENS, France) and Tomas Vojnar (Brno Technical University, Czech Republic)
Model checking freeze LTL over one-counter automata
Stephane Demri (ENS, France) Ranko Lazic (Warwick University, UK) and Arnaud Sangnier (ENS, France)

Detailed Programme Information:

ETAPS 2008 | Top | HTML 4.01 | Last Update: 2007-12-27