FM 2006: Formal Methods: 14th International Symposium on Formal Methods, Hamilton, Canada, August 21-27, 2006, Proceedings

Front Cover
Jayadev Misra, Tobias Nipkow, Emil Sekerinski
Springer Science & Business Media, Aug 10, 2006 - Computers - 620 pages

This book presents the refereed proceedings of the 14th International Symposium on Formal Methods, FM 2006, held in Hamilton, Canada, August 2006. The book presents 36 revised full papers together with 2 invited contributions and extended abstracts of 7 invited industrial presentations, organized in topical sections on interactive verification, formal modelling of systems, real time, industrial experience, specification and refinement, programming languages, algebra, formal modelling of systems, and more.

 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

The Embedded Systems Design Challenge
1
Machine Checked Proofs for an Electronic Purse
16
Interactive Verification of Medical Guidelines
32
Certifying Airport Security Regulations Using the Focal Environment
48
A Case Study
64
Validating the Microsoft Hypervisor
81
Interface InputOutput Automata
82
Properties of Behavioural Model Merging
98
Resolution
364
A Fully General Operational Semantics for UML 20 Sequence Diagrams with Potential and Mandatory Choice
380
Towards Automatic Exception Safety Verification
396
Enforcer Efficient Failure Injection
412
Automated Boundary Test Generation from JML Specifications
428
Formal Reasoning About Nonatomic JAVA CARD Methods in Dynamic Logic
444
Formal Verification of a C Compiler FrontEnd
460
A Memory Model Sensitive Checker for C
476

Automatic Translation from Circus to Java
115
Quantitative Refinement and Model Checking for the Analysis of Probabilistic Systems
131
Modeling and Validating Distributed Embedded RealTime Systems with VDM
147
Towards Modularized Verification of Distributed TimeTriggered Systems
163
A Story About Formal Methods Adoption by a Railway Signaling Manufacturer
179
Case Studies Using a MetricsDriven Approach
190
Compositional Class Refinement in ObjectZ
205
A Proposal for Records in EventB
221
Pointfree Factorization of Operation Refinement
236
A Formal Template Language Enabling Metaproof
252
Support for Framing Dependencies and Sharing Without Restrictions
268
TypeSafe TwoLevel Data Transformation
284
Feature Algebra
300
Using DomainIndependent Problems for Introducing Formal Methods
316
Compositional Binding in Network Domains
332
Formal Modeling of Communication Protocols by Graph Transformation
348
Refactoring with Specifications
492
Mechanical Verification of Recursive Procedures Manipulating Pointers Using Separation Logic
508
ModelBased Variable and Transition Orderings for Efficient Symbolic Model Checking
524
Exact and Approximate Strategies for Symmetry Reduction in Model Checking
541
When an Efficient LTL Algorithm on Sequences Is Needed to ModelCheck Traces
557
PSL Model Checking and RunTime Verification Via Testers
573
Lightweight PlugIn or New Engineering Discipline
587
Exotic Flowers Thriving in an Expanding Niche
592
Deriving Secure Protocols
598
ModelBased Security Engineering for Real
600
Cost Effective Software Engineering for Security
607
Formal Methods and Cryptography
612
Verified Software Grand Challenge
617
Author Index
618
Copyright

Other editions - View all

Common terms and phrases

Bibliographic information