CSDL - Proceedings S

Third IEEE International Conference on Software Engineering and Formal Methods - Copyright (PDF)

pp. iv

Introduction

Preface (PDF)

pp. x

Program Committee (PDF)

pp. xi

Steering Committee (PDF)

pp. xii

External Referees (PDF)

pp. xiii

Conference Chairs (PDF)

pp. xiv

Keynote Talk 1

Towards the Formal Verification of a C0 Compiler: Code Generation and Implementation Correctnes (Abstract)

Dirk Leinenbach, Saarland University, Germany

Wolfgang Paul, Saarland University, Germany

Elena Petrova, Saarland University, Germany

pp. 2-12

PDF

Testing

Use of Verification for Testing and Debugging of Complex Reactive Systems (Abstract)

Mark Trakhtenbrot, Holon Academic Institute of Technology, Israel

pp. 13-22

PDF

EXPERIMENTAL EVALUATION OF FSM-BASED TESTING METHODS (Abstract)

Rita Dorofeeva, Tomsk State University, Russia

Nina Yevtushenko, Tomsk State University, Russia

Khaled El-Fakih, American University of Sharjah, UAE

Ana R. Cavalli, Institut National des Telecommunications, France

pp. 23-32

PDF

Putting Detectors in Their Place (Abstract)

Arshad Jhumka, University of Warwick, Coventry, UK

Martin Hiller, Volvo Technological Department, Gothenburg, Sweden

pp. 33-43

PDF

Real-Time Systems

Timed Automata with Data Structures for Distributed Systems Design and Analysis (Abstract)

Ruggero Lanotte, Universita dell Insubria

Andrea Maggiolo-Schettini, Universita di Pisa

Angelo Troina, Universita di Pisa

pp. 44-53

PDF

Operational Semantics for Real-Time Processes with Action Refinement (Abstract)

Xiuli Sun, Chinese Academy of Sciences, China

Jinzhao Wu, Universitat Mannheim, Germany

pp. 54-63

PDF

Specifying Urgency in Timed I/O Automata (Abstract)

Biniam Gebremichael, Radboud University Nijmegen, The Netherlands

Frits Vaandrager, Radboud University Nijmegen, The Netherlands

pp. 64-74

PDF

Keynote Talk 2

A Cloverleaf of Software Engineering (Abstract)

Dines Bjorner, National University of Singapore

pp. 75-85

PDF

Static Analysis

Precise Analysis of Memory Consumption using Program Logics (Abstract)

Gilles Barthe, INRIA Sophia-Antipolis, France

Mariela Pavlova, INRIA Sophia-Antipolis, France

Gerardo Schneider, University of Oslo, Norway

pp. 86-95

PDF

Using Dominators to Extract Observable Protocol Contexts (Abstract)

Mahadevan Subramaniam, University of Nebraska at Omaha

Jiangfan Shi, University of Nebraska at Omaha

pp. 96-105

PDF

Counting Interface Automata and their Application in Static Analysis of Actor Models (Abstract)

Ernesto Wandeler, Ernesto Wandeler

Jorn W. Janneck, Jorn W. Janneck

Edward A. Lee, Edward A.

Lothar Thiele, Lothar Thiele

pp. 106-116

PDF

Requirements and Specification

Generating Relational Database Transactions From Recursive Functions Defined on EB^3 Traces (Abstract)

Frederic Gervais, Universite de Sherbrooke, Canada

Marc Frappier, Universite de Sherbrooke, Canada

Regine Laleau, LACL, Universite Paris 12, France

pp. 117-126

PDF

Workflow Enactment Based on a Chemical Metaphor (Abstract)

Zsolt Nemeth, MTA SZTAKI Computer and Automation Research Institute, Hungary

Christian Perez, IRISA, Campus Universitaire de Beaulieu,Cedex,France

Thierry Priol, IRISA, Campus Universitaire de Beaulieu,Cedex,France

pp. 127-136

PDF

Safe Concurrency for Aggregate Objects with Invariants (Abstract)

Bart Jacobs, Katholieke Universiteit Leuven Celestijnenlaan, Belgium

