The Community for Technology Leaders
Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05) (2005)
Koblenz, Germany
Sept. 7, 2005 to Sept. 9, 2005
ISBN: 0-7695-2435-4
TABLE OF CONTENTS
Papers

Preface (PDF)

pp. x

External referees (PDF)

pp. xiii
Cover
Introduction
Keynote Talk 1

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

Elena Petrova , Saarland University, Germany
Wolfgang Paul , Saarland University, Germany
Dirk Leinenbach , Saarland University, Germany
pp. 2-12
Testing

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

Mark Trakhtenbrot , Holon Academic Institute of Technology, Israel
pp. 13-22

EXPERIMENTAL EVALUATION OF FSM-BASED TESTING METHODS (Abstract)

Rita Dorofeeva , Tomsk State University, Russia
Khaled El-Fakih , American University of Sharjah, UAE
Ana R. Cavalli , Institut National des Telecommunications, France
Nina Yevtushenko , Tomsk State University, Russia
pp. 23-32

Putting Detectors in Their Place (Abstract)

Martin Hiller , Volvo Technological Department, Gothenburg, Sweden
Arshad Jhumka , University of Warwick, Coventry, UK
pp. 33-43
Real-Time Systems

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

Jinzhao Wu , Universitat Mannheim, Germany
Xiuli Sun , Chinese Academy of Sciences, China
pp. 54-63

Specifying Urgency in Timed I/O Automata (Abstract)

Frits Vaandrager , Radboud University Nijmegen, The Netherlands
Biniam Gebremichael , Radboud University Nijmegen, The Netherlands
pp. 64-74
Keynote Talk 2

A Cloverleaf of Software Engineering (Abstract)

Dines Bjorner , National University of Singapore
pp. 75-85
Static Analysis

Precise Analysis of Memory Consumption using Program Logics (Abstract)

Gerardo Schneider , University of Oslo, Norway
Gilles Barthe , INRIA Sophia-Antipolis, France
Mariela Pavlova , INRIA Sophia-Antipolis, France
pp. 86-95

Using Dominators to Extract Observable Protocol Contexts (Abstract)

Jiangfan Shi , University of Nebraska at Omaha
Mahadevan Subramaniam , University of Nebraska at Omaha
pp. 96-105
Requirements and Specification

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

Marc Frappier , Universite de Sherbrooke, Canada
Regine Laleau , LACL, Universite Paris 12, France
Frederic Gervais , Universite de Sherbrooke, Canada
pp. 117-126

Workflow Enactment Based on a Chemical Metaphor (Abstract)

Christian Perez , IRISA, Campus Universitaire de Beaulieu,Cedex,France
Thierry Priol , IRISA, Campus Universitaire de Beaulieu,Cedex,France
Zsolt Nemeth , MTA SZTAKI Computer and Automation Research Institute, Hungary
pp. 127-136

Safe Concurrency for Aggregate Objects with Invariants (Abstract)

Frank Piessens , Katholieke Universiteit Leuven Celestijnenlaan, Belgium
Wolfram Schulte , Microsoft Research, Redmond, WA., USA
Bart Jacobs , Katholieke Universiteit Leuven Celestijnenlaan, Belgium
K. Rustan M. Leino , Microsoft Research, Redmond, WA., USA
pp. 137-147
Keynote Talk 3

Invariants on Demand (Abstract)

K. Rustan M. Leino , Microsoft Research, Redmond, WA, USA
pp. 148-149
Program Verification

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

Robert G. Clark , University of Stirling, Scotland
Savi Maharaj , University of Stirling, Scotland
Thomas Wilson , University of Stirling, Scotland
pp. 150-159

Proving Correctness of JavaCard DL Taclets using Bali (Abstract)

Kerry Trentelman , RSISE, Australian National University
pp. 160-169

Object Oriented Verification Kernels for Secure Java Applications (Abstract)

Wolfgang Reif , Universitat Augsburgm, Germany
Holger Grandy , Universitat Augsburgm, Germany
Kurt Stenzel , Universitat Augsburgm, Germany
pp. 170-179

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

Angela Wallenburg , Goteborg University, Sweden
Ola Olsson , Goteborg University, Sweden
pp. 180-189

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

Claude Marche , INRIA Futurs - Universite Paris, France
Thierry Hubert , INRIA Futurs - Universite Paris, France
pp. 190-199

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

Jan Olaf Blech , University of Karlsruhe, Karlsruhe, Germany
Sabine Glesner , University of Karlsruhe, Karlsruhe, Germany
Lars Gesellensetter , University of Karlsruhe, Karlsruhe, Germany
pp. 200-209

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

Ruzica Piskac , Max Planck Institut fur Informatik, Germany
Hans De Nivelle , Max Planck Institut fur Informatik, Germany
pp. 210-219

