9. ICFEM 2007: Boca Raton, FL, USA

Michael Butler, Michael G. Hinchey, María M. Larrondo-Petrie (Eds.): Formal Methods and Software Engineering, 9th International Conference on Formal Engineering Methods, ICFEM 2007, Boca Raton, FL, USA, November 14-15, 2007, Proceedings. Lecture Notes in Computer Science 4789 Springer 2007, ISBN 978-3-540-76648-3 BibTeX

Invited Talks

Jean-Raymond Abrial:
A System Development Process with Event-B and the Rodin Platform. 1-3
Electronic Edition (link) BibTeX
T. S. E. Maibaum:
Challenges in Software Certification. 4-18
Electronic Edition (link) BibTeX

Martin de Groot:
Integrating Formal Methods with System Management. 19-36
Electronic Edition (link) BibTeX
Jeremy Bryans, John S. Fitzgerald:
Formal Engineering of XACML Access Control Policies in VDM++. 37-56
Electronic Edition (link) BibTeX
Jin Song Dong, Yuzhang Feng, Ho-fung Leung:
A Verification Framework for Agent Knowledge. 57-75
Electronic Edition (link) BibTeX

Rasmus Adler, Ina Schaefer, Tobias Schüle, Eric Vecchié:
From Model-Based Design to Formal Verification of Adaptive Embedded Systems. 76-95
Electronic Edition (link) BibTeX
Chunqing Chen, Jin Song Dong, Jun Sun:
Machine-Assisted Proof Support for Validation Beyond Simulink. 96-115
Electronic Edition (link) BibTeX
Jacques Julliand, Hassan Mountassir, Emilie Oudot:
VeSTA: A Tool to Verify the Correct Integration of a Component in a Composite Timed System. 116-135
Electronic Edition (link) BibTeX

Shaoying Liu:
Integrating Specification-Based Review and Testing for Detecting Errors in Programs. 136-150
Electronic Edition (link) BibTeX
Ana Cavalcanti, Marie-Claude Gaudel:
Testing for Refinement in CSP. 151-170
Electronic Edition (link) BibTeX
Lihua Duan, Jessica Chen:
Reducing Test Sequence Length Using Invertible Sequences. 171-190
Electronic Edition (link) BibTeX

Wenhui Zhang:
Model Checking with SAT-Based Characterization of ACTL Formulas. 191-211
Electronic Edition (link) BibTeX
Carlos Gonzalia, Annabelle McIver:
Automating Refinement Checking in Probabilistic System Design. 212-231
Electronic Edition (link) BibTeX
Kuntal Das Barman, Debapriyay Mukhopadhyay:
Model Checking in Practice: Analysis of Generic Bootloader Using SPIN. 232-245
Electronic Edition (link) BibTeX
Cong Tian, Zhenhua Duan:
Model Checking Propositional Projection Temporal Logic Based on SPIN. 246-265
Electronic Edition (link) BibTeX

Juan Ignacio Perna, Jim Woodcock:
A Denotational Semantics for Handel-C Hardware Compilation. 266-285
Electronic Edition (link) BibTeX
Marcel Oliveira, Jim Woodcock:
Automatic Generation of Verified Concurrent Hardware. 286-306
Electronic Edition (link) BibTeX
Guillermo Rodríguez-Navas, Julian Proenza, Hans Hansson:
Modeling and Verification of Master/Slave Clock Synchronization Using Hybrid Automata and Model-Checking. 307-326
Electronic Edition (link) BibTeX

Benoît Fraikin, Marc Frappier:
Efficient Symbolic Execution of Large Quantifications in a Process Algebra. 327-344
Electronic Edition (link) BibTeX
Thuy Duong Vu, Chris R. Jesshope:
Formalizing SANE Virtual Processor in Thread Algebra. 345-365
Electronic Edition (link) BibTeX
Arjan J. Mooij:
Calculating and Composing Progress Properties in Terms of the Leads-to Relation. 366-386
Electronic Edition (link) BibTeX