NASA Formal Methods

1. Front Matter

   Pages I-XI

   PDF

2. Incremental Construction of Realizable Choreographies

   • Sarah Benyagoub, Meriem Ouederni, Yamine Aït-Ameur, Atif Mashkoor

   Pages 1-19

3. Formal Assurance for Cooperative Intelligent Autonomous Agents

   • Siddhartha Bhattacharyya, Thomas C. Eskridge, Natasha A. Neogi, Marco Carvalho, Milton Stafford

   Pages 20-36

4. Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C

   • Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue

   Pages 37-53

5. An Executable Formal Framework for Safety-Critical Human Multitasking

   • Giovanna Broccia, Paolo Milazzo, Peter Csaba Ölveczky

   Pages 54-69

6. Simpler Specifications and Easier Proofs of Distributed Algorithms Using History Variables

   • Saksham Chand, Yanhong A. Liu

   Pages 70-86

7. Don’t Miss the End: Preventing Unsafe End-of-File Comparisons

   • Charles Zhuo Chen, Werner Dietl

   Pages 87-94

8. An Efficient Rewriting Framework for Trace Coverage of Symmetric Systems

   • Flavio M. De Paula, Arvind Haran, Brad Bingham

   Pages 95-112

9. Verification of Fault-Tolerant Protocols with Sally

   • Bruno Dutertre, Dejan Jovanović, Jorge A. Navas

   Pages 113-120

10. Output Range Analysis for Deep Feedforward Neural Networks

    • Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, Ashish Tiwari

    Pages 121-138

11. 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

12. Twenty Percent and a Few Days – Optimising a Bitcoin Majority Attack

    • Ansgar Fehnker, Kaylash Chaudhary

    Pages 157-163

13. 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

14. Towards a Formal Safety Framework for Trajectories

    • Marco A. Feliú, Mariano M. Moscato

    Pages 179-184

15. Static Value Analysis of Python Programs by Abstract Interpretation

    • Aymeric Fromherz, Abdelraouf Ouadjaout, Antoine Miné

    Pages 185-202

16. Model-Based Testing for General Stochastic Time

    • Marcus Gerhold, Arnd Hartmanns, Mariëlle Stoelinga

    Pages 203-219

17. Strategy Synthesis for Autonomous Agents Using PRISM

    • Ruben Giaquinta, Ruth Hoffmann, Murray Ireland, Alice Miller, Gethin Norman

    Pages 220-236

18. The Use of Automated Theory Formation in Support of Hazard Analysis

    • Andrew Ireland, Maria Teresa Llano, Simon Colton

    Pages 237-243

19. Distributed Model Checking Using ProB

    • Philipp Körner, Jens Bendisposto

    Pages 244-260

20. Optimal Storage of Combinatorial State Spaces

    • Alfons Laarman

    Pages 261-279

This book constitutes the proceedings of the 10th International Symposium on NASA Formal Methods, NFM 2018, held in Newport News, VA, USA, in April 2018.
The 24 full and 7 short papers presented in this volume were carefully reviewed and selected from 92 submissions. The papers focus on formal techniques and other approaches for software assurance, their theory, current capabilities and limitations, as well as their potential application to aerospace, robotics, and other NASA-relevant safety-critical systems during all stages of the software life-cycle.

• artificial intelligence
• automated theorem proving
• code generation
• computer software selection and evaluation
• distributed computer systems
• fault tolerance
• formal methods
• formal verification
• model checking
• problem solving
• programming languages
• real time systems
• run-time verification
• semantics
• software engineering
• specifications
• temporal logic
• verification

• NASA Langley Research Center, Hampton, USA

  Aaron Dutle, César Muñoz, Anthony Narkawicz

Policies and ethics