This book constitutes the refereed proceedings of the 12th InternationalConference on Formal Engineering Methods, ICFEM 2010, held in Shanghai, China,November 2010.The 42 revised full papers together with 3 invited talks presented were carefully reviewed and selected from 114 submissions.

Invited Talks.- Fostering Proof Scores in CafeOBJ.- Exploiting Partial Success in Applying Automated Formal Methods.- Multicore Embedded Systems: The Timing Problem and Possible Solutions.- Theorem Proving and Decision Procedures.- Applying PVS Background Theories and Proof Strategies in Invariant Based Programming.- Proof Obligation Generation and Discharging for Recursive Definitions in VDM.- Correct-by-Construction Model Transformations from Partially Ordered Specifications in Coq.- Decision Procedures for the Temporal Verification of Concurrent Lists.- An Improved Decision Procedure for Propositional Projection Temporal Logic.- Web Services and Workflow.- A Semantic Model for Service Composition with Coordination Time Delays.- Compensable WorkFlow Nets.- Automatically Testing Web Services Choreography with Assertions.- Applying Ordinary Differential Equations to the Performance Analysis of Service Composition.- Verification I.- Verifying Heap-Manipulating Programs with Unknown Procedure Calls.- API Conformance Verification for Java Programs.- Assume-Guarantee Reasoning with Local Specifications.- Automating Coinduction with Case Analysis.- Applications of Formal Methods.- Enhanced Semantic Access to Formal Software Models.- Making Pattern- and Model-Based Software Development More Rigorous.- Practical Parameterised Session Types.- A Formal Verification Study on the Rotterdam Storm Surge Barrier.- Verification II.- Formalization and Correctness of the PALS Architectural Pattern for Distributed Real-Time Systems.- Automated Multiparameterised Verification by Cut-Offs.- Automating Cut-off for Multi-parameterized Systems.- Method for Formal Verification of Soft-Error Tolerance Mechanisms in Pipelined Microprocessors.- Formal Verification of Tokeneer Behaviours Modelled in fUML Using CSP.- Probability and Concurrency.- Model Checking Hierarchical Probabilistic Systems.- Trace-Driven Verification of Multithreaded Programs.- Closed Form Approximations for Steady State Probabilities of a Controlled Fork-Join Network.- Reasoning about Safety and Progress Using Contracts.- Program Analysis.- Abstract Program Slicing: From Theory towards an Implementation.- Loop Invariant Synthesis in a Combined Domain.- Software Metrics in Static Program Analysis.- A Combination of Forward and Backward Reachability Analysis Methods.- Model Checking.- Model Checking a Model Checker: A Code Contract Combined Approach.- On Symmetries and Spotlights – Verifying Parameterised Systems.- A Methodology for Automatic Diagnosability Analysis.- Making the Right Cut in Model Checking Data-Intensive Timed Systems.- Comparison of Model Checking Tools for Information Systems.- Object Orientation and Model Driven Engineering.- A Modular Scheme for Deadlock Prevention in an Object-Oriented Programming Model.- Model-Driven Protocol Design Based on Component Oriented Modeling.- Laws of Pattern Composition.- Dynamic Resource Reallocation between Deployment Components.- Specification and Verification.- A Pattern System to Support Refining Informal Ideas into Formal Expressions.- Specification Translation of State Machines from Equational Theories into Rewrite Theories.- Alternating Interval Based Temporal Logics.