


default search action
9th ICFEM 2007: Boca Raton, FL, USA
- Michael J. Butler, Michael G. Hinchey, María M. Larrondo-Petrie

:
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 W. 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 Gonzalía, 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
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

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














