Accepted Papers

The program committee selected 24 regular papers and 7 short papers from over 90 submissions. Each paper was read by at least 3 reviewers.

Proceedings of the Tenth NASA Formal Methods Symposium appear in Springer's Lecture Notes in Computer Science, Formal Methods subline, as Volume 10811.

• Ansgar Fehnker, Kaylash Chaudhary and Vinay Mehta An Even Better Approach - Improving the B.A.T.M.A.N. Protocol Through Formal Modelling and Analysis
• Massimo Narizzano, Luca Pulina, Armando Tacchella and Simone Vuotto. Consistency of Property Specification Patterns with Boolean and Constrained Numerical Signals
• Marcus Gerhold, Arnd Hartmanns and Mariëlle Stoelinga . Model-Based Testing for General Stochastic Time
• Ruben Giaquinta, Ruth Hoffmann, Murray Ireland, Alice Miller, and Gethin Norman. Strategy Synthesis for Autonomous Agents using PRISM
• Miguel Romero and Camilo Rocha . Symbolic Execution and Reachability Analysis using Rewriting Modulo SMT for Spatial Concurrent Constraint Systems with Extrusion
• Lola Masson, Jérémie Guiochet, Helene Waeselynck, Kalou Cabrera, Sofia Cassel and Martin Törngren. Tuning permissiveness of active safety monitors for autonomous systems
• Radha Nakade, Eric Mercer, Peter Aldous and Jay McCarthy. Model Checking Task Parallel Programs for Data-race
• Aymeric Fromherz, Abdelraouf Ouadjaout and Antoine Miné. Static Value Analysis of Python Programs by Abstract Interpretation
• Flavio M. de Paula, Arvind Haran and Brad Bingham. An Efficient Rewriting Framework for Trace Coverage of Symmetric Systems
• Ansgar Fehnker and Kaylash Chaudhary . Twenty Percent and a Few Days - Optimising a Bitcoin Majority Attack (short paper)
• Jeroen Meijer and Jaco van de Pol. Sound Black-Box Checking in the LearnLib
• Philipp Koerner and Jens Bendisposto. Distributed Model Checking Using ProB
• Saksham Chand and Yanhong A. Liu. Simpler Specifications and Easier Proofs of Distributed Algorithms Using History Variables
• Siddhartha Bhattacharyya, Thomas Eskridge, Natasha Neogi, Marco Carvalho and Milton Stafford. Formal Assurance for Cooperative Intelligent Autonomous Agents
• Yassmeen Elderhalli, Osman Hasan, Waqar Ahmed and Sofiène Tahar. Formal Dynamic Fault Trees Analysis using an Integration of Theorem Proving and Model Checking
• Sarah Benyagoub, Meriem Ouederni, Yamine Ait Ameur, and Atif Mashkoor. Incremental Construction of Realizable Choreographies
• César Augusto Ochoa Escudero, Rémi Delmas, Thomas Bochot, Matthieu David, andVirginie Wiels. Automatic Generation of DO-178 Test Procedures
• Andrew Ireland, Maria Teresa Llano and Simon Colton. The Use of Automated Theory Formation in Support of Hazard Analysis (short paper)
• Zhuo Chen and Werner Dietl. Don't Miss the End: Preventing Unsafe End-of-File Comparisons (short paper)
• András Vörös, Márton Búr, István Ráth, Ákos Horváth, Zoltán Micskei, László Balogh, Bálint Hegyi, Benedek Horváth, Zsolt Mázló and Dániel Varró. MoDeS3: Model-based Demonstrator for Smart and Safe Cyber-Physical Systems (short paper)
• Giovanna Broccia, Paolo Milazzo and Peter Csaba Ölveczky. An Executable Formal Framework for Safety-Critical Human Multitasking
• Marco Feliú and Mariano Moscato . Towards a Formal Safety Framework for Trajectories (short paper)
• Rui Qiu, Sarfraz Khurshid, Corina Pasareanu, Junye Wen and Guowei Yang . Using Test Ranges to Improve Symbolic Execution
• Allan Blanchard, Nikolai Kosmatov and Frédéric Loulergue . Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C
• Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan and Ashish Tiwari. Output Range Analysis for Deep Feedforward Neural Networks
• Bruno Dutertre, Dejan Jovanović and Jorge Navas. Verification of Fault-Tolerant Protocols with Sally (short paper)
• Alfons Laarman. Optimal Storage of Combinatorial State Spaces
• Alfons Laarman. Stubborn Transaction Reduction
• Cumhur Erkan Tuncali, Bardh Hoxha, Guohui Ding, Georgios Fainekos and Sriram Sankaranarayanan. Experience Report: Application of Falsification Methods on the UxAS System (short paper)
• Hendrik Maarand and Tarmo Uustalu. Certified Foata Normalization for Generalized Traces
• Francesco Marconi, Giovanni Quattrocchi, Luciano Baresi, Marcello M. Bersani and Matteo Rossi. On the Timed Analysis of Big-Data Applications