Skip to main content
SpringerLink
Log in
Book cover

NASA Formal Methods

7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings

  • Conference proceedings
  • © 2015

Overview

Editors:
  1. Klaus Havelund

    1. Jet Propulsion Laboratory, Pasadena, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Gerard Holzmann

    1. Jet Propulsion Laboratory, Pasadena, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  3. Rajeev Joshi

    1. Jet Propulsion Laboratory, Pasadena, 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 9058)

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

Included in the following conference series:

Conference proceedings info: NFM 2015.

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

  1. Front Matter

    Pages I-XIII
    Download chapter PDF

  2. Invited Papers

    1. Front Matter

      Pages 1-1
      Download chapter PDF

    2. Moving Fast with Software Verification

      • Cristiano Calcagno, Dino Distefano, Jeremy Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca et al.
      Pages 3-11

    3. Developing Verified Software Using Leon

      • Viktor Kuncak
      Pages 12-15

  3. Regular Papers

    1. Front Matter

      Pages 17-17
      Download chapter PDF

    2. Timely Rollback: Specification and Verification

      • Martín Abadi, Michael Isard
      Pages 19-34

    3. Sum of Abstract Domains

      • Gianluca Amato, Simone Di Nardo Di Maio, Francesca Scozzari
      Pages 35-49

    4. Reachability Preservation Based Parameter Synthesis for Timed Automata

      • Étienne André, Giuseppe Lipari, Hoang Gia Nguyen, Youcheng Sun
      Pages 50-65

    5. Compositional Verification of Parameterised Timed Systems

      • Lăcrămioara Aştefănoaei, Souha Ben Rayana, Saddek Bensalem, Marius Bozga, Jacques Combaz
      Pages 66-81

    6. Requirements Analysis of a Quad-Redundant Flight Control System

      • John Backes, Darren Cofer, Steven Miller, Michael W. Whalen
      Pages 82-96

    7. Partial Order Reduction and Symmetry with Multiple Representatives

      • Dragan Bošnački, Mark Scheffer
      Pages 97-111

    8. Statistical Model Checking of Ad Hoc Routing Protocols in Lossy Grid Networks

      • Alice Dal Corso, Damiano Macedonio, Massimo Merro
      Pages 112-126

    9. Efficient Guiding Strategies for Testing of Temporal Properties of Hybrid Systems

      • Tommaso Dreossi, Thao Dang, Alexandre Donzé, James Kapinski, Xiaoqing Jin, Jyotirmoy V. Deshmukh
      Pages 127-142

    10. First-Order Transitive Closure Axiomatization via Iterative Invariant Injections

      • Aboubakr Achraf El Ghazi, Mana Taghdiri, Mihai Herda
      Pages 143-157

    11. Reachability Analysis Using Extremal Rates

      • Andrew N. Fisher, Chris J. Myers, Peng Li
      Pages 158-172

    12. Towards Realizability Checking of Contracts Using Theories

      • Andrew Gacek, Andreas Katis, Michael W. Whalen, John Backes, Darren Cofer
      Pages 173-187

    13. Practical Partial Order Reduction for CSP

      • Thomas Gibson-Robinson, Henri Hansen, A. W. Roscoe, Xu Wang
      Pages 188-203

    14. A Little Language for Testing

      • Alex Groce, Jervis Pinto
      Pages 204-218

    15. Detecting MPI Zero Buffer Incompatibility by SMT Encoding

      • Yu Huang, Eric Mercer
      Pages 219-233

    16. A Falsification View of Success Typing

      • Robert Jakob, Peter Thiemann
      Pages 234-247
Back to top

Other volumes

  1. NASA Formal Methods

Keywords

About this book

This book constitutes the refereed proceedings of the 7th International Symposium on NASA Formal Methods, NFM 2015, held in Pasadena, CA, USA, in April 2015.

The 24 revised regular papers presented together with 9 short papers were carefully reviewed and selected from 108 submissions. The topics include model checking, theorem proving; SAT and SMT solving; symbolic execution; static analysis; runtime verification; systematic testing; program refinement; compositional verification; security and intrusion detection; modeling and specification formalisms; model-based development; model-based testing; requirement engineering; formal approaches to fault tolerance; and applications of formal methods.

Editors and Affiliations

  • Jet Propulsion Laboratory, Pasadena, USA

    Klaus Havelund, Gerard Holzmann, Rajeev Joshi

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation