Blick ins Buch

NASA Formal Methods

4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012, Proceedings

Alwyn Goodloe, Suzette Person (Herausgeber)

Buch | Softcover

XII, 466 Seiten

2012
Springer Berlin (Verlag)
978-3-642-28890-6 (ISBN)

Lese- und Medienproben

Inhaltsverzeichnis (PDF)
Blick ins Buch (midvox)

Artikel merken

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.

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
Reihe/Serie	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