Front Matter ....Pages I-XI
Incremental Construction of Realizable Choreographies (Sarah Benyagoub, Meriem Ouederni, Yamine Aït-Ameur, Atif Mashkoor)....Pages 1-19
Formal Assurance for Cooperative Intelligent Autonomous Agents (Siddhartha Bhattacharyya, Thomas C. Eskridge, Natasha A. Neogi, Marco Carvalho, Milton Stafford)....Pages 20-36
Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C (Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue)....Pages 37-53
An Executable Formal Framework for Safety-Critical Human Multitasking (Giovanna Broccia, Paolo Milazzo, Peter Csaba Ölveczky)....Pages 54-69
Simpler Specifications and Easier Proofs of Distributed Algorithms Using History Variables (Saksham Chand, Yanhong A. Liu)....Pages 70-86
Don’t Miss the End: Preventing Unsafe End-of-File Comparisons (Charles Zhuo Chen, Werner Dietl)....Pages 87-94
An Efficient Rewriting Framework for Trace Coverage of Symmetric Systems (Flavio M. De Paula, Arvind Haran, Brad Bingham)....Pages 95-112
Verification of Fault-Tolerant Protocols with Sally (Bruno Dutertre, Dejan Jovanović, Jorge A. Navas)....Pages 113-120
Output Range Analysis for Deep Feedforward Neural Networks (Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, Ashish Tiwari)....Pages 121-138
Formal Dynamic Fault Trees Analysis Using an Integration of Theorem Proving and Model Checking (Yassmeen Elderhalli, Osman Hasan, Waqar Ahmad, Sofiène Tahar)....Pages 139-156
Twenty Percent and a Few Days – Optimising a Bitcoin Majority Attack (Ansgar Fehnker, Kaylash Chaudhary)....Pages 157-163
An Even Better Approach – Improving the B.A.T.M.A.N. Protocol Through Formal Modelling and Analysis (Ansgar Fehnker, Kaylash Chaudhary, Vinay Mehta)....Pages 164-178
Towards a Formal Safety Framework for Trajectories (Marco A. Feliú, Mariano M. Moscato)....Pages 179-184
Static Value Analysis of Python Programs by Abstract Interpretation (Aymeric Fromherz, Abdelraouf Ouadjaout, Antoine Miné)....Pages 185-202
Model-Based Testing for General Stochastic Time (Marcus Gerhold, Arnd Hartmanns, Mariëlle Stoelinga)....Pages 203-219
Strategy Synthesis for Autonomous Agents Using PRISM (Ruben Giaquinta, Ruth Hoffmann, Murray Ireland, Alice Miller, Gethin Norman)....Pages 220-236
The Use of Automated Theory Formation in Support of Hazard Analysis (Andrew Ireland, Maria Teresa Llano, Simon Colton)....Pages 237-243
Distributed Model Checking Using ProB (Philipp Körner, Jens Bendisposto)....Pages 244-260
Optimal Storage of Combinatorial State Spaces (Alfons Laarman)....Pages 261-279
Stubborn Transaction Reduction (Alfons Laarman)....Pages 280-298
Certified Foata Normalization for Generalized Traces (Hendrik Maarand, Tarmo Uustalu)....Pages 299-314
On the Timed Analysis of Big-Data Applications (Francesco Marconi, Giovanni Quattrocchi, Luciano Baresi, Marcello M. Bersani, Matteo Rossi)....Pages 315-332
Tuning Permissiveness of Active Safety Monitors for Autonomous Systems (Lola Masson, Jérémie Guiochet, Hélène Waeselynck, Kalou Cabrera, Sofia Cassel, Martin Törngren)....Pages 333-348
Sound Black-Box Checking in the LearnLib (Jeroen Meijer, Jaco van de Pol)....Pages 349-366
Model-Checking Task Parallel Programs for Data-Race (Radha Nakade, Eric Mercer, Peter Aldous, Jay McCarthy)....Pages 367-382
Consistency of Property Specification Patterns with Boolean and Constrained Numerical Signals (Massimo Narizzano, Luca Pulina, Armando Tacchella, Simone Vuotto)....Pages 383-398
Automatic Generation of DO-178 Test Procedures (César Ochoa Escudero, Rémi Delmas, Thomas Bochot, Matthieu David, Virginie Wiels)....Pages 399-415
Using Test Ranges to Improve Symbolic Execution (Rui Qiu, Sarfraz Khurshid, Corina S. Păsăreanu, Junye Wen, Guowei Yang)....Pages 416-434
Symbolic Execution and Reachability Analysis Using Rewriting Modulo SMT for Spatial Concurrent Constraint Systems with Extrusion (Miguel Romero, Camilo Rocha)....Pages 435-451
Experience Report: Application of Falsification Methods on the UxAS System (Cumhur Erkan Tuncali, Bardh Hoxha, Guohui Ding, Georgios Fainekos, Sriram Sankaranarayanan)....Pages 452-459
MoDeS3: Model-Based Demonstrator for Smart and Safe Cyber-Physical Systems (András Vörös, Márton Búr, István Ráth, Ákos Horváth, Zoltán Micskei, László Balogh et al.)....Pages 460-467
Back Matter ....Pages 469-470