Formal Methods and Software Engineering

1. Temporal Logics

   1. Time Constraints with Temporal Logic Programming

      • Meng Han, Zhenhua Duan, Xiaobing Wang

      Pages 266-282

   2. Stepwise Satisfiability Checking Procedure for Reactive System Specifications by Tableau Method and Proof System

      • Yoshinori Neya, Noriaki Yoshiura

      Pages 283-298

2. Abstraction and Refinement

   1. Equational Abstraction Refinement for Certified Tree Regular Model Checking

      • Yohan Boichut, Benoit Boyer, Thomas Genet, Axel Legay

      Pages 299-315

   2. SMT-Based False Positive Elimination in Static Program Analysis

      • Maximilian Junker, Ralf Huuck, Ansgar Fehnker, Alexander Knapp

      Pages 316-331

   3. Predicate Analysis with Block-Abstraction Memoization

      • Daniel Wonisch, Heike Wehrheim

      Pages 332-347

   4. Heuristic-Guided Abstraction Refinement for Concurrent Systems

      • Nils Timm, Heike Wehrheim, Mike Czech

      Pages 348-363

   5. More Anti-chain Based Refinement Checking

      • Ting Wang, Songzheng Song, Jun Sun, Yang Liu, Jin Song Dong, Xinyu Wang et al.

      Pages 364-380

3. Tools

   1. An Analytical and Experimental Comparison of CSP Extensions and Tools

      • Ling Shi, Yang Liu, Jun Sun, Jin Song Dong, Gustavo Carvalho

      Pages 381-397

   2. Symbolic Model-Checking of Stateful Timed CSP Using BDD and Digitization

      • Truong Khanh Nguyen, Jun Sun, Yang Liu, Jin Song Dong

      Pages 398-413

   3. Annotations for Alloy: Automated Incremental Analysis Using Domain Specific Solvers

      • Svetoslav Ganov, Sarfraz Khurshid, Dewayne E. Perry

      Pages 414-429

   4. State Space c-Reductions of Concurrent Systems in Rewriting Logic

      • Alberto Lluch Lafuente, José Meseguer, Andrea Vandin

      Pages 430-446

4. Testing and Runtime Verification

   1. A Practical Loop Invariant Generation Approach Based on Random Testing, Constraint Solving and Verification

      • Mengjun Li

      Pages 447-461

   2. ConSMutate: SQL Mutants for Guiding Concolic Testing of Database Applications

      • Tanmoy Sarkar, Samik Basu, Johnny S. Wong

      Pages 462-477

   3. Demonic Testing of Concurrent Programs

      • Scott West, Sebastian Nanz, Bertrand Meyer

      Pages 478-493

   4. Towards Certified Runtime Verification

      • Jan Olaf Blech, Yliès Falcone, Klaus Becker

      Pages 494-509

5. Back Matter

   PDF

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.

• concurrent systems
• distributed systems
• model checking
• specification optimization
• temporal logic
• algorithm analysis and problem complexity

• Japan Advanced Institute of Science and Technology (JAIST), Nuomi, Japan

  Toshiaki Aoki

• National Institute of Advanced Industrial Science and Technology (AIST), Amagasaki, Japan

  Kenji Taguchi

Policies and ethics