FM 2006: Formal Methods 14th International Symposium on Formal Methods, Hamilton, Canada, August 21-27, 2006. Proceedings /
| Συγγραφή απο Οργανισμό/Αρχή: | |
|---|---|
| Άλλοι συγγραφείς: | , , |
| Μορφή: | Ηλεκτρονική πηγή Ηλ. βιβλίο |
| Γλώσσα: | English |
| Έκδοση: |
Berlin, Heidelberg :
Springer Berlin Heidelberg,
2006.
|
| Σειρά: | Lecture Notes in Computer Science,
4085 |
| Θέματα: | |
| Διαθέσιμο Online: | Full Text via HEAL-Link |
Πίνακας περιεχομένων:
- 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 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 Circus to Java
- Quantitative Refinement 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 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.
