Formal Methods and Software Engineering

1. Front Matter

   PDF

2. Invited Talks

   1. Fostering Proof Scores in CafeOBJ 

      • Kokichi Futatsugi

      Pages 1-20

   2. Exploiting Partial Success in Applying Automated Formal Methods

      • Matthew B. Dwyer

      Pages 21-21

   3. Multicore Embedded Systems: The Timing Problem and Possible Solutions

      • Wang Yi

      Pages 22-23

3. Theorem Proving and Decision Procedures

   1. Applying PVS Background Theories and Proof Strategies in Invariant Based Programming

      • Johannes Eriksson, Ralph-Johan Back

      Pages 24-39

   2. Proof Obligation Generation and Discharging for Recursive Definitions in VDM

      • Augusto Ribeiro, Peter Gorm Larsen

      Pages 40-55

   3. Correct-by-Construction Model Transformations from Partially Ordered Specifications in Coq

      • Iman Poernomo, Jeffrey Terrell

      Pages 56-73

   4. Decision Procedures for the Temporal Verification of Concurrent Lists

      • Alejandro Sánchez, César Sánchez

      Pages 74-89

   5. An Improved Decision Procedure for Propositional Projection Temporal Logic

      • Zhenhua Duan, Cong Tian

      Pages 90-105

4. Web Services and Workflow

   1. A Semantic Model for Service Composition with Coordination Time Delays

      • Natallia Kokash, Behnaz Changizi, Farhad Arbab

      Pages 106-121

   2. Compensable WorkFlow Nets

      • Fazle Rabbi, Hao Wang, Wendy MacCaull

      Pages 122-137

   3. Automatically Testing Web Services Choreography with Assertions

      • Lei Zhou, Jing Ping, Hao Xiao, Zheng Wang, Geguang Pu, Zuohua Ding

      Pages 138-154

   4. Applying Ordinary Differential Equations to the Performance Analysis of Service Composition

      • Zuohua Ding, Hui Shen, Jing Liu

      Pages 155-170

5. Verification I

   1. Verifying Heap-Manipulating Programs with Unknown Procedure Calls

      • Shengchao Qin, Chenguang Luo, Guanhua He, Florin Craciun, Wei-Ngan Chin

      Pages 171-187

   2. API Conformance Verification for Java Programs

      • Xin Li, H. James Hoover, Piotr Rudnicki

      Pages 188-203

   3. Assume-Guarantee Reasoning with Local Specifications

      • Alessio Lomuscio, Ben Strulo, Nigel Walker, Peng Wu

      Pages 204-219

   4. Automating Coinduction with Case Analysis

      • Eugen-Ioan Goriac, Dorel Lucanu, Grigore Roşu

      Pages 220-236

6. Applications of Formal Methods

   1. Enhanced Semantic Access to Formal Software Models

      • Hai H. Wang, Danica Damljanovic, Jing Sun

      Pages 237-252

   2. Making Pattern- and Model-Based Software Development More Rigorous

      • Denis Hatebur, Maritta Heisel

      Pages 253-269

   3. Practical Parameterised Session Types

      • Andi Bejleri

      Pages 270-286

This book constitutes the refereed proceedings of the 12th International
Conference 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. The papers address all current issues in formal methods and their applications in software engineering. They are organized in topical sections on theorem proving and decision procedures, web services and workflow, verification, applications of formal methods, probability and concurrency, program analysis, model checking, object orientation and mod
el driven engineering, as well as specification and verification.

• BPEL
• Web Services
• algebraic specification
• automata
• automated verification
• automatic translation
• behavioral specification
• bounded model checking
• case analysis
• combined domain
• component-based sysetms
• decision procedure
• equational theory
• software engineering
• verification
• algorithm analysis and problem complexity

• School of Computing, Computer Science Dept, National University of Singapore, Singapore, Singapore

  Jin Song Dong

• Software Engineering Institute, East China Normal University, Shanghai, China

  Huibiao Zhu

Policies and ethics