Formal Methods and Software Engineering: 14th International Conference on Formal Engineering Methods, ICFEM 2012, Kyoto, Japan, November 12-16, 2012. Proceedings

✍ Scribed by Mario Tokoro (auth.), Toshiaki Aoki, Kenji Taguchi (eds.)

• Publisher: Springer-Verlag Berlin Heidelberg
• Year: 2012
• Tongue: English
• Leaves: 523
• Series: Lecture Notes in Computer Science 7635 Programming and Software Engineering
• Edition: 1
• Category: Library

✦ Synopsis

This book constitutes the refereed proceedings of the 14th International Conference on Formal Engineering Methods, ICFEM 2012, held in Kyoto, Japan, November 2012. The 31 revised full papers together with 3 invited talks presented were carefully reviewed and selected from 85 submissions. The papers address all current issues in formal methods and their applications in software engineering. They are organized in topical sections on concurrency, applications of formal methods to new areas, quantity and probability, formal verification, modeling and development methodology, temporal logics, abstraction and refinement, tools, as well as testing and runtime verification.

✦ Table of Contents

Front Matter....Pages -
Toward Practical Application of Formal Methods in Software Lifecycle Processes....Pages 1-1
Formal Methods in the Aerospace Industry: Follow the Money....Pages 2-3
Applying Term Rewriting to Speech Recognition of Numbers....Pages 4-4
Variable Permissions for Concurrency Verification....Pages 5-21
A Concurrent Temporal Programming Model with Atomic Blocks....Pages 22-37
A Composable Mixed Mode Concurrency Control Semantics for Transactional Programs....Pages 38-53
Towards a Formal Verification Methodology for Collective Robotic Systems....Pages 54-70
Modeling Resource-Aware Virtualized Applications for the Cloud in Real-Time ABS....Pages 71-86
Specification and Model Checking of the Chandy and Lamport Distributed Snapshot Algorithm in Rewriting Logic....Pages 87-102
Quantitative Program Dependence Graphs....Pages 103-118
Quantitative Analysis of Information Flow Using Theorem Proving....Pages 119-134
Modeling and Verification of Probabilistic Actor Systems Using pRebeca....Pages 135-150
Modular Verification of OO Programs with Interfaces....Pages 151-166
Separation Predicates: A Taste of Separation Logic in First-Order Logic....Pages 167-181
The Confinement Problem in the Presence of Faults....Pages 182-197
Verification of ATL Transformations Using Transformation Models and Model Finders....Pages 198-213
Automatic Generation of Provably Correct Embedded Systems....Pages 214-229
Complementary Methodologies for Developing Hybrid Systems with Event-B....Pages 230-248
A Temporal Logic with Mean-Payoff Constraints....Pages 249-265
Time Constraints with Temporal Logic Programming....Pages 266-282
Stepwise Satisfiability Checking Procedure for Reactive System Specifications by Tableau Method and Proof System....Pages 283-298
Equational Abstraction Refinement for Certified Tree Regular Model Checking....Pages 299-315
SMT-Based False Positive Elimination in Static Program Analysis....Pages 316-331
Predicate Analysis with Block-Abstraction Memoization....Pages 332-347
Heuristic-Guided Abstraction Refinement for Concurrent Systems....Pages 348-363
More Anti-chain Based Refinement Checking....Pages 364-380
An Analytical and Experimental Comparison of CSP Extensions and Tools....Pages 381-397
Symbolic Model-Checking of Stateful Timed CSP Using BDD and Digitization....Pages 398-413
Annotations for Alloy: Automated Incremental Analysis Using Domain Specific Solvers....Pages 414-429
State Space c-Reductions of Concurrent Systems in Rewriting Logic....Pages 430-446
A Practical Loop Invariant Generation Approach Based on Random Testing, Constraint Solving and Verification....Pages 447-461
ConSMutate: SQL Mutants for Guiding Concolic Testing of Database Applications....Pages 462-477
Demonic Testing of Concurrent Programs....Pages 478-493
Towards Certified Runtime Verification....Pages 494-509
Back Matter....Pages -

✦ Subjects

Software Engineering; Programming Techniques; Programming Languages, Compilers, Interpreters; Algorithm Analysis and Problem Complexity; Mathematical Logic and Formal Languages; Computer Communication Networks