FM 2005: Formal Methods International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005. Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Fitzgerald, John (Επιμελητής έκδοσης), Hayes, Ian J. (Επιμελητής έκδοσης), Tarlecki, Andrzej (Επιμελητής έκδοσης)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg, 2005.
• Σειρά: Lecture Notes in Computer Science, 3582
• Θέματα: Computer science.; Computer programming.; Software engineering.; Programming languages (Electronic computers).; Computer logic.; Mathematical logic.; Management information systems.; Computer Science.; Software Engineering.; Logics and Meanings of Programs.; Programming Languages, Compilers, Interpreters.; Programming Techniques.; Mathematical Logic and Formal Languages.; Management of Computing and Information Systems.

This volume contains the proceedings of Formal Methods 2005, the 13th InternationalSymposiumonFormalMethodsheldinNewcastleuponTyne,UK, during July 18–22, 2005. Formal Methods Europe (FME, www.fmeurope.org) is an independent association which aims to stimulate the use of, and research on, formal meth...

Πίνακας περιεχομένων:

• Keynote Talks
• Formal Aids for the Growth of Software Systems
• Formal Methods and Testing: Hypotheses, and Correctness Approximations
• The Natural History of Bugs: Using Formal Methods to Analyse Software Related Failures in Space Missions
• Object Orientation
• Modular Verification of Static Class Invariants
• Decoupling in Object Orientation
• Controlling Object Allocation Using Creation Guards
• Symbolic Animation of JML Specifications
• Resource Analysis and Verification
• Certified Memory Usage Analysis
• Compositional Specification and Analysis of Cost-Based Properties in Probabilistic Programs
• Formally Defining and Verifying Master/Slave Speculative Parallelization
• Timing and Testing
• Systematic Implementation of Real-Time Models
• Timing Tolerances in Safety-Critical Software
• Timed Testing with TorX
• Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems
• CSP, B and Circus
• Adding Conflict and Confusion to CSP
• Combining CSP and B for Specification and Property Verification
• Operational Semantics for Model Checking Circus
• Control Law Diagrams in Circus
• Security
• Verification of a Signature Architecture with HOL-Z
• End-to-End Integrated Security and Performance Analysis on the DEGAS Choreographer Platform
• Formal Verification of Security Properties of Smart Card Embedded Source Code
• Networks and Processes
• A Formal Model of Addressing for Interoperating Networks
• An Approach to Unfolding Asynchronous Communication Protocols
• Semantics of BPEL4WS-Like Fault and Compensation Handling
• Abstraction, Retrenchment and Rewriting
• On Some Galois Connection Based Abstractions for the Mu-Calculus
• Retrenching the Purse: Finite Sequence Numbers, and the Tower Pattern
• Strategic Term Rewriting and Its Application to a Vdm-sl to Sql Conversion
• Scenarios and Modeling Languages
• Synthesis of Distributed Processes from Scenario-Based Specifications
• Verifying Scenario-Based Aspect Specifications
• An MDA Approach Towards Integrating Formal and Informal Modeling Languages
• Model Checking
• Model-Checking of Specifications Integrating Processes, Data and Time
• Automatic Symmetry Detection for Model Checking Using Computational Group Theory
• On Partitioning and Symbolic Model Checking
• Dynamic Component Substitutability Analysis
• Industry Day: Abstracts of Invited Talks
• Floating-Point Verification
• Preliminary Results of a Case Study: Model Checking for Advanced Automotive Applications
• Model-Based Testing in Practice
• Testing Concurrent Object-Oriented Systems with Spec Explorer
• ASD Case Notes: Costs and Benefits of Applying Formal Methods to Industrial Control Software
• The Informal Nature of Systems Engineering.