default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID3rd SEFM 2005: Koblenz, Germany
- Bernhard K. Aichernig, Bernhard Beckert:
Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), 7-9 September 2005, Koblenz, Germany. IEEE Computer Society 2005, ISBN 0-7695-2435-4
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 EB3 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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-12-13 19:00 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
