| Invited Talks |
| A System Development Process with Event-B and the Rodin Platform / Jean-Raymond Abrial |
| Challenges in Software Certification / Tom Maibaum |
| Security and Knowledge |
| Integrating Formal Methods with System Management / Martin de Groot |
| Formal Engineering of XACML Access Control Policies in VDM++ / Jeremy W. Bryans ; John S. Fitzgerald |
| A Verification Framework for Agent Knowledge / Jin Song Dong ; Yuzhang Feng ; Ho-fung Leung |
| Embedded Systems |
| From Model-Based Design to Formal Verification of Adaptive Embedded Systems / Rasmus Adler ; Ina Schaefer ; Tobias Schuele ; Eric Vecchie |
| Machine-Assisted Proof Support for Validation Beyond Simulink / Chunqing Chen ; Jun Sun |
| VeSTA: A Tool to Verify the Correct Integration of a Component in a Composite Timed System / Jacques Julliand ; Hassan Mountassir ; Emilie Oudot |
| Testing |
| Integrating Specification-Based Review and Testing for Detecting Errors in Programs / Shaoying Liu |
| Testing for Refinement in CSP / Ana Cavalcanti ; Marie-Claude Gaudel |
| Reducing Test Sequence Length Using Invertible Sequences / Lihua Duan ; Jessica Chen |
| Automated Analysis |
| Model Checking with SAT-Based Characterization of ACTL Formulas / Wenhui Zhang |
| Automating Refinement Checking in Probabilistic System Design / Carlos Gonzalia ; Annabelle McIver |
| Model Checking in Practice: Analysis of Generic Bootloader Using SPIN / Kuntal Das Barman ; Debapriyay Mukhopadhyay |
| Model Checking Propositional Projection Temporal Logic Based on SPIN / Cong Tian ; Zhenhua Duan |
| Hardware |
| A Denotational Semantics for Handel-C Hardware Compilation / Juan Ignacio Perna ; Jim Woodcock |
| Automatic Generation of Verified Concurrent Hardware / Marcel Oliveira |
| Modeling and Verification of Master/Slave Clock Synchronization Using Hybrid Automata and Model-Checking / Guillermo Rodriguez-Navas ; Julian Proenza ; Hans Hansson |
| Concurrency |
| Efficient Symbolic Execution of Large Quantifications in a Process Algebra / Benoit Fraikin ; Marc Frappier |
| Formalizing SANE Virtual Processor in Thread Algebra / Thuy Duong Vu ; Chris Jesshope |
| Calculating and Composing Progress Properties in Terms of the Leads-to Relation / Arjan J. Mooij |
| Author Index |
| Invited Talks |
| A System Development Process with Event-B and the Rodin Platform / Jean-Raymond Abrial |
| Challenges in Software Certification / Tom Maibaum |
| Security and Knowledge |
| Integrating Formal Methods with System Management / Martin de Groot |
| Formal Engineering of XACML Access Control Policies in VDM++ / Jeremy W. Bryans ; John S. Fitzgerald |
