NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012, Proceedings

Front Cover
Alwyn Goodloe, Suzette Person
Springer Science & Business Media, Mar 27, 2012 - Computers - 466 pages
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.
 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

SMTBased Model Checking
1
Verified Software Toolchain
2
Formal Verification by Abstract Interpretation
3
Quantitative Timed Analysis of Interactive Markov Chains
8
Lessons Learnt from the Adoption of Formal ModelBased Development
24
Symbolic Execution of Communicating and Hierarchically Composed UMLRT State Machines
39
Inferring Definite Counterexamples through UnderApproximation
54
Modifying Test Suite Composition to Enable Effective PredicateLevel Statistical Debugging
70
Learning Markov Models for Stationary System Behaviors
216
The Use of Rippling to Automate EventB Invariant Preservation Proofs
231
ThreadModular Model Checking with Iterative Refinement
237
Towards LTL Model Checking of Unmodified ThreadBased C C++ Programs
252
Integrating Statechart Components in Polyglot
267
Using PVS to Investigate Incidents through the Lens of Distributed Cognition
273
Automated Analysis of Parametric TimingBased Mutual Exclusion Algorithms
279
Efficient Symbolic Execution of ValueBased Data Structures for Critical Systems
295

Rigorous Polynomial Approximation Using Taylor Models in Coq
85
Enhancing the Inverse Method with State Merging
100
ClassModular ClassEscape and Pointsto Analysis for ObjectOriented Languages
106
Testing Static Analyzers with Randomly Generated Programs
120
Compositional Verification of Architectural Models
126
A Safety Case Pattern for ModelBased Development Approach
141
PVS Linear Algebra Libraries for Verification of Control Software Algorithms in CACSL
147
A Controlled Language for Consistency Checking of Natural Language Temporal Requirements
162
Some Steps into Verification of Exact Real Arithmetic
168
Runtime Verification Meets Android Security
174
Specification in PDL with Recursion
181
An Empirical Study
195
Sound Formal Verification of Linuxs USB BP Keyboard Driver
210
Generating Verifiable Java Code from Verified PVS Specifications
310
Belief Bisimulation for Hidden Markov Models
326
Abstract Model Repair
341
ClosedLoop Symbolic Execution
356
On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols
371
Incremental Verification with Mode Variable Invariants in State Machines
388
A Semantic Analysis of Wireless Network Security Protocols
403
Runtime Verification with Predictive Semantics
418
A Case Study in Verification of Embedded Network Software
433
Checking and Distributing Statistical Model Checking
449
Author Index
464
Copyright

Other editions - View all

Common terms and phrases

Bibliographic information