NASA Formal Methods
Springer Berlin (Verlag)
978-3-642-28890-6 (ISBN)
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.-
Erscheint lt. Verlag | 27.3.2012 |
---|---|
Reihe/Serie | Lecture Notes in Computer Science | Programming and Software Engineering |
Zusatzinfo | XII, 466 p. 79 illus. |
Verlagsort | Berlin |
Sprache | englisch |
Gewicht | 720 g |
Themenwelt | Mathematik / Informatik ► Informatik ► Betriebssysteme / Server |
Mathematik / Informatik ► Informatik ► Programmiersprachen / -werkzeuge | |
Mathematik / Informatik ► Informatik ► Software Entwicklung | |
Schlagworte | cyber security • Formalism • Formal Techniques • Model Checking • symbolic execution |
ISBN-10 | 3-642-28890-1 / 3642288901 |
ISBN-13 | 978-3-642-28890-6 / 9783642288906 |
Zustand | Neuware |
Haben Sie eine Frage zum Produkt? |
aus dem Bereich