| Andrew Simpson and Jaco Jacobs | On the cloud-enabled refinement checking of railway signalling interlockings |
| Colin Pilbrow and Robi Malik | Compositional Nonblocking Verification with Always Enabled Events and Selfloop-only Events |
| Simon Ware, Robi Malik, Sahar Mohajerani and Martin Fabian | Certainly Unsupervisable States |
| Judy Bowen, Steve Reeves and Steve Jones | Creating Visualisations of Formal Models of Interactive Medical Devices |
| Yongjian Li and Jun Pang | A Strand Space Approach to Provable Anonymity |
| Linna Pang, Chen-Wei Wang, Mark Lawford and Alan Wassyng | Formalizing and Verifying Function Blocks using Tabular Expressions and PVS |
| Chen-Wei Wang, Jonathan Ostroff and Simon Hudon | Precise Documentation and Validation of Requirements |
| Jonathan Ostroff, Chen-Wei Wang, Yang Liu, Jun Sun and Simon Hudon | TTM/PAT: Specifying and Verifying Timed Transition Models |
| Jagadish Suryadevara, Gaetana Sapienza, Cristina Seceleanu, Tiberiu Seceleanu, Stein Erik Ellevseth and Paul Pettersson | Wind Turbine System: An Industrial Case Study in Formal Modeling and Verification |
| David Pearce and Lindsay Groves | Reflections on Verifying Software with Whiley |
| Kriangkrai Traichaiyaporn and Toshiaki Aoki | Refinement Tree and Its Patterns: a Graphical Approach for Event-B Modeling |
| Xiaoyun Guo, Hsin-Hung Lin, Kenro Yatake and Toshiaki Aoki | An UPPAAL Framework for Model Checking Automotive Systems with FlexRay Protocol |
| Cyrille Valentin Artho, Koji Hayamizu, Rudolf Ramler and Yoriyuki Yamagata | With an Open Mind: How to Write Good Models |
| Gustavo Carvalho, Flavia Barros, Florian Lapschies, Uwe Schulze and Jan Peleska | Model Based Testing from Controlled Natural Language Requirements |
| Khaza Anuarul Hoque, Otmane Ait Mohamed and Yvon Savaria | Early Analysis of Soft Error Effects for Aerospace Applications using Probabilistic Model Checking |
| Zeynab Sabahi Kaviani, Ramtin Khosravi, Marjan Sirjani, Peter Olveczky and Ehsan Khamespanah | Formal Semantics and Analysis of Timed Rebeca in Real-Time Maude |
| Youcheng Sun, Romain Soulat, Giuseppe Lipari, Etienne Andre and Laurent Fribourg | Parametric Schedulability Analysis of Fixed Priority Real-Time Distributed Systems |
| Johanna Nellen, Erika Abraham, Xin Chen and Pieter Collins | Counterexample generation for hybrid automata |
|
Conference Information
General Information
 |
|