8. ICFEM 2006: Macao, China

Keynote Talks

• Zhou Chaochen:
  Program Verification Through Computer Algebra. 1
  
• Gary T. Leavens:
  JML's Rich, Inherited Specifications for Behavioral Subtypes. 2-34
  
• John A. McDermid, Andy Galloway:
  Three Perspectives in Formal Engineering. 35-54
  

Specification and Verification

• Bernhard Beckert, Gerd Beuster:
  A Method for Formalizing, Analyzing, and Verifying Secure User Interfaces. 55-73
  
• Chunqing Chen, Jin Song Dong:
  Applying Timed Interval Calculus to Simulink Diagrams. 74-93
  
• E. Allen Emerson, Richard J. Trefler, Thomas Wahl:
  Reducing Model Checking of the Few to the One. 94-113
  
• Kazuhiro Ogata, Masahiro Nakano, Weiqiang Kong, Kokichi Futatsugi:
  Induction-Guided Falsification. 114-131
  
• Nikola Trcka:
  Verifying chi Models of Industrial Systems with Spin. 132-148
  
• Xiaodong Yi, Ji Wang, Xuejun Yang:
  Stateful Dynamic Partial-Order Reduction. 149-167
  

Internetware and Web-Based Systems

• Xiaoning Ding, Jun Wei, Tao Huang:
  User-Defined Atomicity Constraint: A More Flexible Transaction Model for Reliable Service Composition. 168-184
  
• Puwei Wang, Zhi Jin, Lin Liu:
  Environment Ontology-Based Capability Specification for Web Service Discovery. 185-205
  
• Yan Zhang, Jun Hu, Xiaofeng Yu, Tian Zhang, Xuandong Li, Guoliang Zheng:
  Scenario-Based Component Behavior Derivation. 206-225
  
• Jin Song Dong, Yang Liu, Jun Sun, Xian Zhang:
  Verification of Computation Orchestration Via Timed Automata. 226-245
  
• Jing Li, Jifeng He, Geguang Pu, Huibiao Zhu:
  Towards the Semantics for Web Service Choreography Description Language. 246-263
  
• Hongli Yang, Xiangpeng Zhao, Zongyan Qiu, Chao Cai, Geguang Pu:
  Type Checking Choreography Description Language. 264-283
  

Concurrent, Communicating, Timing and Probabilistic Systems

• Brijesh Dongol:
  Formalising Progress Properties of Non-blocking Programs. 284-303
  
• Douglas A. Creager, Andrew C. Simpson:
  Towards a Fully Generic Theory of Data. 304-323
  
• A. W. Roscoe, Zhenzhong Wu:
  Verifying Statemate Statecharts Using CSP and FDR. 324-341
  
• Jin Song Dong, Ping Hao, Jun Sun, Xian Zhang:
  A Reasoning Method for Timed CSP Based on Constraint Solving. 342-359
  
• Tarek Sadani, Marc Boyer, Pierre de Saqui-Sannes, Jean-Pierre Courtiat:
  Mapping RT-LOTOS Specifications into Time Petri Nets. 360-379
  
• Larissa Meinicke, Ian J. Hayes:
  Reasoning Algebraically About Probabilistic Loops. 380-399
  

Object and Component Orientation

• Nicolas Marti, Reynald Affeldt, Akinori Yonezawa:
  Formal Verification of the Heap Manager of an Operating System Using Separation Logic. 400-419
  
• Bart Jacobs, Jan Smans, Frank Piessens, Wolfram Schulte:
  A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs. 420-439
  
• Xiangpeng Zhao, Quan Long, Zongyan Qiu:
  Model Checking Dynamic UML Consistency. 440-459
  

Testing and Model Checking

• Jessica Chen, Lihua Duan:
  Conditions for Avoiding Controllability Problems in Distributed Testing. 460-477
  
• Samira Tasharofi, Sepand Ansari, Marjan Sirjani:
  Generating Test Cases for Constraint Automata by Genetic Symbiosis Algorithm. 478-493
  
• Isabel Nunes, Antónia Lopes, Vasco Thudichum Vasconcelos, João Abreu, Luís S. Reis:
  Checking the Conformance of Java Classes Against Algebraic Specifications. 494-513
  
• Heike Wehrheim:
  Incremental Slicing. 514-528
  
• Aleksandar Dimovski, Ranko Lazic:
  Assume-Guarantee Software Verification Based on Game Semantics. 529-548
  
• Marcelo d'Amorim, Ahmed Sobeih, Darko Marinov:
  Optimized Execution of Deterministic Blocks in Java PathFinder. 549-567
  

Tools

• Soon-Kyeong Kim, David A. Carrington:
  A Tool for a Formal Pattern Modeling Language. 568-587
  
• Jean-Raymond Abrial, Michael J. Butler, Stefan Hallerstede, Laurent Voisin:
  An Open Extensible Tool Environment for Event-B. 588-605
  
• B. Meenakshi, Abhishek Bhatnagar, Sudeepa Roy:
  Tool for Translating Simulink Models into Input Language of a Model Checker. 606-620
  

Fault-Tolerance and Security

• Tim McComb, Luke Wildman:
  Verifying Abstract Information Flow Properties in Fault Tolerant Security Devices. 621-638
  
• Luigia Petre, Kaisa Sere, Marina A. Waldén:
  A Language for Modeling Network Availability. 639-659
  
• Christian Attiogbé:
  Multi-process Systems Analysis Using Event B: Application to Group Communication Systems. 660-677
  

Specification and Refinement

• John Derrick, Siobhán North, Tony Simons:
  Issues in Implementing a Model Checker for Z. 678-696
  
• Leo Freitas, Ana Cavalcanti, Jim Woodcock:
  Taking Our Own Medicine: Applying the Refinement Calculus to State-Rich Refinement Model Checking. 697-716
  
• Nikolai Tillmann, Feng Chen, Wolfram Schulte:
  Discovering Likely Method Specifications. 717-736
  
• Tomi Westerlund, Juha Plosila:
  Time Aware Modelling and Analysis of Multiclocked VLSI Systems. 737-756
  
• Andreas Bauer, Martin Leucker, Jonathan Streit:
  SALT - Structured Assertion Language for Temporal Logic. 757-775