K. Rustan M. Leino, Microsoft Research, Redmond, WA., USA

Frank Piessens, Katholieke Universiteit Leuven Celestijnenlaan, Belgium

Wolfram Schulte, Microsoft Research, Redmond, WA., USA

pp. 137-147

PDF

Keynote Talk 3

Invariants on Demand (Abstract)

K. Rustan M. Leino, Microsoft Research, Redmond, WA, USA

pp. 148-149

PDF

Program Verification

Omnibus Verification Policies: A flexible, configurable approach to assertion-based software verification (Abstract)

Thomas Wilson, University of Stirling, Scotland

Savi Maharaj, University of Stirling, Scotland

Robert G. Clark, University of Stirling, Scotland

pp. 150-159

PDF

Proving Correctness of JavaCard DL Taclets using Bali (Abstract)

Kerry Trentelman, RSISE, Australian National University

pp. 160-169

PDF

Object Oriented Verification Kernels for Secure Java Applications (Abstract)

Holger Grandy, Universitat Augsburgm, Germany

Kurt Stenzel, Universitat Augsburgm, Germany

Wolfgang Reif, Universitat Augsburgm, Germany

pp. 170-179

PDF

Customised Induction Rules for Proving Correctness of Imperative Programs (Abstract)

Ola Olsson, Goteborg University, Sweden

Angela Wallenburg, Goteborg University, Sweden

pp. 180-189

PDF

A case study of C source code verification: the Schorr-Waite algorithm (Abstract)

Thierry Hubert, INRIA Futurs - Universite Paris, France

Claude Marche, INRIA Futurs - Universite Paris, France

pp. 190-199

PDF

Formal Verification of Dead Code Elimination in Isabelle/HOL (Abstract)

Jan Olaf Blech, University of Karlsruhe, Karlsruhe, Germany

Lars Gesellensetter, University of Karlsruhe, Karlsruhe, Germany

Sabine Glesner, University of Karlsruhe, Karlsruhe, Germany

pp. 200-209

PDF

Verification of an Off-Line Checker for Priority Queues (Abstract)

Hans De Nivelle, Max Planck Institut fur Informatik, Germany

Ruzica Piskac, Max Planck Institut fur Informatik, Germany

pp. 210-219

PDF

Building Verification Condition Generators by Compositional Extensions (Abstract)

I.S.W.B. Prasetya, Utrecht Univ

A. Azurat, Univ. Indonesia

T.E.J. Vos, Univ. Politecnica de Valencia

A. Van Leeuwen, Utrecht Univ.

pp. 220-230

PDF

True Concurrency

Towards A Truly Concurrent Model for Processes Sharing Resources (Abstract)

Naiyong Jin, East China Normal University, China

Jifeng He, United Nations University, Macau

pp. 231-239

PDF

A Proposal For Relative Time Petri Nets (Abstract)

Joseph Kuehn, University of Adelaide, Australia

Charles Lakos, University of Adelaide, Australia

Robert Esser, University of Adelaide, Australia

pp. 240-249

PDF

From RT-LOTOS to Time Petri Nets New Foundations for a Verification Platform (Abstract)

T. Sadani, ENSICA, Cedex, France

P. De Saqui-Sannes, ENSICA, Cedex, France

J.-P. Courtiat, LAAS-CNRS, Cedex, France

pp. 250-260

PDF

The FME Lecture (Keynote Talk 4)

Making Formal Methods Work (Abstract)

Anthony Hall, anthonyhall.org

pp. 261-262

PDF

Formal Methods for Maintenance and Change

On the Theory of Patching (Abstract)

Zoltan Pap, Budapest University of Technology, Hungary

Gyula Csopaki, Budapest University of Technology, Hungary

Sarolta Dibuz, Ericsson, Sweden

pp. 263-271

PDF

Pragmatic Consistency Management in Industrial Requirements Specifications (Abstract)

Jan Scheffczyk, Universitat der Bundeswehr Munchen

Uwe M. Borghoff, Universitat der Bundeswehr Munche

Andreas Birk, sd&m AG

Johannes Siedersleben, sd&m AG

pp. 272-281

