Skip to main content
SpringerLink
Log in
Book cover

NASA Formal Methods

Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011, Proceedings

  • Conference proceedings
  • © 2011

Overview

Editors:
  1. Mihaela Bobaru

    1. NASA Jet Propulsion Laboratory, Pasadena, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Klaus Havelund

    1. NASA Jet Propulsion Laboratory, Pasadena, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  3. Gerard J. Holzmann

    1. NASA Jet Propulsion Laboratory, Pasadena, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  4. Rajeev Joshi

    1. NASA Jet Propulsion Laboratory, Pasadena, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  • Fast track conference proceedings
  • Unique visibility
  • State of the art research

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

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

Included in the following conference series:

Conference proceedings info: NFM 2011.

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

  1. Front Matter

    Download chapter PDF

  2. Invited Talks

    1. From Retrospective Verification to Forward-Looking Development

      • K. Rustan M. Leino
      Pages 1-1

    2. Specifications for Free

      • Andreas Zeller
      Pages 2-12

  3. Invited Tutorials

    1. The Theory and Practice of SALT

      • Andreas Bauer, Martin Leucker
      Pages 13-40

    2. VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java

      • Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, Frank Piessens
      Pages 41-55

    3. Verifying Functional Correctness of C Programs with VCC

      • MichaÅ‚ Moskal
      Pages 56-57

  4. Regular Papers

    1. Bakar Kiasan: Flexible Contract Checking for Critical Systems Using Symbolic Execution

      • Jason Belt, John Hatcliff, Robby, Patrice Chalin, David Hardin, Xianghua Deng
      Pages 58-72

    2. Approximate Quantifier Elimination for Propositional Boolean Formulae

      • Jörg Brauer, Andy King
      Pages 73-88

    3. Towards Flight Control Verification Using Automated Theorem Proving

      • William Denman, Mohamed H. Zaki, Sofiène Tahar, Luis Rodrigues
      Pages 89-100

    4. Generalized Rabin(1) Synthesis with Applications to Robust System Synthesis

      • Rüdiger Ehlers
      Pages 101-115

    5. Integrating an Automated Theorem Prover into Agda

      • Simon Foster, Georg Struth
      Pages 116-130

    6. Efficient Predicate Abstraction of Program Summaries

      • Arie Gurfinkel, Sagar Chaki, Samir Sapra
      Pages 131-145

    7. Synthesis for PCTL in Parametric Markov Decision Processes

      • Ernst Moritz Hahn, Tingting Han, Lijun Zhang
      Pages 146-161

    8. Formalizing Probabilistic Safety Claims

      • Heber Herencia-Zapana, George Hagen, Anthony Narkawicz
      Pages 162-176

    9. The OpenTheory Standard Theory Library

      • Joe Hurd
      Pages 177-191

    10. Instantiation-Based Invariant Discovery

      • Temesghen Kahsai, Yeting Ge, Cesare Tinelli
      Pages 192-206

    11. Stuttering Mostly Speeds Up Solving Parity Games

      • Sjoerd Cranen, Jeroen J. A. Keiren, Tim A. C. Willemse
      Pages 207-221

    12. Counterexample-Based Error Localization of Behavior Models

      • Tsutomu Kumazawa, Tetsuo Tamai
      Pages 222-236

    13. Call Invariants

      • Shuvendu K. Lahiri, Shaz Qadeer
      Pages 237-251

    14. Symmetry for the Analysis of Dynamic Systems

      • Zarrin Langari, Richard Trefler
      Pages 252-266
Back to top

Other volumes

  1. NASA Formal Methods

Keywords

About this book

This book constitutes the refereed proceedings of the Third International Symposium on NASA Formal Methods, NFM 2011, held in Pasadena, CA, USA, in April 2011.
The 26 revised full papers presented together with 12 tool papers, 3 invited talks, and 2 invited tutorials were carefully reviewed and selected from 141 submissions. The topics covered by NFM 2011 included but were not limited to: theorem proving, logic model checking, automated testing and simulation, model-based engineering, real-time and stochastic systems, SAT and SMT solvers, symbolic execution, abstraction and abstraction refinement, compositional verification techniques; static and dynamic analysis techniques, fault protection, cyber security, specification formalisms, requirements analysis, and applications of formal techniques.

Editors and Affiliations

  • NASA Jet Propulsion Laboratory, Pasadena, USA

    Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann, Rajeev Joshi

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation