Integrated Formal Methods 4th International Conference, IFM 2004, Cnaterbury, UK, April 4-7, 2004. Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Boiten, Eerke A. (Επιμελητής έκδοσης), Derrick, John (Επιμελητής έκδοσης), Smith, Graeme (Επιμελητής έκδοσης)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg, 2004.
• Σειρά: Lecture Notes in Computer Science, 2999
• Θέματα: Computer science.; Computer programming.; Software engineering.; Programming languages (Electronic computers).; Computers.; Computer logic.; Computer Science.; Theory of Computation.; Logics and Meanings of Programs.; Programming Techniques.; Software Engineering.; Programming Languages, Compilers, Interpreters.

The fourth conference in the series of international meetings on Integrated F- mal Methods, IFM, was held in Canterbury, UK, 4–7 April 2004. The conference was organized by the Computing Laboratory at the University of Kent, whose main campus is just outside the ancient town of Canterbury, part of t...

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

• Invited Talks
• SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft
• Design Verification for Control Engineering
• Integrating Model Checking and Theorem Proving in a Reflective Functional Language
• Tutorial
• A Tutorial Introduction to Designs in Unifying Theories of Programming
• Contributed Papers
• An Integration of Program Analysis and Automated Theorem Proving
• Verifying Controlled Components
• Efficient CSP Z Data Abstraction
• State/Event-Based Software Model Checking
• Formalising Behaviour Trees with CSP
• Generating MSCs from an Integrated Formal Specification Language
• UML to B: Formal Verification of Object-Oriented Models
• Software Verification with Integrated Data Type Refinement for Integer Arithmetic
• Constituent Elements of a Correctness-Preserving UML Design Approach
• Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption
• Linking CSP-OZ with UML and Java: A Case Study
• Object-Oriented Modelling with High-Level Modular Petri Nets
• Specification and Verification of Synchronizing Concurrent Objects
• Understanding Object-Z Operations as Generalised Substitutions
• Embeddings of Hybrid Automata in Process Algebra
• An Optimal Approach to Hardware/Software Partitioning for Synchronous Model
• A Many-Valued Logic with Imperative Semantics for Incremental Specification of Timed Models
• Integrating Temporal Logics
• Integration of Specification Languages Using Viewpoints
• Integrating Formal Methods by Unifying Abstractions
• Formally Justifying User-Centred Design Rules: A Case Study on Post-completion Errors
• Using UML Sequence Diagrams as the Basis for a Formal Test Description Language
• Viewpoint-Based Testing of Concurrent Components
• A Method for Compiling and Executing Expressive Assertions.