NASA Formal Methods

SMT-Based Model Checking.-Verified Software Toolchain (Abstract).-Formal Verification by Abstract Interpretation.-Quantitative Timed Analysis of Interactive Markov Chains .-Lessons Learnt from the Adoption of Formal Model-Based Development .-Symbolic Execution of Communicating and Hierarchically Composed UML-RT State Machines .-Inferring Definite Counterexamples through Under-Approximation .-Modifying Test Suite Composition to Enable Effective Predicate-Level Statistical Debugging.-Rigorous Polynomial Approximation Using Taylor Models in COQ.-Enhancing the Inverse Method with State Merging.-Class-Modular, Class-Escape and Points-to Analysis for Object-Oriented Languages.-Testing Static Analyzers with Randomly Generated Programs.-Compositional Verification of Architectural Models.-A Safety Case Pattern for Model-Based Development Approach.-PVS Linear Algebra Libraries for Verification of Control Software Algorithms in C/ACSL .-Temporal Action Language (TAL): A Controlled Language for Consistency Checking of Natural Language Temporal Requirements (Preliminary Results) .-Some Steps into Verification of Exact Real Arithmetic.-Runtime Verification Meets Android Security .-Specification in PDL with Recursion.-Automatically Proving Thousands of Verification Conditions Using an SMT Solver: An Empirical Study .-Sound Formal Verification of Linux’s USB BP Keyboard Driver .-Learning Markov Models for Stationary System Behaviors .-The Use of Rippling to Automate Event-B Invariant Preservation Proofs .-Thread-Modular Model Checking with Iterative Refinement .-Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs .-Integrating Statechart Components in Polyglot .-Using PVS to Investigate Incidents through the Lens of Distributed Cognition.-Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms.-Efficient Symbolic Execution of Value-Based Data Structures for Critical Systems.-Generating Verifiable Java Code from Verified PVS Specifications.-Belief Bisimulation for Hidden Markov Models: Logical Characterisation and Decision Algorithm.-Abstract Model Repair .-CLSE: Closed-Loop Symbolic Execution .-On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols.-Incremental Verification with Mode Variable Invariants in State Machines .-A Semantic Analysis of Wireless Network Security Protocols.-Runtime Verification with Predictive Semantics .-A Case Study in Verification of Embedded Network Software.-Checking and Distributing Statistical Model Checking.-