3. SEFM 2005: Koblenz, Germany

Cover

• Title Page.
  
• Copyright.
  

Introduction

• Preface.
  
• Program Committee.
  
• Steering Committee.
  
• External Referees.
  
• Conference Chairs.
  

Keynote Talk 1

• Dirk Leinenbach, Wolfgang J. Paul, Elena Petrova:
  Towards the Formal Verification of a C0 Compiler: Code Generation and Implementation Correctnes. 2-12
  

Testing

• Mark B. Trakhtenbrot:
  Use of Verification for Testing and Debugging of Complex Reactive Systems. 13-22
  
• Rita Dorofeeva, Nina Yevtushenko, Khaled El-Fakih, Ana R. Cavalli:
  Experimental Evaluation of FSM-Based Testing Methods. 23-32
  
• Arshad Jhumka, Martin Hiller:
  Putting Detectors in Their Place. 33-43
  

Real-Time Systems

• Ruggero Lanotte, Andrea Maggiolo-Schettini, Angelo Troina:
  Timed Automata with Data Structures for Distributed Systems Design and Analysis. 44-53
  
• Xiuli Sun, Jinzhao Wu:
  Operational Semantics for Real-Time Processes with Action Refinement. 54-63
  
• Biniam Gebremichael, Frits W. Vaandrager:
  Specifying Urgency in Timed I/O Automata. 64-74
  

Keynote Talk 2

• Dines Bjørner:
  A Cloverleaf of Software Engineering. 75-85
  

Static Analysis

• Gilles Barthe, Mariela Pavlova, Gerardo Schneider:
  Precise Analysis of Memory Consumption using Program Logics. 86-95
  
• Mahadevan Subramaniam, Jiangfan Shi:
  Using Dominators to Extract Observable Protocol Contexts. 96-105
  
• Ernesto Wandeler, Jörn W. Janneck, Edward A. Lee, Lothar Thiele:
  Counting Interface Automata and their Application in Static Analysis of Actor Models. 106-116
  

Requirements and Specification

• Frédéric Gervais, Marc Frappier, Régine Laleau:
  Generating Relational Database Transactions From Recursive Functions Defined on EB³ Traces. 117-126
  
• Zsolt Németh, Christian Pérez, Thierry Priol:
  Workflow Enactment Based on a Chemical Metaphor. 127-136
  
• Bart Jacobs, Frank Piessens, K. Rustan M. Leino, Wolfram Schulte:
  Safe Concurrency for Aggregate Objects with Invariants. 137-147
  

Keynote Talk 3

• K. Rustan M. Leino:
  Invariants on Demand. 148-149
  

Program Verification

• Thomas Wilson, Savi Maharaj, Robert G. Clark:
  Omnibus Verification Policies: A flexible, configurable approach to assertion-based software verification. 150-159
  
• Kerry Trentelman:
  Proving Correctness of JavaCard DL Taclets using Bali. 160-169
  
• Holger Grandy, Kurt Stenzel, Wolfgang Reif:
  Object Oriented Verification Kernels for Secure Java Applications. 170-179
  
• Ola Olsson, Angela Wallenburg:
  Customised Induction Rules for Proving Correctness of Imperative Programs. 180-189
  
• Thierry Hubert, Claude Marché:
  A case study of C source code verification: the Schorr-Waite algorithm. 190-199
  
• Jan Olaf Blech, Lars Gesellensetter, Sabine Glesner:
  Formal Verification of Dead Code Elimination in Isabelle/HOL. 200-209
  
• Hans de Nivelle, Ruzica Piskac:
  Verification of an Off-Line Checker for Priority Queues. 210-219
  
• I. S. W. B. Prasetya, A. Azurat, Tanja E. J. Vos, Arthur van Leeuwen:
  Building Verification Condition Generators by Compositional Extensions. 220-230
  

True Concurrency

• Naiyong Jin, Jifeng He:
  Towards A Truly Concurrent Model for Processes Sharing Resources. 231-239
  
• Joseph Kuehn, Charles Lakos, Robert Esser:
  A Proposal For Relative Time Petri Nets. 240-249
  
• Tarek Sadani, Pierre de Saqui-Sannes, Jean-Pierre Courtiat:
  From RT-LOTOS to Time Petri Nets New Foundations for a Verification Platform. 250-260
  

The FME Lecture (Keynote Talk 4)

• Anthony Hall:
  Making Formal Methods Work. 261-262
  

Formal Methods for Maintenance and Change

• Zoltán Pap, Gyula Csopaki, Sarolta Dibuz:
  On the Theory of Patching. 263-271
  
• Jan Scheffczyk, Uwe M. Borghoff, Andreas Birk, Johannes Siedersleben:
  Pragmatic Consistency Management in Industrial Requirements Specifications. 272-281
  
• James Welch, David Faitelson, Jim Davies:
  Automatic Maintenance of Association Invariants. 282-292
  

Keynote Talk 5

• Joseph Sifakis:
  A Framework for Component-based Construction Extended Abstract. 293-300
  

Abstraction

• Mila Dalla Preda, Roberto Giacobazzi:
  Control Code Obfuscation by Abstract Interpretation. 301-310
  
• Shiva Nejati, Arie Gurfinkel, Marsha Chechik:
  Stuttering Abstraction for Model Checkin. 311-320
  
• Lilia Georgieva, Patrick Maier:
  Description Logics for Shape Analysis. 321-331
  

Human-Computer Interaction

• Hui Shi, Robert J. Ross, John A. Bateman:
  Formalising Control in Robust Spoken Dialogue Systems. 332-341
  
• Anke Dittmar, Peter Forbrig:
  A unified description formalism for complex HCI-systems. 342-351
  
• Antonio Cerone, Peter A. Lindsay, Simon Connelly:
  Formal Analysis of Human-computer Interaction using Model-checking. 352-362
  

Tools and Practice

• Gareth Carter, Rosemary Monahan, Joseph M. Morris:
  Software Refinement with Perfect Developer. 363-373
  
• Samuel Colin, Dorian Petit, Vincent Poirriez, Jérôme Rocheteau, Rafael Marcano, Georges Mariano:
  BRILLANT : An Open Source and XML-based platform for Rigourous Software Development. 373-382
  
• Patrice Chalin:
  Logical Foundations of Program Assertions: What do Practitioners Want?. 383-393
  

Component-Based Development

• Nabil Hameurlain:
  On Compatibility and Behavioural Substitutability of Component Protocols. 394-403
  
• Walter Mesquita, Augusto Sampaio, Ana Cristina Vieira de Melo:
  A Strategy for the Formal Composition of Frameworks. 404-413
  
• Dilian Gurov, Marieke Huisman:
  Interface Abstraction for Compositional Verificatio. 414-424
  

Quality of Service

• Dan Hirsch, Emilio Tuosto:
  SHReQ: Coordinating Application Level QoS. 425-434
  
• Siva Anantharaman, Jing Chen, Gaétan Hains:
  A Synchronous Process Calculus for Service Costs. 435-444
  

Last update Mon Feb 13 04:40:16 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page