- 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
- 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.
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)| Authors | Title |
|---|---|
| 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)| Authors | Title |
|---|---|
| Chunyan Mu | Quantitative Program Dependence Graphs |
| Tarek Mhamdi, Osman Hasan and Sofiene Tahar | Quantitative Analysis of Information Flow using Theorem Proving |
| Mahsa Varshosaz and Ramtin Khosravi | Modeling and Verification of Probabilistic Actor Systems using pRebeca |
Session 4 [Formal Verification]
Chair: Shengchao Qin (Teesside University, UK)| Authors | Title |
|---|---|
| Zongyan Qiu, Ali Hong and Yijing Liu | Modular Verification of OO Programs with Interfaces |
| François Bobot and Jean-Christophe Filliâtre | Separation Predicates: a Taste of Separation Logic in First-Order Logic |
| William Harrison, Adam Procter and Gerard Allwein | The Confinement Problem in the Presence of Faults |
Session 5 [Tools]
Chair: Yuki Chiba (JAIST, Japan)| Authors | Title |
|---|---|
| Ling Shi, Yang Liu, Jun Sun, Jin Song Dong and Gustavo Carvalho | An Analytical and Experimental Comparison of CSP Extensions and Tools |
| Truong Khanh Nguyen, Jun Sun, Yang Liu and Jin Song Dong | Symbolic 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)| Authors | Title |
|---|---|
| Li Mengjun | A 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 Meyer | Demonic 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)| Authors | Title |
|---|---|
| Takashi Tomita, Shin Hiura, Shigeki Hagihara and Naoki Yonezaki | A Temporal Logic with Mean-Payoff Constraints |
| Meng Han and Zhenhua Duan | Time 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)| Authors | Title |
|---|---|
| Ralf Huuck, Ansgar Fehnker, Maximilian Junker and Alexander Knapp | SMT-based False Positive Elimination in Static Program Analysis |
| Daniel Wonisch and Heike Wehrheim | Predicate Analysis with Block-Abstraction Memoization |
Session 9 [Abstraction and Refinement 2]
Chair: Fumiko Nagoya (Aoyama Gakuin University, Japan)| Authors | Title |
|---|---|
| Yohan Boichut, Benoit Boyer, Axel Legay and Thomas Genet. | Equational Abstraction Refinement for Certified Tree Regular Model Checking |
| Nils Timm, Heike Wehrheim and Mike Czech | Heuristic-Guided Abstraction Refinement for Concurrent Systems |
| Ting Wang, Songzheng Song, Jun Sun, Yang Liu, Jin Song Dong, Xinyu Wang and Shanping Li | More Anti-Chain Based Refinement Checking |
Session 10 [Modeling and Development Methodology]
Chair: Kenji Taguchi (AIST, Japan)| Authors | Title |
|---|---|
| Fabian Buttner, Marina Egea, Jordi Cabot and Martin Gogolla | Verification 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 Zhu | Complementary Methodologies for Developing Hybrid Systems with Event-B |
©ICFEM2012