PDF

Automatic Maintenance of Association Invariants (Abstract)

James Welch, Oxford University, UK

David Faitelson, Oxford University, UK

Jim Davies, Oxford University, UK

pp. 282-292

PDF

Keynote Talk 5

A Framework for Component-based Construction Extended Abstract (Abstract)

Joseph Sifakis, VERIMAG Laboratory, France

pp. 293-300

PDF

Abstraction

Control Code Obfuscation by Abstract Interpretation (Abstract)

Mila Dalla Preda, Universita di Verona, Italy

Roberto Giacobazzi, Universita di Verona, Italy

pp. 301-310

PDF

Stuttering Abstraction for Model Checkin (Abstract)

Shiva Nejati, University of Toronto, Canada

Arie Gurfinkel, University of Toronto, Canada

Marsha Chechik, University of Toronto, Canada

pp. 311-320

PDF

Description Logics for Shape Analysis (Abstract)

Lilia Georgieva, Heriot-Watt University, Edinburgh, UK

Patrick Maier, Max-Planck-Institut fur Informatik, Germany

pp. 321-331

PDF

Human-Computer Interaction

Formalising Control in Robust Spoken Dialogue Systems (Abstract)

Hui Shi, Universitat Bremen, Germany

Robert J. Ross, Universitat Bremen, Germany

John Bateman, Universitat Bremen, Germany

pp. 332-341

PDF

A unified description formalism for complex HCI-systems (Abstract)

Anke Dittmar, Rostock University, Germany

Peter Forbrig, Rostock University, Germany

pp. 342-351

PDF

Formal Analysis of Human-computer Interaction using Model-checking (Abstract)

Antonio Cerone, United Nations University Macau SAR China

Peter A. Lindsay, University of Queensland Brisbane, Australia

Simon Connelly, University of Queensland Brisbane, Australia

pp. 352-362

PDF

Tools and Practice

Software Refinement with Perfect Developer (Abstract)

Gareth Carter, National University of Ireland, Maynooth

Rosemary Monahan, National University of Ireland, Maynooth

Joseph M. Morris, Dublin City University

pp. 363-373

PDF

BRILLANT : An Open Source and XML-based platform for Rigourous Software Development (Abstract)

Samuel Colin, Universite de Valenciennes, Cedex, France

Dorian Petit, Universite de Valenciennes, Cedex, France

Vincent Poirriez, Universite de Valenciennes, Cedex, France

Jerome Rocheteau, INRETS-ESTAS, France

Rafael Marcano, INRETS-ESTAS, France

Georges Mariano, INRETS-ESTAS, France

pp. 373-382

PDF

Logical Foundations of Program Assertions: What do Practitioners Want? (Abstract)

Patrice Chalin, Concordia University, Canada

pp. 383-393

PDF

Component-Based Development

On Compatibility and Behavioural Substitutability of Component Protocols (Abstract)

Nabil Hameurlain, LIUPPA Laboratory, University of Pau, France

pp. 394-403

PDF

A Strategy for the Formal Composition of Frameworks (Abstract)

Walter Mesquita, Universidade Federal de Pernambuco, Brazil

Augusto Sampaio, Universidade Federal de Pernambuco, Brazil

Ana C. V. De Melo, Universidade de Sao Paulo, Brazil

pp. 404-413

PDF

Interface Abstraction for Compositional Verificatio (Abstract)

Dilian Gurov, Royal Institute of Technology Kista, Swede

Marieke Huisman, INRIA Sophia Antipolis Sophia Antipolis, France

pp. 414-424

PDF

Quality of Service

SHReQ: Coordinating Application Level QoS (Abstract)

Dan Hirsch, Universita di Pisa, Italy

Emilio Tuosto, Universita di Pisa, Italy

pp. 425-434

PDF

A Synchronous Process Calculus for Service Costs (Abstract)

Siva Anantharaman, LIFO - Universite d' Orleans, France

Jing Chen, LIFO - Universite d' Orleans, France

Gaetan Hains, LIFO - Universite d' Orleans, France

pp. 435-444

PDF

Author Index

Author Index (PDF)

pp. 445