NASA Formal Methods

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

  • Klaus Havelund
  • Gerard Holzmann
  • Rajeev Joshi
Conference proceedings NFM 2015

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

Also part of the Programming and Software Engineering book sub series (LNPSE, volume 9058)

Table of contents

  1. Front Matter
    Pages I-XIII
  2. Invited Papers

    1. Front Matter
      Pages 1-1
    2. Cristiano Calcagno, Dino Distefano, Jeremy Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca et al.
      Pages 3-11
    3. Viktor Kuncak
      Pages 12-15
  3. Regular Papers

    1. Front Matter
      Pages 17-17
    2. Martín Abadi, Michael Isard
      Pages 19-34
    3. Gianluca Amato, Simone Di Nardo Di Maio, Francesca Scozzari
      Pages 35-49
    4. Étienne André, Giuseppe Lipari, Hoang Gia Nguyen, Youcheng Sun
      Pages 50-65
    5. Lăcrămioara Aştefănoaei, Souha Ben Rayana, Saddek Bensalem, Marius Bozga, Jacques Combaz
      Pages 66-81
    6. John Backes, Darren Cofer, Steven Miller, Michael W. Whalen
      Pages 82-96
    7. Dragan Bošnački, Mark Scheffer
      Pages 97-111
    8. Alice Dal Corso, Damiano Macedonio, Massimo Merro
      Pages 112-126
    9. Tommaso Dreossi, Thao Dang, Alexandre Donzé, James Kapinski, Xiaoqing Jin, Jyotirmoy V. Deshmukh
      Pages 127-142
    10. Aboubakr Achraf El Ghazi, Mana Taghdiri, Mihai Herda
      Pages 143-157
    11. Andrew N. Fisher, Chris J. Myers, Peng Li
      Pages 158-172
    12. Andrew Gacek, Andreas Katis, Michael W. Whalen, John Backes, Darren Cofer
      Pages 173-187
    13. Thomas Gibson-Robinson, Henri Hansen, A. W. Roscoe, Xu Wang
      Pages 188-203
    14. Alex Groce, Jervis Pinto
      Pages 204-218
    15. Yu Huang, Eric Mercer
      Pages 219-233
    16. Robert Jakob, Peter Thiemann
      Pages 234-247
    17. Wenrui Meng, Junkil Park, Oleg Sokolsky, Stephanie Weirich, Insup Lee
      Pages 248-262
    18. Rajiv Murali, Andrew Ireland, Gudmund Grov
      Pages 263-278
    19. Anitha Murugesan, Michael W. Whalen, Neha Rungta, Oksana Tkachuk, Suzette Person, Mats P. E. Heimdahl et al.
      Pages 279-294
    20. Shashank Pathak, Erika Ábrahám, Nils Jansen, Armando Tacchella, Joost-Pieter Katoen
      Pages 295-309
    21. Daniel Schwartz-Narbonne, Martin Schäf, Dejan Jovanović, Philipp Rümmer, Thomas Wies
      Pages 327-342
    22. Holger Siegel, Axel Simon
      Pages 343-358
    23. Ahlem Triki, Borzoo Bonakdarpour, Jacques Combaz, Saddek Bensalem
      Pages 359-374
    24. Freek Verbeek, Oto Havle, Julien Schmaltz, Sergey Tverdyshev, Holger Blasum, Bruno Langenstein et al.
      Pages 375-389
  4. Short Papers

    1. Front Matter
      Pages 391-391
    2. Ivan Bocić, Tevfik Bultan
      Pages 393-399
    3. Luis M. Carril, Walter F. Tichy
      Pages 400-407
    4. Xin Chen, Stefan Schupp, Ibtissem Ben Makhlouf, Erika Ábrahám, Goran Frehse, Stefan Kowalewski
      Pages 408-414
    5. Jesús Aransay, Jose Divasón
      Pages 415-421
    6. Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey
      Pages 422-428
    7. Reza Hajisheykhi, Ali Ebnenasir, Sandeep S. Kulkarni
      Pages 429-435
    8. Marijn J. H. Heule, Martina Seidl, Armin Biere
      Pages 436-442
    9. Greg Eakman, Howard Reubenstein, Tom Hawkins, Mitesh Jain, Panagiotis Manolios
      Pages 443-449
    10. Olli Saarikivi, Keijo Heljanko
      Pages 450-456
  5. Back Matter
    Pages 457-458

About these proceedings


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.


Isabelle/HOL SAT solving Web application domain-specific language embedded systems fault analysis formal methods formal verification hybrid systems java model checking real-time systems simulation software engineering specification static analysis theorem proving timed automata use cases verification

Editors and affiliations

  • Klaus Havelund
    • 1
  • Gerard Holzmann
    • 2
  • Rajeev Joshi
    • 3
  1. 1.Jet Propulsion LaboratoryPasadenaUSA
  2. 2.Jet Propulsion LaboratoryPasadenaUSA
  3. 3.Jet Propulsion LaboratoryPasadenaUSA

Bibliographic information

  • DOI
  • Copyright Information Springer International Publishing Switzerland 2015
  • Publisher Name Springer, Cham
  • eBook Packages Computer Science Computer Science (R0)
  • Print ISBN 978-3-319-17523-2
  • Online ISBN 978-3-319-17524-9
  • Series Print ISSN 0302-9743
  • Series Online ISSN 1611-3349
  • Buy this book on publisher's site
Industry Sectors
Chemical Manufacturing
Finance, Business & Banking
IT & Software
Consumer Packaged Goods
Energy, Utilities & Environment