NASA Formal Methods

1. Front Matter

   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

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.

• automated reasoning
• concurrency
• requirements analysis
• software verification
• validation

• NASA Jet Propulsion Laboratory, Pasadena, USA

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

Policies and ethics