Integrated formal methods : 4th International Conference, IFM 2004, Cnaterbury, UK, April 4-7, 2004 : proceedings
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...
保存先:
| 第一著者: | |
|---|---|
| 団体著者: | |
| その他の著者: | , |
| フォーマット: | Livre numérique |
| 言語: | Anglais |
| 出版事項: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| シリーズ: | Lecture notes in computer science
2999 |
| 主題: | |
| オンライン･アクセス: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| 注記: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • Integrated formal methods, 4th international conference, IFM 2004, Canterbury, UK, April 4-7, 2004, proceedings, Eerke A. Boiten, John Derrick, Graeme Smith (eds.), Berlin, Springer, 2004, 1 vol. (XI-540 p.), Lecture notes in computer science, 3-540-21377-5 • Integrated Formal Methods, Texte imprimé, 9783662170496 |
目次:
- 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.