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

Invited Talks

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

Security and Knowledge

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

Embedded Systems

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

Testing

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

Automated Analysis

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

Hardware

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

Concurrency

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

Last update Sun May 19 22:34:19 2013 CET by the DBLP Team —

This material is Open Data

Data released under the ODC-BY 1.0 license — See also our legal information page