Program

PROCEEDINGS
ICFEM 2012 proceedings are published by Springer as Volume 7635 in the Lecture Notes in Computer Science series.

ICFEM 2012 (Tentative) Program

14-Nov (Wed) 15-Nov (Thu) 16-Nov (Fri)
08:30~17:00 Registration 08:30-17:00 Registration    
09:00~09:15 Opening        
09:15~10:30 Invited Speech#1 09:00~10:15 Invited Speech#2 09:00~10:15 Invited Speech#3
10:30~11:00 Break 10:15~10:45 Break 10:15~10:45 Break
11:00~12:30 Session 1
(Concurrency)
10:45~12:15 Session 4
(Formal Verification)
10:45~12:15 Session 9 (Abstraction and Refinement 2)
12:30~14:00 Lunch 12:15~13:45 Lunch 12:15~13:45 Lunch
14:00~15:30 Session 2
(Applications of Formal Methods to New Areas)
13:45~15:45 Session 5
(Tools)


Session 6 (Testing and Run-time Verification)
13:45~15:15 Session 10
(Modeling and Development Methodology)

15:30~16:00 Break 15:45~16:15 Break 15:15~15:30 Closing
16:00~17:30 Session 3
(Quantity and Probability)
16:15~17:45 Session 7 (Temporal Logics)

Session 8 (Abstraction and Refinement 1)
   
18:30~20:00 Reception Party 18:30-20:30 Banquet    

Contents of Each Session

Invited Speaker #1
Mario Tokoro (Sony Computer Science Laboratories, Inc., Japan),
"Toward Practical Application of Formal Methods in Software Lifecycle Processes"
Invited Speaker #2
Darren Cofer (Rockwell Collins, USA),
"Formal Methods in the Aerospace Industry: Follow the Money"
Invited Speaker #3
Robert Shostak (Vocera Communications, Inc., USA),
"Applying Term Rewriting to Speech Recognition of Numbers"

Session 1 [Concurrency]

Chiar:Kazuhiro Ogata (JAIST, Japan)
Authors Title
Duy-Khanh Le, Wei-Ngan Chin and Yong-Meng Teo Variable Permissions for Concurrency Verification
Xiaoxiao Yang, Yu Zhang, Ming Fu and Xinyu Feng A Concurrent Temporal Programming Model with Atomic Blocks
Granville Barnett and Shengchao Qin A Composable Mixed Mode Concurrency Control Semantics for Transactional Programs

Session 2 [Applications of Formal Methods to New Areas]

Chair: Peter Ölveczky(University of Oslo, Norway)
AuthorsTitle
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
Einar Broch Johnsen, Rudolf Schlatte and Silvia Lizeth Tapia Tarifa. Modeling Resource-Aware Virtualized Applications for the Cloud in Real-Time ABS
Kazuhiro Ogata and Phan Thi Thanh Huyen. Specification and Model Checking of the Chandy & Lamport Distributed Snapshot Algorithm in Rewriting Logic

Session3 [Quantity and Probability]

Chiar: Naoki Yonezaki (Tokyo Institute of Technology, Japan)
AuthorsTitle
Chunyan MuQuantitative Program Dependence Graphs
Tarek Mhamdi, Osman Hasan and Sofiene Tahar Quantitative Analysis of Information Flow using Theorem Proving
Mahsa Varshosaz and Ramtin KhosraviModeling and Verification of Probabilistic Actor Systems using pRebeca

Session 4 [Formal Verification]

Chair: Shengchao Qin (Teesside University, UK)
AuthorsTitle
Zongyan Qiu, Ali Hong and Yijing LiuModular Verification of OO Programs with Interfaces
François Bobot and Jean-Christophe FilliâtreSeparation Predicates:
a Taste of Separation Logic in First-Order Logic
William Harrison, Adam Procter and Gerard AllweinThe Confinement Problem in the Presence of Faults

Session 5 [Tools]

Chair: Yuki Chiba (JAIST, Japan)
AuthorsTitle
Ling Shi, Yang Liu, Jun Sun, Jin Song Dong and Gustavo CarvalhoAn Analytical and Experimental Comparison of CSP Extensions and Tools
Truong Khanh Nguyen, Jun Sun, Yang Liu and Jin Song DongSymbolic Model-Checking of Stateful Timed CSP using BDD and Digitization
Svetoslav Ganov, Sarfraz Khurshid
and Dewayne Perry
Annotation-aided Automated Incremental Analysis for Alloy via Domain Specific Solvers
Alberto Lluch Lafuente, Jose Meseguer and Andrea Vandin State Space c-Reductions of Concurrent Systems in Rewriting Logic

Session 6 [Testing and Run-time Verification]

Chair: Cyrille Artho (AIST, Japan)
AuthorsTitle
Li MengjunA Practical Loop Invariant Generation Approach Based on Random Testing, Constraint Solving and Verification
Tanmoy Sarkar, Samik Basu and
Johnny S. Wong
ConSMutate: SQL Mutants for Guiding Concolic Testing of Database Applications
Scott West, Sebastian Nanz and Bertrand MeyerDemonic Testing of Concurrent Programs
Jan Olaf Blech, Ylies Falcone and Klaus Becker Towards Certified Runtime Verification

Session 7 [Temporal Logics]

Chair: Jin Song Dong (National University of Singapore, Singapore)
AuthorsTitle
Takashi Tomita, Shin Hiura, Shigeki Hagihara and Naoki YonezakiA Temporal Logic with Mean-Payoff Constraints
Meng Han and Zhenhua DuanTime Constraints with Temporal Logic Programming
Yoshinori Neya and Noriaki Yoshiura Stepwise Satisfiability Checking Procedure for Reactive System Specifications by Tableau Method and Proof System

Session 8 [Abstraction and Refinement 1]

Chair: Jun Sun (Singapore University of Technology and Design, Singapore)
AuthorsTitle
Ralf Huuck, Ansgar Fehnker, Maximilian Junker and Alexander KnappSMT-based False Positive Elimination in Static Program Analysis
Daniel Wonisch and Heike WehrheimPredicate Analysis with Block-Abstraction Memoization

Session 9 [Abstraction and Refinement 2]

Chair: Fumiko Nagoya (Aoyama Gakuin University, Japan)
AuthorsTitle
Yohan Boichut, Benoit Boyer, Axel Legay and Thomas Genet.Equational Abstraction Refinement for Certified Tree Regular Model Checking
Nils Timm, Heike Wehrheim and Mike CzechHeuristic-Guided Abstraction Refinement for Concurrent Systems
Ting Wang, Songzheng Song, Jun Sun, Yang Liu, Jin Song Dong, Xinyu Wang and Shanping LiMore Anti-Chain Based Refinement Checking

Session 10 [Modeling and Development Methodology]

Chair: Kenji Taguchi (AIST, Japan)
AuthorsTitle
Fabian Buttner, Marina Egea, Jordi Cabot and Martin GogollaVerification of ATL Transformations Using Transformation Models and Model Finders
Shang-Wei Lin, Yang Liu, Pao-Ann Hsiung,
Jun Sun and Jin Song Dong
Automatic Generation of Provably Correct Embedded Systems
Wen Su, Jean-Raymond Abrial and Huibiao ZhuComplementary Methodologies for Developing Hybrid Systems with Event-B