Formal Methods and Software Engineering [electronic resource] : 14th International Conference on Formal Engineering Methods, ICFEM 2012, Kyoto, Japan, November 12-16, 2012. Proceedings / edited by Toshiaki Aoki, Kenji Taguchi.

Toward Practical Application of Formal Methods in Software Lifecycle Processes -- Formal Methods in the Aerospace Industry: Follow the Money -- Applying Term Rewriting to Speech Recognition of Numbers -- Variable Permissions for Concurrency Verification -- A Concurrent Temporal Programming Model with Atomic Blocks -- A Composable Mixed Mode Concurrency Control Semantics for Transactional Programs -- Towards a Formal Verification Methodology for Collective Robotic Systems -- Modeling Resource-Aware Virtualized Applications for the Cloud in Real-Time ABS -- Specification and Model Checking of the Chandy and Lamport Distributed Snapshot Algorithm in Rewriting Logic -- Quantitative Program Dependence Graphs -- Quantitative Analysis of Information Flow Using Theorem Proving -- Modeling and Verification of Probabilistic Actor Systems Using pRebeca -- Modular Verification of OO Programs with Interfaces -- Separation Predicates: A Taste of Separation Logic in First-Order Logic -- The Confinement Problem in the Presence of Faults -- Verification of ATL Transformations Using Transformation Models and Model Finders -- Automatic Generation of Provably Correct Embedded Systems -- Complementary Methodologies for Developing Hybrid Systems with Event-B -- A Temporal Logic with Mean-Payoff Constraints -- Time Constraints with Temporal Logic Programming -- Stepwise Satisfiability Checking Procedure for Reactive System Specifications by Tableau Method and Proof System -- Equational Abstraction Refinement for Certified Tree Regular Model Checking -- SMT-Based False Positive Elimination in Static Program Analysis -- Predicate Analysis with Block-Abstraction Memoization -- Heuristic-Guided Abstraction Refinement for Concurrent Systems -- More Anti-chain Based Refinement Checking -- An Analytical and Experimental Comparison of CSP Extensions and Tools -- Symbolic Model-Checking of Stateful Timed CSP Using BDD and Digitization -- Annotations for Alloy: Automated Incremental Analysis Using Domain Specific Solvers -- State Space c-Reductions of Concurrent Systems in Rewriting Logic -- A Practical Loop Invariant Generation Approach Based on Random Testing, Constraint Solving and Verification -- ConSMutate: SQL Mutants for Guiding Concolic Testing of Database Applications -- Demonic Testing of Concurrent Programs -- Towards Certified Runtime Verification.