Skip to main content
SpringerLink
Log in

NASA Formal Methods

9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings

  • Conference proceedings
  • © 2017

Overview

Editors:
  1. Clark Barrett

    1. Stanford University, Palo Alto, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Misty Davies

    1. NASA Ames Research Center, Moffett Field, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  3. Temesghen Kahsai

    1. NASA Ames Research Center, Moffett Field, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 10227)

Part of the book sub series: Programming and Software Engineering (LNPSE)

Included in the following conference series:

Conference proceedings info: NFM 2017.

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (31 papers)

  1. Front Matter

    Pages I-XI
    Download chapter 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
Back to top

Other volumes

  1. NASA Formal Methods

Keywords

About this book

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.

Editors and Affiliations

  • Stanford University, Palo Alto, USA

    Clark Barrett

  • NASA Ames Research Center, Moffett Field, USA

    Misty Davies, Temesghen Kahsai

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation