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
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 - Guillermo Rodríguez-Navas
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
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.
last updated on 2024-12-19 22:18 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: