1. Home
  2. Proceedings
  3. SEFM
  4. SEFM 2005
Default Cover Image

Third IEEE International Conference on Software Engineering and Formal Methods

Sept. 7 2005 to Sept. 9 2005

Koblenz

Table of Contents

Papers
Steering CommitteeFreely available from IEEE.pp. xii
Introduction
Conference ChairsFreely available from IEEE.pp. xiv
PrefaceFreely available from IEEE.pp. x
External refereesFreely available from IEEE.pp. xiii-xiii
Towards the formal verification of a C0 compiler: code generation and implementation correctnessFreely available from IEEE.pp. 2-11
by D. Leinenbach, W. Paul, E. Petrova
Timed automata with data structures for distributed systems design and analysisFull-text access may be available. Sign in or learn about subscription options.pp. 44-53
by R. Lanotte, A. Maggiolo-Schettini, A. Troina
Testing
Use of Verification for Testing and Debugging of Complex Reactive SystemsFull-text access may be available. Sign in or learn about subscription options.pp. 13-22
by Mark Trakhtenbrot
Testing
EXPERIMENTAL EVALUATION OF FSM-BASED TESTING METHODSFull-text access may be available. Sign in or learn about subscription options.pp. 23-32
by Rita Dorofeeva, Nina Yevtushenko, Khaled El-Fakih, Ana R. Cavalli
Testing
Putting Detectors in Their PlaceFull-text access may be available. Sign in or learn about subscription options.pp. 33-43
by Arshad Jhumka, Martin Hiller
Real-Time Systems
Operational Semantics for Real-Time Processes with Action RefinementFull-text access may be available. Sign in or learn about subscription options.pp. 54-63
by Xiuli Sun, Jinzhao Wu
Real-Time Systems
Specifying Urgency in Timed I/O AutomataFull-text access may be available. Sign in or learn about subscription options.pp. 64-74
by Biniam Gebremichael, Frits Vaandrager
Keynote Talk 2
A cloverleaf of software engineeringFreely available from IEEE.pp. 75-84
by D. Bjoerner
Static Analysis
Precise Analysis of Memory Consumption using Program LogicsFull-text access may be available. Sign in or learn about subscription options.pp. 86-95
by Gilles Barthe, Mariela Pavlova, Gerardo Schneider
Static Analysis
Using Dominators to Extract Observable Protocol ContextsFull-text access may be available. Sign in or learn about subscription options.pp. 96-105
by Mahadevan Subramaniam, Jiangfan Shi
Static Analysis
Counting Interface Automata and their Application in Static Analysis of Actor ModelsFull-text access may be available. Sign in or learn about subscription options.pp. 106-116
by Ernesto Wandeler, Jorn W. Janneck, Edward A. Lee, Lothar Thiele
Requirements and Specification
Generating Relational Database Transactions From Recursive Functions Defined on EB^3 TracesFull-text access may be available. Sign in or learn about subscription options.pp. 117-126
by Frederic Gervais, Marc Frappier, Regine Laleau
Requirements and Specification
Workflow Enactment Based on a Chemical MetaphorFull-text access may be available. Sign in or learn about subscription options.pp. 127-136
by Zsolt Nemeth, Christian Perez, Thierry Priol
Requirements and Specification
Safe Concurrency for Aggregate Objects with InvariantsFull-text access may be available. Sign in or learn about subscription options.pp. 137-147
by Bart Jacobs, K. Rustan M. Leino, Frank Piessens, Wolfram Schulte
Program Verification
Omnibus Verification Policies: A flexible, configurable approach to assertion-based software verificationFull-text access may be available. Sign in or learn about subscription options.pp. 150-159
by Thomas Wilson, Savi Maharaj, Robert G. Clark
Program Verification
Proving Correctness of JavaCard DL Taclets using BaliFull-text access may be available. Sign in or learn about subscription options.pp. 160-169
by Kerry Trentelman
Program Verification
Object Oriented Verification Kernels for Secure Java ApplicationsFull-text access may be available. Sign in or learn about subscription options.pp. 170-179
by Holger Grandy, Kurt Stenzel, Wolfgang Reif
Program Verification
Customised Induction Rules for Proving Correctness of Imperative ProgramsFull-text access may be available. Sign in or learn about subscription options.pp. 180-189
by Ola Olsson, Angela Wallenburg
Program Verification
A case study of C source code verification: the Schorr-Waite algorithmFull-text access may be available. Sign in or learn about subscription options.pp. 190-199
by Thierry Hubert, Claude Marche
Program Verification
Formal Verification of Dead Code Elimination in Isabelle/HOLFull-text access may be available. Sign in or learn about subscription options.pp. 200-209
by Jan Olaf Blech, Lars Gesellensetter, Sabine Glesner
Program Verification
Verification of an Off-Line Checker for Priority QueuesFull-text access may be available. Sign in or learn about subscription options.pp. 210-219
by Hans De Nivelle, Ruzica Piskac
Program Verification
Building Verification Condition Generators by Compositional ExtensionsFull-text access may be available. Sign in or learn about subscription options.pp. 220-230
by I.S.W.B. Prasetya, A. Azurat, T.E.J. Vos, A. Van Leeuwen
True Concurrency
Towards A Truly Concurrent Model for Processes Sharing ResourcesFull-text access may be available. Sign in or learn about subscription options.pp. 231-239
by Naiyong Jin, Jifeng He
True Concurrency
A Proposal For Relative Time Petri NetsFull-text access may be available. Sign in or learn about subscription options.pp. 240-249
by Joseph Kuehn, Charles Lakos, Robert Esser
True Concurrency
From RT-LOTOS to Time Petri Nets New Foundations for a Verification PlatformFull-text access may be available. Sign in or learn about subscription options.pp. 250-260
by T. Sadani, P. De Saqui-Sannes, J.-P. Courtiat
The FME Lecture (Keynote Talk 4)
Making formal methods workFreely available from IEEE.pp. 261-261
by A. Hall
Formal Methods for Maintenance and Change
On the Theory of PatchingFull-text access may be available. Sign in or learn about subscription options.pp. 263-271
by Zoltan Pap, Gyula Csopaki, Sarolta Dibuz
Formal Methods for Maintenance and Change
Pragmatic Consistency Management in Industrial Requirements SpecificationsFull-text access may be available. Sign in or learn about subscription options.pp. 272-281
by Jan Scheffczyk, Uwe M. Borghoff, Andreas Birk, Johannes Siedersleben
Formal Methods for Maintenance and Change
Automatic Maintenance of Association InvariantsFull-text access may be available. Sign in or learn about subscription options.pp. 282-292
by James Welch, David Faitelson, Jim Davies
Keynote Talk 5
A Framework for Component-based Construction Extended AbstractFull-text access may be available. Sign in or learn about subscription options.pp. 293-300
by Joseph Sifakis
Abstraction
Control Code Obfuscation by Abstract InterpretationFull-text access may be available. Sign in or learn about subscription options.pp. 301-310
by Mila Dalla Preda, Roberto Giacobazzi
Abstraction
Stuttering Abstraction for Model CheckinFull-text access may be available. Sign in or learn about subscription options.pp. 311-320
by Shiva Nejati, Arie Gurfinkel, Marsha Chechik
Abstraction
Description Logics for Shape AnalysisFull-text access may be available. Sign in or learn about subscription options.pp. 321-331
by Lilia Georgieva, Patrick Maier
Human-Computer Interaction
Formalising Control in Robust Spoken Dialogue SystemsFull-text access may be available. Sign in or learn about subscription options.pp. 332-341
by Hui Shi, Robert J. Ross, John Bateman
Human-Computer Interaction
A unified description formalism for complex HCI-systemsFull-text access may be available. Sign in or learn about subscription options.pp. 342-351
by Anke Dittmar, Peter Forbrig
Human-Computer Interaction
Formal Analysis of Human-computer Interaction using Model-checkingFull-text access may be available. Sign in or learn about subscription options.pp. 352-362
by Antonio Cerone, Peter A. Lindsay, Simon Connelly
Tools and Practice
Software Refinement with Perfect DeveloperFull-text access may be available. Sign in or learn about subscription options.pp. 363-373
by Gareth Carter, Rosemary Monahan, Joseph M. Morris
Tools and Practice
BRILLANT : An Open Source and XML-based platform for Rigourous Software DevelopmentFull-text access may be available. Sign in or learn about subscription options.pp. 373-382
by Samuel Colin, Dorian Petit, Vincent Poirriez, Jerome Rocheteau, Rafael Marcano, Georges Mariano
Tools and Practice
Logical Foundations of Program Assertions: What do Practitioners Want?Full-text access may be available. Sign in or learn about subscription options.pp. 383-393
by Patrice Chalin
Component-Based Development
On Compatibility and Behavioural Substitutability of Component ProtocolsFull-text access may be available. Sign in or learn about subscription options.pp. 394-403
by Nabil Hameurlain
Component-Based Development
A Strategy for the Formal Composition of FrameworksFull-text access may be available. Sign in or learn about subscription options.pp. 404-413
by Walter Mesquita, Augusto Sampaio, Ana C. V. De Melo
Component-Based Development
Interface Abstraction for Compositional VerificatioFull-text access may be available. Sign in or learn about subscription options.pp. 414-424
by Dilian Gurov, Marieke Huisman
Quality of Service
SHReQ: Coordinating Application Level QoSFull-text access may be available. Sign in or learn about subscription options.pp. 425-434
by Dan Hirsch, Emilio Tuosto
Quality of Service
A Synchronous Process Calculus for Service CostsFull-text access may be available. Sign in or learn about subscription options.pp. 435-444
by Siva Anantharaman, Jing Chen, Gaetan Hains
Showing 48 out of 48