FM 2006: Formal Methods: 14th International Symposium on Formal Methods, Hamilton, Canada, August 21-27, 2006, Proceedings (Lecture Notes in Computer Science, 4085)

Frontmatter
Invited Talk
	The Embedded Systems Design Challenge
Interactive Verification
	The Mondex Challenge: Machine Checked Proofs for an Electronic Purse
	Interactive Verification of Medical Guidelines
	Certifying Airport Security Regulations Using the {\\sf Focal} Environment
	Proving Safety Properties of an Aircraft Landing Protocol Using I/O Automata and the PVS Theorem Prover: A Case Study
Invited Talk
	Validating the Microsoft Hypervisor
Formal Modelling of Systems
	Interface Input/Output Automata
	Properties of Behavioural Model Merging
	Automatic Translation from $<$Emphasis FontCategory={\\textquotedbl}SansSerif{\\textquotedbl} Type={\\textquotedbl}Italic{\\textquotedbl}$>$Circus$<$/Emphasis$>$ to Java
	Quantitative Refinement {\\itshape and} Model Checking for the Analysis of Probabilistic Systems
Real Time
	Modeling and Validating Distributed Embedded Real-Time Systems with VDM++
	Towards Modularized Verification of Distributed Time-Triggered Systems
Industrial Experience
	A Story About Formal Methods Adoption by a Railway Signaling Manufacturer
	Partially Introducing Formal Methods into Object-Oriented Development: Case Studies Using a Metrics-Driven Approach
Specification Refinement
	Compositional Class Refinement in Object-Z
	A Proposal for Records in Event-B
	Pointfree Factorization of Operation Refinement
	A Formal Template Language Enabling Metaproof
Progrmming Languages
	Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions
	Type-Safe Two-Level Data Transformation
Algebra
	Feature Algebra
Education
	Using Domain-Independent Problems for Introducing Formal Methods
Formal Modelling of Systems
	Compositional Binding in Network Domains
	Formal Modeling of Communication Protocols by Graph Transformation
	Feature Specification and Static Analysis for Interaction Resolution
	A Fully General Operational Semantics for UML~2.0 Sequence Diagrams with Potential and Mandatory Choice
Formal Aspects of Java
	Towards Automatic Exception Safety Verification
	Enforcer -- Efficient Failure Injection
	Automated Boundary Test Generation from JML Specifications
	Formal Reasoning About Non-atomic {\\sc Java Card} Methods in Dynamic Logic
Programming Languages
	Formal Verification of a C Compiler Front-End
	A Memory Model Sensitive Checker for C\\#
	Changing Programs Correctly: Refactoring with Specifications
	Mechanical Verification of Recursive Procedures Manipulating Pointers Using Separation Logic
Model Checking
	Model-Based Variable and Transition Orderings for Efficient Symbolic Model Checking
	Exact and Approximate Strategies for Symmetry Reduction in Model Checking
	Monitoring Distributed Controllers: When an Efficient LTL Algorithm on Sequences Is Needed to Model-Check Traces
	PSL Model Checking and Run-Time Verification Via Testers
Industry Day: Abstracts of Invited Talks
	Formal Methods for Security: Lightweight Plug-In or New Engineering Discipline
	Formal Methods in the Security Business: Exotic Flowers Thriving in an Expanding Niche
	Connector-Based Software Development: Deriving Secure Protocols
	Model-Based Security Engineering for Real
	Cost Effective Software Engineering for Security
	Formal Methods and Cryptography
	Verified Software Grand Challenge
Backmatter