Building Verification Condition Generators by Compositional Extensions (Abstract)

T.E.J. Vos , Univ. Politecnica de Valencia
I.S.W.B. Prasetya , Utrecht Univ
A. Van Leeuwen , Utrecht Univ.
A. Azurat , Univ. Indonesia
pp. 220-230
True Concurrency

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

Jifeng He , United Nations University, Macau
Naiyong Jin , East China Normal University, China
pp. 231-239

A Proposal For Relative Time Petri Nets (Abstract)

Charles Lakos , University of Adelaide, Australia
Robert Esser , University of Adelaide, Australia
Joseph Kuehn , University of Adelaide, Australia
pp. 240-249

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

T. Sadani , ENSICA, Cedex, France
J.-P. Courtiat , LAAS-CNRS, Cedex, France
P. De Saqui-Sannes , ENSICA, Cedex, France
pp. 250-260
The FME Lecture (Keynote Talk 4)

Making Formal Methods Work (Abstract)

Anthony Hall , anthonyhall.org
pp. 261-262
Formal Methods for Maintenance and Change

On the Theory of Patching (Abstract)

Zoltan Pap , Budapest University of Technology, Hungary
Sarolta Dibuz , Ericsson, Sweden
Gyula Csopaki , Budapest University of Technology, Hungary
pp. 263-271

Pragmatic Consistency Management in Industrial Requirements Specifications (Abstract)

Jan Scheffczyk , Universitat der Bundeswehr Munchen
Andreas Birk , sd&m AG
Uwe M. Borghoff , Universitat der Bundeswehr Munche
pp. 272-281

Automatic Maintenance of Association Invariants (Abstract)

James Welch , Oxford University, UK
Jim Davies , Oxford University, UK
David Faitelson , Oxford University, UK
pp. 282-292
Keynote Talk 5
Abstraction

Control Code Obfuscation by Abstract Interpretation (Abstract)

Mila Dalla Preda , Universita di Verona, Italy
Roberto Giacobazzi , Universita di Verona, Italy
pp. 301-310

Stuttering Abstraction for Model Checkin (Abstract)

Shiva Nejati , University of Toronto, Canada
Marsha Chechik , University of Toronto, Canada
Arie Gurfinkel , University of Toronto, Canada
pp. 311-320

Description Logics for Shape Analysis (Abstract)

Lilia Georgieva , Heriot-Watt University, Edinburgh, UK
Patrick Maier , Max-Planck-Institut fur Informatik, Germany
pp. 321-331
Human-Computer Interaction

Formalising Control in Robust Spoken Dialogue Systems (Abstract)

Robert J. Ross , Universitat Bremen, Germany
Hui Shi , Universitat Bremen, Germany
John Bateman , Universitat Bremen, Germany
pp. 332-341

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

Peter Forbrig , Rostock University, Germany
Anke Dittmar , Rostock University, Germany
pp. 342-351

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

Peter A. Lindsay , University of Queensland Brisbane, Australia
Simon Connelly , University of Queensland Brisbane, Australia
Antonio Cerone , United Nations University Macau SAR China
pp. 352-362
Tools and Practice

Software Refinement with Perfect Developer (Abstract)

Rosemary Monahan , National University of Ireland, Maynooth
Gareth Carter , National University of Ireland, Maynooth
Joseph M. Morris , Dublin City University
pp. 363-373

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

Georges Mariano , INRETS-ESTAS, France
Rafael Marcano , INRETS-ESTAS, France
Samuel Colin , Universite de Valenciennes, Cedex, France
Jerome Rocheteau , INRETS-ESTAS, France
Vincent Poirriez , Universite de Valenciennes, Cedex, France
Dorian Petit , Universite de Valenciennes, Cedex, France
pp. 373-382
Component-Based Development

On Compatibility and Behavioural Substitutability of Component Protocols (Abstract)

Nabil Hameurlain , LIUPPA Laboratory, University of Pau, France
pp. 394-403

A Strategy for the Formal Composition of Frameworks (Abstract)

Augusto Sampaio , Universidade Federal de Pernambuco, Brazil
Ana C. V. De Melo , Universidade de Sao Paulo, Brazil
Walter Mesquita , Universidade Federal de Pernambuco, Brazil
pp. 404-413

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
Quality of Service

SHReQ: Coordinating Application Level QoS (Abstract)

Dan Hirsch , Universita di Pisa, Italy
Emilio Tuosto , Universita di Pisa, Italy
pp. 425-434

A Synchronous Process Calculus for Service Costs (Abstract)

Jing Chen , LIFO - Universite d' Orleans, France
Siva Anantharaman , LIFO - Universite d' Orleans, France
Gaetan Hains , LIFO - Universite d' Orleans, France
pp. 435-444
Author Index

Author Index (PDF)

pp. 445
90 ms
(Ver 3.3 (11022016))