NASA Formal Methods

1. Front Matter

   Pages I-XI

   PDF

2. An Automata-Theoretic Approach to Modeling Systems and Specifications over Infinite Data

   • Hadar Frenkel, Orna Grumberg, Sarai Sheinvald

   Pages 1-18

3. Learning from Faults: Mutation Testing in Active Automata Learning

   • Bernhard K. Aichernig, Martin Tappler

   Pages 19-34

4. Parametric Model Checking Timed Automata Under Non-Zenoness Assumption

   • Étienne André, Hoang Gia Nguyen, Laure Petrucci, Jun Sun

   Pages 35-51

5. Multi-timed Bisimulation for Distributed Timed Automata

   • James Ortiz, Moussa Amrani, Pierre-Yves Schobbens

   Pages 52-67

6. Auto-Active Proof of Red-Black Trees in SPARK

   • Claire Dross, Yannick Moy

   Pages 68-83

7. Analysing Security Protocols Using Refinement in iUML-B

   • Colin Snook, Thai Son Hoang, Michael Butler

   Pages 84-98

8. On Learning Sparse Boolean Formulae for Explaining AI Decisions

   • Susmit Jha, Vasumathi Raman, Alessandro Pinto, Tuhin Sahai, Michael Francis

   Pages 99-114

9. Event-Based Runtime Verification of Temporal Properties Using Time Basic Petri Nets

   • Matteo Camilli, Angelo Gargantini, Patrizia Scandurra, Carlo Bellettini

   Pages 115-130

10. Model-Counting Approaches for Nonlinear Numerical Constraints

    • Mateus Borges, Quoc-Sang Phan, Antonio Filieri, Corina S. Păsăreanu

    Pages 131-138

11. Input Space Partitioning to Enable Massively Parallel Proof

    • Ashlie B. Hocking, M. Anthony Aiello, John C. Knight, Nikos Aréchiga

    Pages 139-145

12. Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations

    • Hugo Daniel Macedo, Alessandro Fantechi, Anne E. Haxthausen

    Pages 146-162

13. Modular Model-Checking of a Byzantine Fault-Tolerant Protocol

    • Benjamin F. Jones, Lee Pike

    Pages 163-177

14. Improved Learning for Stochastic Timed Models by State-Merging Algorithms

    • Braham Lotfi Mediouni, Ayoub Nouri, Marius Bozga, Saddek Bensalem

    Pages 178-193

15. Verifying Safety and Persistence Properties of Hybrid Systems Using Flowpipes and Continuous Invariants

    • Andrew Sogokon, Paul B. Jackson, Taylor T. Johnson

    Pages 194-211

16. A Relational Shape Abstract Domain

    • Hugo Illous, Matthieu Lemerre, Xavier Rival

    Pages 212-229

17. Floating-Point Format Inference in Mixed-Precision

    • Matthieu Martel

    Pages 230-246

18. A Verification Technique for Deterministic Parallel Programs

    • Saeed Darabi, Stefan C. C. Blom, Marieke Huisman

    Pages 247-264

19. Systematic Predicate Abstraction Using Variable Roles

    • Yulia Demyanova, Philipp Rümmer, Florian Zuleger

    Pages 265-281

20. specgen: A Tool for Modeling Statecharts in CSP

    • Brandon Shapiro, Chris Casinghino

    Pages 282-287

This book constitutes the proceedings of the 9th International Symposium on NASA Formal Methods, NFM 2017, held in Moffett Field, CA, USA, in May 2017.

The 23 full and 8 short papers presented in this volume were carefully reviewed and selected from 77 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.

• automata theory
• logic and verification
• model checking
• abstract interpretation
• application of formal methods
• quantitative analysis
• static analysis
• proofs and certificate
• formal requirements
• formal verification
• formal specification
• formal methods
• timed automata
• natural language
• machine learning
• separation logic
• algorithms
• static analysis
• algorithm analysis and problem complexity

• Stanford University, Palo Alto, USA

  Clark Barrett

• NASA Ames Research Center, Moffett Field, USA

  Misty Davies, Temesghen Kahsai

Policies and ethics