دانلود کتاب NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings

فهرست مطالب :

Front Matter....Pages -
SMT-Based Model Checking....Pages 1-1
Verified Software Toolchain....Pages 2-2
Formal Verification by Abstract Interpretation....Pages 3-7
Quantitative Timed Analysis of Interactive Markov Chains....Pages 8-23
Lessons Learnt from the Adoption of Formal Model-Based Development....Pages 24-38
Symbolic Execution of Communicating and Hierarchically Composed UML-RT State Machines....Pages 39-53
Inferring Definite Counterexamples through Under-Approximation....Pages 54-69
Modifying Test Suite Composition to Enable Effective Predicate-Level Statistical Debugging....Pages 70-84
Rigorous Polynomial Approximation Using Taylor Models in Co q ....Pages 85-99
Enhancing the Inverse Method with State Merging....Pages 100-105
Class-Modular, Class-Escape and Points-to Analysis for Object-Oriented Languages....Pages 106-119
Testing Static Analyzers with Randomly Generated Programs....Pages 120-125
Compositional Verification of Architectural Models....Pages 126-140
A Safety Case Pattern for Model-Based Development Approach....Pages 141-146
PVS Linear Algebra Libraries for Verification of Control Software Algorithms in C/ACSL....Pages 147-161
Temporal Action Language (TAL): A Controlled Language for Consistency Checking of Natural Language Temporal Requirements....Pages 162-167
Some Steps into Verification of Exact Real Arithmetic....Pages 168-173
Runtime Verification Meets Android Security....Pages 174-180
Specification in PDL with Recursion....Pages 181-194
Automatically Proving Thousands of Verification Conditions Using an SMT Solver: An Empirical Study....Pages 195-209
Sound Formal Verification of Linux’s USB BP Keyboard Driver....Pages 210-215
Learning Markov Models for Stationary System Behaviors....Pages 216-230
The Use of Rippling to Automate Event-B Invariant Preservation Proofs....Pages 231-236
Thread-Modular Model Checking with Iterative Refinement....Pages 237-251
Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs....Pages 252-266
Integrating Statechart Components in Polyglot....Pages 267-272
Using PVS to Investigate Incidents through the Lens of Distributed Cognition....Pages 273-278
Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms....Pages 279-294
Efficient Symbolic Execution of Value-Based Data Structures for Critical Systems....Pages 295-309
Generating Verifiable Java Code from Verified PVS Specifications....Pages 310-325
Belief Bisimulation for Hidden Markov Models....Pages 326-340
Abstract Model Repair....Pages 341-355
CLSE: Closed-Loop Symbolic Execution....Pages 356-370
On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols....Pages 371-387
Incremental Verification with Mode Variable Invariants in State Machines....Pages 388-402
A Semantic Analysis of Wireless Network Security Protocols....Pages 403-417
Runtime Verification with Predictive Semantics....Pages 418-432
A Case Study in Verification of Embedded Network Software....Pages 433-448
Checking and Distributing Statistical Model Checking....Pages 449-463
Back Matter....Pages -