Table of Contents

• Title Page [doi]
• Program Committee [doi]
• Conference Chairs [doi]
• Preface [doi]
• Copyright [doi]
• External Referees [doi]
• Steering Committee [doi]
• Towards the Formal Verification of a C0 Compiler: Code Generation and Implementation CorrectnesDirk Leinenbach, Wolfgang J. Paul, Elena Petrova. 2-12 [doi]
• Use of Verification for Testing and Debugging of Complex Reactive SystemsMark B. Trakhtenbrot. 13-22 [doi]
• Experimental Evaluation of FSM-Based Testing MethodsRita Dorofeeva, Nina Yevtushenko, Khaled El-Fakih, Ana R. Cavalli. 23-32 [doi]
• Putting Detectors in Their PlaceArshad Jhumka, Martin Hiller. 33-43 [doi]
• Timed Automata with Data Structures for Distributed Systems Design and AnalysisRuggero Lanotte, Andrea Maggiolo-Schettini, Angelo Troina. 44-53 [doi]
• Operational Semantics for Real-Time Processes with Action RefinementXiuli Sun, Jinzhao Wu. 54-63 [doi]
• Specifying Urgency in Timed I/O AutomataBiniam Gebremichael, Frits W. Vaandrager. 64-74 [doi]
• A Cloverleaf of Software EngineeringDines Bjørner. 75-85 [doi]
• Precise Analysis of Memory Consumption using Program LogicsGilles Barthe, Mariela Pavlova, Gerardo Schneider. 86-95 [doi]
• Using Dominators to Extract Observable Protocol ContextsMahadevan Subramaniam, Jiangfan Shi. 96-105 [doi]
• Counting Interface Automata and their Application in Static Analysis of Actor ModelsErnesto Wandeler, Jörn W. Janneck, Edward A. Lee, Lothar Thiele. 106-116 [doi]
• Generating Relational Database Transactions From Recursive Functions Defined on EB:::3::: TracesFrédéric Gervais, Marc Frappier, Régine Laleau. 117-126 [doi]
• Workflow Enactment Based on a Chemical MetaphorZsolt Németh, Christian Pérez, Thierry Priol. 127-136 [doi]
• Safe Concurrency for Aggregate Objects with InvariantsBart Jacobs 0002, Frank Piessens, K. Rustan M. Leino, Wolfram Schulte. 137-147 [doi]
• Invariants on DemandK. Rustan M. Leino. 148-149 [doi]
• Omnibus Verification Policies: A flexible, configurable approach to assertion-based software verificationThomas Wilson, Savi Maharaj, Robert G. Clark. 150-159 [doi]
• Proving Correctness of JavaCard DL Taclets using BaliKerry Trentelman. 160-169 [doi]
• Object Oriented Verification Kernels for Secure Java ApplicationsHolger Grandy, Kurt Stenzel, Wolfgang Reif. 170-179 [doi]
• Customised Induction Rules for Proving Correctness of Imperative ProgramsOla Olsson, Angela Wallenburg. 180-189 [doi]
• A case study of C source code verification: the Schorr-Waite algorithmThierry Hubert, Claude Marché. 190-199 [doi]
• Formal Verification of Dead Code Elimination in Isabelle/HOLJan Olaf Blech, Lars Gesellensetter, Sabine Glesner. 200-209 [doi]
• Verification of an Off-Line Checker for Priority QueuesHans de Nivelle, Ruzica Piskac. 210-219 [doi]
• Building Verification Condition Generators by Compositional ExtensionsI. S. W. B. Prasetya, A. Azurat, Tanja E. J. Vos, Arthur van Leeuwen. 220-230 [doi]
• Towards A Truly Concurrent Model for Processes Sharing ResourcesNaiyong Jin, Jifeng He. 231-239 [doi]
• A Proposal For Relative Time Petri NetsJoseph Kuehn, Charles Lakos, Robert Esser. 240-249 [doi]
• From RT-LOTOS to Time Petri Nets New Foundations for a Verification PlatformTarek Sadani, Pierre de Saqui-Sannes, Jean-Pierre Courtiat. 250-260 [doi]
• Making Formal Methods WorkAnthony Hall. 261-262 [doi]
• On the Theory of PatchingZoltán Pap, Gyula Csopaki, Sarolta Dibuz. 263-271 [doi]
• Pragmatic Consistency Management in Industrial Requirements SpecificationsJan Scheffczyk, Uwe M. Borghoff, Andreas Birk, Johannes Siedersleben. 272-281 [doi]
• Automatic Maintenance of Association InvariantsJames Welch, David Faitelson, Jim Davies. 282-292 [doi]
• A Framework for Component-based Construction Extended AbstractJoseph Sifakis. 293-300 [doi]
• Control Code Obfuscation by Abstract InterpretationMila Dalla Preda, Roberto Giacobazzi. 301-310 [doi]
• Stuttering Abstraction for Model CheckinShiva Nejati, Arie Gurfinkel, Marsha Chechik. 311-320 [doi]
• Description Logics for Shape AnalysisLilia Georgieva, Patrick Maier. 321-331 [doi]
• Formalising Control in Robust Spoken Dialogue SystemsHui Shi, Robert J. Ross, John A. Bateman. 332-341 [doi]
• A unified description formalism for complex HCI-systemsAnke Dittmar, Peter Forbrig. 342-351 [doi]
• Formal Analysis of Human-computer Interaction using Model-checkingAntonio Cerone, Peter A. Lindsay, Simon Connelly. 352-362 [doi]
• Software Refinement with Perfect DeveloperGareth Carter, Rosemary Monahan, Joseph M. Morris. 363-373 [doi]
• BRILLANT : An Open Source and XML-based platform for Rigourous Software DevelopmentSamuel Colin, Dorian Petit, Vincent Poirriez, Jérôme Rocheteau, Rafael Marcano, Georges Mariano. 373-382 [doi]
• Logical Foundations of Program Assertions: What do Practitioners Want?Patrice Chalin. 383-393 [doi]
• On Compatibility and Behavioural Substitutability of Component ProtocolsNabil Hameurlain. 394-403 [doi]
• A Strategy for the Formal Composition of FrameworksWalter Mesquita, Augusto Sampaio, Ana Cristina Vieira de Melo. 404-413 [doi]
• Interface Abstraction for Compositional VerificatioDilian Gurov, Marieke Huisman. 414-424 [doi]
• SHReQ: Coordinating Application Level QoSDan Hirsch, Emilio Tuosto. 425-434 [doi]
• A Synchronous Process Calculus for Service CostsSiva Anantharaman, Jing Chen, Gaétan Hains. 435-444 [doi]