Skip to main content
SpringerLink
Log in
Book cover

NASA Formal Methods

6th International Symposium, NFM 2014, Houston, TX, USA, April 29 - May 1, 2014. Proceedings

  • Conference proceedings
  • © 2014

Overview

Editors:
  1. Julia M. Badger

    1. NASA, Houston, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Kristin Yvonne Rozier

    1. Intelligent Systems Division, 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 8430)

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

Included in the following conference series:

Conference proceedings info: NFM 2014.

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 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 (29 papers)

  1. Front Matter

    Download chapter PDF

  2. DO-333 Certification Case Studies

    • Darren Cofer, Steven Miller
    Pages 1-15

  3. A Compositional Monitoring Framework for Hard Real-Time Systems

    • André de Matos Pedro, David Pereira, Luís Miguel Pinho, Jorge Sousa Pinto
    Pages 16-30

  4. Leadership Election: An Industrial SoS Application of Compositional Deadlock Verification

    • Pedro R. G. Antonino, Marcel Medeiros Oliveira, Augusto C. A. Sampaio, Klaus E. Kristensen, Jeremy W. Bryans
    Pages 31-45

  5. Verification of Certifying Computations through AutoCorres and Simpl

    • Lars Noschinski, Christine Rizkallah, Kurt Mehlhorn
    Pages 46-61

  6. Distinguishing Sequences for Partially Specified FSMs

    • Robert M. Hierons, Uraz Cengiz Türker
    Pages 62-76

  7. On Proving Recoverability of Smart Electrical Grids

    • Seppo Horsmanheimo, Maryam Kamali, Mikko Kolehmainen, Mats Neovius, Luigia Petre, Mauno Rönkkö et al.
    Pages 77-91

  8. Providing Early Warnings of Specification Problems

    • Dustin Hoffman, Aditi Tagore, Diego Zaccai, Bruce W. Weide
    Pages 92-97

  9. Mechanized, Compositional Verification of Low-Level Code

    • Björn Bartels, Nils Jähnig
    Pages 98-112

  10. Formally Verified Computation of Enclosures of Solutions of Ordinary Differential Equations

    • Fabian Immler
    Pages 113-127

  11. On the Quantum Formalization of Coherent Light in HOL

    • Mohamed Yousri Mahmoud, Sofiène Tahar
    Pages 128-142

  12. Refinement Types for tla  + 

    • Stephan Merz, Hernán Vanzetto
    Pages 143-157

  13. Using Lightweight Theorem Proving in an Asynchronous Systems Context

    • Matthew Danish, Hongwei Xi
    Pages 158-172

  14. JKelloy: A Proof Assistant for Relational Specifications of Java Programs

    • Aboubakr Achraf El Ghazi, Mattias Ulbrich, Christoph Gladisch, Shmuel Tyszberowicz, Mana Taghdiri
    Pages 173-187

  15. Verifying Hybrid Systems Involving Transcendental Functions

    • Paul Jackson, Andrew Sogokon, James Bridge, Lawrence Paulson
    Pages 188-202

  16. Verifying Nonpolynomial Hybrid Systems by Qualitative Abstraction and Automated Theorem Proving

    • William Denman
    Pages 203-208

  17. Combining PVSio with Stateflow

    • Paolo Masci, Yi Zhang, Paul Jones, Patrick Oladimeji, Enrico D’Urso, Cinzia Bernardeschi et al.
    Pages 209-214

  18. Qed. Computing What Remains to Be Proved

    • Loïc Correnson
    Pages 215-229

  19. Warps and Atomics: Beyond Barrier Synchronization in the Verification of GPU Kernels

    • Ethel Bardsley, Alastair F. Donaldson
    Pages 230-245

  20. Testing-Based Compiler Validation for Synchronous Languages

    • Pierre-Loïc Garoche, Falk Howar, Temesghen Kahsai, Xavier Thirioux
    Pages 246-251
Back to top

Other volumes

  1. NASA Formal Methods

Keywords

About this book

This book constitutes the refereed proceedings of the 6th International Symposium on NASA Formal Methods, NFM 2014, held in Houston, TX, USA, April 29 – May 1, 2014. The 20 revised regular papers presented together with 9 short papers were carefully reviewed and selected from 107 submissions. The topics include model checking, theorem proving, static analysis, model-based development, runtime monitoring, formal approaches to fault tolerance, applications of formal methods to aerospace systems, formal analysis of cyber-physical systems, including hybrid and embedded systems, formal methods in systems engineering, modeling, requirements and specifications, requirements generation, specification debugging, formal validation of specifications, use of formal methods in safety cases, use of formal methods in human-machine interaction analysis, formal methods for parallel hardware implementations, use of formal methods in automated software engineering and testing, correct-by-design, design for verification, and property based design techniques, techniques and algorithms for scaling formal methods, e.g., abstraction and symbolic methods, compositional techniques, parallel and distributed techniques, and application of formal methods to emerging technologies.

Editors and Affiliations

  • NASA, Houston, USA

    Julia M. Badger

  • Intelligent Systems Division, NASA Ames Research Center, Moffett Field, USA

    Kristin Yvonne Rozier

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation