Contents

Workshop

Workshop

Important Dates

April 30, 2012(Extended)
Full Paper Submission
June 18, 2012
June 22, 2012
Acceptance/Rejection Notification
July 16, 2012
Camera Ready Copy Due

Conference:
November 12–16, 2012

What's New

September 30, 2012
Program at a Glance has been Updated.
August 6, 2012
Registration is available now.
June 29, 2012
Accepted papers has been Updated.
April 25, 2012
Web style has been changed.
Jan 30, 2012
CFP has been revised.
Nov 8, 2011
Web site open.

2012 Accepted Papers

ICFEM 2012: 14th International Conference on Formal Engineering Methods

12th-16th, November, 2012

Kyoto Research Park, Kyoto, Japan

URL: http://www.jaist.ac.jp/icfem2012

Daniel Wonisch and Heike Wehrheim. Predicate Analysis with Block-Abstraction Memoization
Yohan Boichut, Benoit Boyer, Axel Legay and Thomas Genet. Equational Abstraction Refinement for Certified Tree Regular   Model Checking
Edmond Gjondrekaj, Michele Loreti, Rosario Pugliese, Francesco Tiezzi, Carlo Pinciroli, Manuele Brambilla, Mauro Birattari and Marco Dorigo. Towards a Formal Verification Methodology for Collective Robotic Systems
Truong Khanh Nguyen, Jun Sun, Yang Liu and Jin Song Dong. Symbolic Model-Checking of Stateful Timed CSP using BDD and Digitization
Fabian Büttner, Marina Egea, Jordi Cabot and Martin Gogolla. Verification of ATL Transformations Using Transformation Models and Model Finders
Jan Olaf Blech, Yliès Falcone and Klaus Becker. Towards Certified Runtime Verification
Li Mengjun. A Practical Loop Invariant Generation Approach Based on Random Testing,  Constraint Solving and Verification
Duy-Khanh Le, Wei-Ngan Chin and Yong-Meng Teo. Variable Permissions for Concurrency Verification
Nils Timm, Heike Wehrheim and Mike Czech. Heuristic-Guided Abstraction Refinement for Concurrent Systems
Xiaoxiao Yang, Yu Zhang, Ming Fu and Xinyu Feng. A Concurrent Temporal Programming Model with  Atomic Blocks
Wen Su, Jean-Raymond Abrial and Huibiao Zhu. Complementary Methodologies for Developing Hybrid Systems with Event-B
Takashi Tomita, Shin Hiura, Shigeki Hagihara and Naoki Yonezaki. A Temporal Logic with Mean-Payoff Constraints
Ling Shi, Yang Liu, Jun Sun, Jin Song Dong and Gustavo Carvalho. An Analytical and Experimental Comparison of CSP Extensions and Tools
Shang-Wei Lin, Yang Liu, Pao-Ann Hsiung, Jun Sun and Jin Song Dong. Automatic Generation of Provably Correct Embedded Systems
Einar Broch Johnsen, Rudolf Schlatte and Silvia Lizeth Tapia Tarifa. Modeling Resource-Aware Virtualized Applications for the Cloud in Real-Time ABS
Ting Wang, Songzheng Song, Jun Sun, Yang Liu, Jin Song Dong, Xinyu Wang and Shanping Li. More Anti-Chain Based Refinement Checking
Alberto Lluch Lafuente, Jose Meseguer and Andrea Vandin. State Space c-Reductions of Concurrent Systems in Rewriting Logic
Meng Han and Zhenhua Duan. Time Constraints with Temporal Logic Programming
François Bobot and Jean-Christophe Filliatre. Separation Predicates: a Taste of Separation Logic in First-Order Logic
Granville Barnett and Shengchao Qin. A Composable Mixed Mode Concurrency Control Semantics for Transactional Programs
Svetoslav Ganov, Sarfraz Khurshid and Dewayne Perry. Annotation-aided Automated Incremental Analysis for Alloy via Domain Specific Solvers
Chunyan Mu. Quantitative Program Dependence Graphs
Tarek Mhamdi, Osman Hasan and Sofiene Tahar. Quantitative Analysis of Information Flow using Theorem Proving
William Harrison, Adam Procter and Gerard Allwein. The Confinement Problem in the Presence of Faults
Tanmoy Sarkar, Samik Basu and Johnny S. Wong. ConSMutate: SQL Mutants for Guiding Concolic Testing of Database Applications
Ralf Huuck, Ansgar Fehnker, Maximilian Junker and Alexander Knapp. SMT-based False Positive Elimination in Static Program Analysis
Yoshinori Neya and Noriaki Yoshiura. Stepwise Satisfiability Checking Procedure  for Reactive System Specifications by Tableau Method and Proof System
Kazuhiro Ogata and Phan Thi Thanh Huyen. Specification and Model Checking of the Chandy & Lamport Distributed Snapshot Algorithm in Rewriting Logic
Zongyan Qiu, Ali Hong and Yijing Liu. Modular Verification of OO Programs with Interfaces
Scott West, Sebastian Nanz and Bertrand Meyer. Demonic Testing of Concurrent Programs
Mahsa Varshosaz and Ramtin Khosravi. Modeling and Verification of Probabilistic Actor Systems using pRebeca