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)

Dirk Leinenbach , Saarland University, Germany
Wolfgang Paul , Saarland University, Germany
Elena Petrova , 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
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

Putting Detectors in Their Place (Abstract)

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

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

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
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)

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

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
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

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

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
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)

Thomas Wilson , University of Stirling, Scotland
Savi Maharaj , University of Stirling, Scotland
Robert G. Clark , 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)

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

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

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

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

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

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

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
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

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

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
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
Gyula Csopaki , Budapest University of Technology, Hungary
Sarolta Dibuz , Ericsson, Sweden
pp. 263-271

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
pp. 272-281

Automatic Maintenance of Association Invariants (Abstract)

James Welch , Oxford University, UK
David Faitelson , Oxford University, UK
Jim Davies , 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
Arie Gurfinkel , University of Toronto, Canada
Marsha Chechik , 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)

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

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

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

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
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

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
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)

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

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)

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

Author Index (PDF)

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