Formal Methods and Software Engineering 6th International Conference on Formal Engineering Methods, ICFEM 2004, Seattle, WA, USA, November 8-12, 2004, Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Davies, Jim (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Schulte, Wolfram (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Barnett, Mike (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2004.
• Έκδοση: 1st ed. 2004.
• Σειρά: Lecture Notes in Computer Science, 3308
• Θέματα: Software engineering.; Computer logic.; Programming languages (Electronic computers).; Software Engineering/Programming and Operating Systems.; Software Engineering.; Logics and Meanings of Programs.; Programming Languages, Compilers, Interpreters.

Formal engineering methods are changing the way that software systems are - veloped.Withlanguageandtoolsupport,theyarebeingusedforautomaticcode generation, and for the automatic abstraction and checking of implementations. In the future, they will be used at every stage of development: requirements,...

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

• Tutorials
• Model-Based Development: Combining Engineering Approaches and Formal Techniques
• Tutorial on the RAISE Language, Method and Tools
• Model-Based Testing with Spec#
• Formal Engineering for Industrial Software Development - An Introduction to the SOFL Specification Language and Method
• Tutorial: Software Model Checking
• Invited Talks
• Engineering Quality Software
• When Can Formal Methods Make a Real Difference?
• On the Adoption of Formal Methods by Industry: The ACL2 Experience
• A CLP Approach to Modelling Systems
• Full Papers
• Multi-prover Verification of C Programs
• Memory-Model-Sensitive Data Race Analysis
• Formal Models for Web Navigations with Session Control and Browser Cache
• Managing Verification Activities Using SVM
• A General Model for Reachability Testing of Concurrent Programs
• A Knowledge Based Analysis of Cache Coherence
• A Propositional Logic-Based Method for Verification of Feature Models
• Deriving Probabilistic Semantics Via the 'Weakest Completion'
• CSP Representation of Game Semantics for Second-Order Idealized Algol
• An Equational Calculus for Alloy
• Guiding Spin Simulation
• Linear Inequality LTL (iLTL): A Model Checker for Discrete Time Markov Chains
• Software Model Checking Using Linear Constraints
• Counterexample Guided Abstraction Refinement Via Program Execution
• Faster Analysis of Formal Specifications
• Bridging Refinement of Interface Automata to Forward Simulation of I/O Automata
• Learning to Verify Safety Properties
• Automatic Extraction of Object-Oriented Observer Abstractions from Unit-Test Executions
• A Specification-Based Approach to Testing Polymorphic Attributes
• From Circus to JCSP
• An Approach to Preserve Protocol Consistency and Executability Across Updates
• A Formal Monitoring-Based Framework for Software Development and Analysis
• Verifying a File System Implementation
• Verifying the On-line Help System of SIEMENS Magnetic Resonance Tomographs
• Implementing Dynamic Aggregations of Abstract Machines in the B Method
• Formal Proof from UML Models
• Interactive Verification of UML State Machines
• Refinement of Actions for Real-Time Concurrent Systems with Causal Ambiguity
• From Durational Specifications to TLA Designs of Timed Automata
• Timed Patterns: TCOZ to Timed Automata.