12. ICFEM 2010: Shanghai, China

Invited Talks

• Kokichi Futatsugi:
  Fostering Proof Scores in CafeOBJ. 1-20
  
• Matthew B. Dwyer:
  Exploiting Partial Success in Applying Automated Formal Methods. 21
  
• Wang Yi:
  Multicore Embedded Systems: The Timing Problem and Possible Solutions. 22-23
  

Theorem Proving and Decision Procedures

• Johannes Eriksson, Ralph-Johan Back:
  Applying PVS Background Theories and Proof Strategies in Invariant Based Programming. 24-39
  
• Augusto Ribeiro, Peter Gorm Larsen:
  Proof Obligation Generation and Discharging for Recursive Definitions in VDM. 40-55
  
• Iman Poernomo, Jeffrey Terrell:
  Correct-by-Construction Model Transformations from Partially Ordered Specifications in Coq. 56-73
  
• Alejandro Sánchez, César Sánchez:
  Decision Procedures for the Temporal Verification of Concurrent Lists. 74-89
  
• Zhenhua Duan, Cong Tian:
  An Improved Decision Procedure for Propositional Projection Temporal Logic. 90-105
  

Web Services and Workflow

• Natallia Kokash, Behnaz Changizi, Farhad Arbab:
  A Semantic Model for Service Composition with Coordination Time Delays. 106-121
  
• Fazle Rabbi, Hao Wang, Wendy MacCaull:
  Compensable WorkFlow Nets. 122-137
  
• Lei Zhou, Jing Ping, Hao Xiao, Zheng Wang, Geguang Pu, Zuohua Ding:
  Automatically Testing Web Services Choreography with Assertions. 138-154
  
• Zuohua Ding, Hui Shen, Jing Liu:
  Applying Ordinary Differential Equations to the Performance Analysis of Service Composition. 155-170
  

Verification I

• Shengchao Qin, Chenguang Luo, Guanhua He, Florin Craciun, Wei-Ngan Chin:
  Verifying Heap-Manipulating Programs with Unknown Procedure Calls. 171-187
  
• Xin Li, H. James Hoover, Piotr Rudnicki:
  API Conformance Verification for Java Programs. 188-203
  
• Alessio Lomuscio, Ben Strulo, Nigel G. Walker, Peng Wu:
  Assume-Guarantee Reasoning with Local Specifications. 204-219
  
• Eugen-Ioan Goriac, Dorel Lucanu, Grigore Rosu:
  Automating Coinduction with Case Analysis. 220-236
  

Applications of Formal Methods

• Hai H. Wang, Danica Damljanovic, Jing Sun:
  Enhanced Semantic Access to Formal Software Models. 237-252
  
• Denis Hatebur, Maritta Heisel:
  Making Pattern- and Model-Based Software Development More Rigorous. 253-269
  
• Andi Bejleri:
  Practical Parameterised Session Types. 270-286
  
• Ken Madlener, Sjaak Smetsers, Marko C. J. D. van Eekelen:
  A Formal Verification Study on the Rotterdam Storm Surge Barrier. 287-302
  

Verification II

• José Meseguer, Peter Csaba Ölveczky:
  Formalization and Correctness of the PALS Architectural Pattern for Distributed Real-Time Systems. 303-320
  
• Antti Siirtola:
  Automated Multiparameterised Verification by Cut-Offs. 321-337
  
• Youssef Hanna, David Samuelson, Samik Basu, Hridesh Rajan:
  Automating Cut-off for Multi-parameterized Systems. 338-354
  
• Miroslav N. Velev, Ping Gao:
  Method for Formal Verification of Soft-Error Tolerance Mechanisms in Pipelined Microprocessors. 355-370
  
• Islam Abdelhalim, James Sharp, Steve A. Schneider, Helen Treharne:
  Formal Verification of Tokeneer Behaviours Modelled in fUML Using CSP. 371-387
  

Probability and Concurrency

• Jun Sun, Songzheng Song, Yang Liu:
  Model Checking Hierarchical Probabilistic Systems. 388-403
  
• Zijiang Yang, Karem A. Sakallah:
  Trace-Driven Verification of Multithreaded Programs. 404-419
  
• Jonathan Billington, Guy Edward Gallasch:
  Closed Form Approximations for Steady State Probabilities of a Controlled Fork-Join Network. 420-435
  
• Imene Ben Hafaiedh, Susanne Graf, Sophie Quinton:
  Reasoning about Safety and Progress Using Contracts. 436-451
  

Program Analysis

• Isabella Mastroeni, Durica Nikolic:
  Abstract Program Slicing: From Theory towards an Implementation. 452-467
  
• Shengchao Qin, Guanhua He, Chenguang Luo, Wei-Ngan Chin:
  Loop Invariant Synthesis in a Combined Domain. 468-484
  
• Andreas Vogelsang, Ansgar Fehnker, Ralf Huuck, Wolfgang Reif:
  Software Metrics in Static Program Analysis. 485-500
  
• Kazuhiro Ogata, Kokichi Futatsugi:
  A Combination of Forward and Backward Reachability Analysis Methods. 501-517
  

Model Checking

• Jun Sun, Yang Liu, Bin Cheng:
  Model Checking a Model Checker: A Code Contract Combined Approach. 518-533
  
• Nils Timm, Heike Wehrheim:
  On Symmetries and Spotlights - Verifying Parameterised Systems. 534-548
  
• Jonathan Ezekiel, Alessio Lomuscio:
  A Methodology for Automatic Diagnosability Analysis. 549-564
  
• Rüdiger Ehlers, Michael Gerke, Hans-Jörg Peter:
  Making the Right Cut in Model Checking Data-Intensive Timed Systems. 565-580
  
• Marc Frappier, Benoît Fraikin, Romain Chossart, Raphaël Chane-Yack-Fa, Mohammed Ouenzar:
  Comparison of Model Checking Tools for Information Systems. 581-596
  

Object Orientation and Model Driven Engineering

• Scott West, Sebastian Nanz, Bertrand Meyer:
  A Modular Scheme for Deadlock Prevention in an Object-Oriented Programming Model. 597-612
  
• Prabhu Shankar Kaliappan, Hartmut König, Sebastian Schmerl:
  Model-Driven Protocol Design Based on Component Oriented Modeling. 613-629
  
• Hong Zhu, Ian Bayley:
  Laws of Pattern Composition. 630-645
  
• Einar Broch Johnsen, Olaf Owe, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa:
  Dynamic Resource Reallocation between Deployment Components. 646-661
  

Specification and Verification

• Xi Wang, Shaoying Liu, Huaikou Miao:
  A Pattern System to Support Refining Informal Ideas into Formal Expressions. 662-677
  
• Min Zhang, Kazuhiro Ogata, Masaki Nakamura:
  Specification Translation of State Machines from Equational Theories into Rewrite Theories. 678-693
  
• Cong Tian, Zhenhua Duan:
  Alternating Interval Based Temporal Logics. 694-709
  

Last update Fri May 25 08:18:53 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page