NASA Formal Methods

1. Front Matter

   PDF

2. SMT-Based Model Checking

   • Cesare Tinelli

   Pages 1-1

3. Verified Software Toolchain

   • Andrew W. Appel

   Pages 2-2

4. Formal Verification by Abstract Interpretation

   • Patrick Cousot

   Pages 3-7

5. Quantitative Timed Analysis of Interactive Markov Chains

   • Dennis Guck, Tingting Han, Joost-Pieter Katoen, Martin R. Neuhäußer

   Pages 8-23

6. Lessons Learnt from the Adoption of Formal Model-Based Development

   • Alessio Ferrari, Alessandro Fantechi, Stefania Gnesi

   Pages 24-38

7. Symbolic Execution of Communicating and Hierarchically Composed UML-RT State Machines

   • Karolina Zurowska, Juergen Dingel

   Pages 39-53

8. Inferring Definite Counterexamples through Under-Approximation

   • Jörg Brauer, Axel Simon

   Pages 54-69

9. Modifying Test Suite Composition to Enable Effective Predicate-Level Statistical Debugging

   • Ross Gore, Paul F. Reynolds Jr.

   Pages 70-84

10. Rigorous Polynomial Approximation Using Taylor Models in Coq

    • Nicolas Brisebarre, Mioara Joldeş, Érik Martin-Dorel, Micaela Mayero, Jean-Michel Muller, Ioana Paşca et al.

    Pages 85-99

11. Enhancing the Inverse Method with State Merging

    • Étienne André, Laurent Fribourg, Romain Soulat

    Pages 100-105

12. Class-Modular, Class-Escape and Points-to Analysis for Object-Oriented Languages

    • Alexander Herz, Kalmer Apinis

    Pages 106-119

13. Testing Static Analyzers with Randomly Generated Programs

    • Pascal Cuoq, Benjamin Monate, Anne Pacalet, Virgile Prevosto, John Regehr, Boris Yakobowski et al.

    Pages 120-125

14. Compositional Verification of Architectural Models

    • Darren Cofer, Andrew Gacek, Steven Miller, Michael W. Whalen, Brian LaValley, Lui Sha

    Pages 126-140

15. A Safety Case Pattern for Model-Based Development Approach

    • Anaheed Ayoub, BaekGyu Kim, Insup Lee, Oleg Sokolsky

    Pages 141-146

16. PVS Linear Algebra Libraries for Verification of Control Software Algorithms in C/ACSL

    • Heber Herencia-Zapana, Romain Jobredeaux, Sam Owre, Pierre-Loïc Garoche, Eric Feron, Gilberto Perez et al.

    Pages 147-161

17. Temporal Action Language (TAL): A Controlled Language for Consistency Checking of Natural Language Temporal Requirements

    • Wenbin Li, Jane Huffman Hayes, Mirosław Truszczyński

    Pages 162-167

18. Some Steps into Verification of Exact Real Arithmetic

    • Norbert Th. Müller, Christian Uhrhan

    Pages 168-173

19. Runtime Verification Meets Android Security

    • Andreas Bauer, Jan-Christoph Küster, Gil Vegliach

    Pages 174-180

20. Specification in PDL with Recursion

    • Xinxin Liu, Bingtian Xue

    Pages 181-194

This book constitutes the refereed proceedings of the Fourth International Symposium on NASA Formal Methods, NFM 2012, held in Norfolk, VA, USA, in April 2012. The 36 revised regular papers presented together with 10 short papers, 3 invited talks were carefully reviewed and selected from 93 submissions. The topics are organized in topical sections on theorem proving, symbolic execution, model-based engineering, real-time and stochastic systems, model checking, 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.

• cyber security
• formal techniques
• formalism
• model checking
• symbolic execution

• NASA Langley Research Center, Hampton, USA

  Alwyn E. Goodloe, Suzette Person

Policies and ethics