6. ICFEM 2004: Seattle, WA, USA

Jim Davies, Wolfram Schulte, Michael Barnett (Eds.): Formal Methods and Software Engineering, 6th International Conference on Formal Engineering Methods, ICFEM 2004, Seattle, WA, USA, November 8-12, 2004, Proceedings. Lecture Notes in Computer Science 3308 Springer 2004, ISBN 3-540-23841-7 BibTeX

Tutorials

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

Invited Talks

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

Full Papers

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