6. ICFEM 2004: Seattle, WA, USA

Tutorials

• Bernhard Schätz:
  Model-Based Development: Combining Engineering Approaches and Formal Techniques. 1-2
  
• Chris George:
  Tutorial on the RAISE Language, Method and Tools. 3-4
  
• Jonathan Jacky:
  Model-Based Testing with Spec#. 5-6
  
• Shaoying Liu:
  Formal Engineering for Industrial Software Development - An Introduction to the SOFL Specification Language and Method. 7-8
  
• Edmund M. Clarke, Daniel Kroening:
  Tutorial: Software Model Checking. 9-10
  

Invited Talks

• Amitabh Srivastava:
  Engineering Quality Software. 11
  
• Peter G. Neumann:
  When Can Formal Methods Make a Real Difference? 12
  
• J. Strother Moore:
  On the Adoption of Formal Methods by Industry: The ACL2 Experience. 13
  
• Joxan Jaffar:
  A CLP Approach to Modelling Systems. 14
  

Full Papers

• Jean-Christophe Filliâtre, Claude Marché:
  Multi-prover Verification of C Programs. 15-29
  
• Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom:
  Memory-Model-Sensitive Data Race Analysis. 30-45
  
• Jessica Chen, Xiaoshan Zhao:
  Formal Models for Web Navigations with Session Control and Browser Cache. 46-60
  
• Bill Aldrich, Ansgar Fehnker, Peter H. Feiler, Zhi Han, Bruce H. Krogh, Eric Lim, Shiva Sivashankar:
  Managing Verification Activities Using SVM. 61-75
  
• Richard H. Carver, Yu Lei:
  A General Model for Reachability Testing of Concurrent Programs. 76-98
  
• Kai Baukus, Ron van der Meyden:
  A Knowledge Based Analysis of Cache Coherence. 99-114
  
• Wei Zhang, Haiyan Zhao, Hong Mei:
  A Propositional Logic-Based Method for Verification of Feature Models. 115-130
  
• Jifeng He, Carroll Morgan, Annabelle McIver:
  Deriving Probabilistic Semantics Via the 'Weakest Completion'. 131-145
  
• Aleksandar Dimovski, Ranko Lazic:
  CSP Representation of Game Semantics for Second-Order Idealized Algol. 146-161
  
• Marcelo F. Frias, Carlos López Pombo, Nazareno Aguirre:
  An Equational Calculus for Alloy. 162-175
  
• Nicolae Goga, Judi Romijn:
  Guiding Spin Simulation. 176-193
  
• YoungMin Kwon, Gul Agha:
  Linear Inequality LTL (iLTL): A Model Checker for Discrete Time Markov Chains. 194-208
  
• Alessandro Armando, Claudio Castellini, Jacopo Mantovani:
  Software Model Checking Using Linear Constraints. 209-223
  
• Daniel Kroening, Alex Groce, Edmund M. Clarke:
  Counterexample Guided Abstraction Refinement Via Program Execution. 224-238
  
• Fabrice Bouquet, Bruno Legeard, Mark Utting, Nicolas Vacelet:
  Faster Analysis of Formal Specifications. 239-258
  
• Yanjun Wen, Ji Wang, Zhi-Chang Qi:
  Bridging Refinement of Interface Automata to Forward Simulation of I/O Automata. 259-273
  
• Abhay Vardhan, Koushik Sen, Mahesh Viswanathan, Gul Agha:
  Learning to Verify Safety Properties. 274-289
  
• Tao Xie, David Notkin:
  Automatic Extraction of Object-Oriented Observer Abstractions from Unit-Test Executions. 290-305
  
• Ling Liu, Huaikou Miao:
  A Specification-Based Approach to Testing Polymorphic Attributes. 306-319
  
• Marcel Oliveira, Ana Cavalcanti:
  From Circus to JCSP. 320-340
  
• Mahadevan Subramaniam, Parvathi Chundi:
  An Approach to Preserve Protocol Consistency and Executability Across Updates. 341-356
  
• Feng Chen, Marcelo d'Amorim, Grigore Rosu:
  A Formal Monitoring-Based Framework for Software Development and Analysis. 357-372
  
• Konstantine Arkoudas, Karen Zee, Viktor Kuncak, Martin C. Rinard:
  Verifying a File System Implementation. 373-390
  
• Carsten Sinz, Wolfgang Küchlin:
  Verifying the On-line Help System of SIEMENS Magnetic Resonance Tomographs. 391-402
  
• Nazareno Aguirre, Juan Bicarregui, Lucio Guzmán, T. S. E. Maibaum:
  Implementing Dynamic Aggregations of Abstract Machines in the B Method. 403-417
  
• Nuno Amálio, Susan Stepney, Fiona Polack:
  Formal Proof from UML Models. 418-433
  
• Michael Balser, Simon Bäumler, Alexander Knapp, Wolfgang Reif, Andreas Thums:
  Interactive Verification of UML State Machines. 434-448
  
• Mila E. Majster-Cederbaum, Jinzhao Wu, Houguang Yue, Naijun Zhan:
  Refinement of Actions for Real-Time Concurrent Systems with Causal Ambiguity. 449-463
  
• Yifeng Chen, Zhiming Liu:
  From Durational Specifications to TLA Designs of Timed Automata. 464-482
  
• Jin Song Dong, Ping Hao, Shengchao Qin, Jun Sun, Wang Yi:
  Timed Patterns: TCOZ to Timed Automata. 483-498