NASA Formal Methods
Editat de Alwyn Goodloe, Suzette Personen Limba Engleză Paperback – 27 mar 2012
Preț: 330.36 lei
Preț vechi: 412.95 lei
-20% Nou
Puncte Express: 496
Preț estimativ în valută:
58.46€ • 68.17$ • 51.33£
58.46€ • 68.17$ • 51.33£
Carte tipărită la comandă
Livrare economică 16-30 ianuarie 26
Preluare comenzi: 021 569.72.76
Specificații
ISBN-13: 9783642288906
ISBN-10: 3642288901
Pagini: 480
Ilustrații: XII, 466 p. 79 illus.
Dimensiuni: 155 x 235 x 26 mm
Greutate: 0.72 kg
Ediția:2012
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
ISBN-10: 3642288901
Pagini: 480
Ilustrații: XII, 466 p. 79 illus.
Dimensiuni: 155 x 235 x 26 mm
Greutate: 0.72 kg
Ediția:2012
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
Public țintă
ResearchCuprins
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 PVSSpecifications.-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.-
Caracteristici
Fast-track conference proceedings State-of-the-art research Up-to-date results