Abstract is missing.
- The Versatile Synchronous ObserverJohn M. Rushby. 1 [doi]
- Thirteen Years of Automated Code Analysis at MicrosoftWolfram Schulte. 2 [doi]
- Model Checking Propositional Deontic Temporal Logic via a μ-Calculus CharacterizationAraceli Acosta, Cecilia Kilmurray, Pablo F. Castro, Nazareno Aguirre. 3-18 [doi]
- An Approach Using the B Method to Formal Verification of PLC Programs in an Industrial SettingHaniel Barbosa, David Déharbe. 19-34 [doi]
- Palytoxin Inhibits the Sodium-Potassium Pump - An Investigation of an Electrophysiological Model Using Probabilistic Model CheckingFernando A. F. Braz, Jader S. Cruz, Alessandra C. Faria-Campos, Sérgio V. A. Campos. 35-50 [doi]
- BETA: A B Based Testing ApproachErnesto Cid Brasil de Matos, Anamaria Martins Moreira. 51-66 [doi]
- A Process Algebra Based Strategy for Generating Test Vectors from SCR SpecificationsGustavo Carvalho, Diogo Falcão, Alexandre Mota, Augusto Sampaio. 67-82 [doi]
- Specification Patterns for Properties over Reachable States of Graph GrammarsSimone Andre da Costa Cavalheiro, Luciana Foss, Leila Ribeiro. 83-98 [doi]
- Compositionality and Refinement in Model-Driven EngineeringJim Davies, Jeremy Gibbons, David Milward, James Welch. 99-114 [doi]
- Identifying Hardware Failures SystematicallyAndré Didier, Alexandre Mota. 115-130 [doi]
- Investigating Time Properties of Interrupt-Driven ProgramsYanhong Huang, Yongxin Zhao, Jianqi Shi, Huibiao Zhu, Shengchao Qin. 131-146 [doi]
- Specifying and Verifying Declarative Fluent Temporal Logic Properties of WorkflowsGermán Regis, Nicolás Ricci, Nazareno Aguirre, T. S. E. Maibaum. 147-162 [doi]
- Composition of Model Transformations: A Categorical FrameworkChristoph Schulz, Michael Löwe, Harald König. 163-178 [doi]
- Verification Rules for Exception Handling in EiffelEmil Sekerinski, Tian Zhang. 179-193 [doi]
- A Sound Reduction of Persistent-Sets for Deadlock Detection in MPI ApplicationsSubodh Sharma, Ganesh Gopalakrishnan, Greg Bronevetsky. 194-209 [doi]
- Alternating-Time Temporal Logic in the Calculus of (Co)Inductive ConstructionsDante Zanarini, Carlos Luna, Luis Sierra. 210-225 [doi]