Abstract is missing.
- A System Development Process with Event-B and the Rodin PlatformJean-Raymond Abrial. 1-3 [doi]
- Challenges in Software CertificationT. S. E. Maibaum. 4-18 [doi]
- Integrating Formal Methods with System ManagementMartin de Groot. 19-36 [doi]
- Formal Engineering of XACML Access Control Policies in VDM++Jeremy Bryans, John S. Fitzgerald. 37-56 [doi]
- A Verification Framework for Agent KnowledgeJin Song Dong, Yuzhang Feng, Ho-Fung Leung. 57-75 [doi]
- From Model-Based Design to Formal Verification of Adaptive Embedded SystemsRasmus Adler, Ina Schaefer, Tobias Schüle, Eric Vecchié. 76-95 [doi]
- Machine-Assisted Proof Support for Validation Beyond SimulinkChunqing Chen, Jin Song Dong, Jun Sun 0001. 96-115 [doi]
- VeSTA: A Tool to Verify the Correct Integration of a Component in a Composite Timed SystemJacques Julliand, Hassan Mountassir, Emilie Oudot. 116-135 [doi]
- Integrating Specification-Based Review and Testing for Detecting Errors in ProgramsShaoying Liu. 136-150 [doi]
- Testing for Refinement in CSPAna Cavalcanti, Marie-Claude Gaudel. 151-170 [doi]
- Reducing Test Sequence Length Using Invertible SequencesLihua Duan, Jessica Chen. 171-190 [doi]
- Model Checking with SAT-Based Characterization of ACTL FormulasWenhui Zhang. 191-211 [doi]
- Automating Refinement Checking in Probabilistic System DesignCarlos Gonzalia, Annabelle McIver. 212-231 [doi]
- Model Checking in Practice: Analysis of Generic Bootloader Using SPINKuntal Das Barman, Debapriyay Mukhopadhyay. 232-245 [doi]
- Model Checking Propositional Projection Temporal Logic Based on SPINCong Tian, Zhenhua Duan. 246-265 [doi]
- A Denotational Semantics for Handel-C Hardware CompilationJuan Ignacio Perna, Jim Woodcock. 266-285 [doi]
- Automatic Generation of Verified Concurrent HardwareMarcel Oliveira, Jim Woodcock. 286-306 [doi]
- Modeling and Verification of Master/Slave Clock Synchronization Using Hybrid Automata and Model-CheckingGuillermo Rodríguez-Navas, Julian Proenza, Hans Hansson. 307-326 [doi]
- Efficient Symbolic Execution of Large Quantifications in a Process AlgebraBenoît Fraikin, Marc Frappier. 327-344 [doi]
- Formalizing SANE Virtual Processor in Thread AlgebraThuy Duong Vu, Chris R. Jesshope. 345-365 [doi]
- Calculating and Composing Progress Properties in Terms of the Leads-to RelationArjan J. Mooij. 366-386 [doi]