NASA formal methods : 8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings /: 8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings. (2016)

• Record Type: Book
• Other Titles: NFM 2016
• Further Information: Note: Edited by Sanjai Rayadurgam, Oksana Tkachuk.
• Editors: Rayadurgam, Sanjai; Tkachuk, Oksana
• Other Names: NFM (Symposium), 8th
• Contents: Requirements and Architectures -- Temporal Logic Framework for Performance Analysis of Architectures of Systems -- On Implementing Real-time Specification Patterns Using Observers -- Contract-Based Verification of Complex Time-Dependent Behaviors in Avionic Systems -- ARSENAL: Automatic Requirements Specification Extraction from Natural Language -- Testing and Run-time Enforcement -- Assisted Coverage Closure -- Synthesizing Runtime Enforcer of Safety Properties under Burst Error -- Compositional Runtime Enforcement -- Improving an Industrial Test Generation Tool using SMT Solver -- The comKorat Tool: Unified Combinatorial and Constraint-based Generation of Structurally Complex Tests -- Theorem Proving and Proofs -- Specification and Proof of High-Level Functional Properties of Bit-Level Programs -- Formal Verification of an Executable LTL Model Checker with Partial Order Reduction -- Verifying Relative Safety, Accuracy, and Termination for Program Approximations -- A Proof Infrastructure for Binary Programs.-Application of Formal Methods -- A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles -- Probabilistic Formal Verification of the SATS Concept of Operation -- Formal Translation of IEC 61131-3 Function Block Diagrams to PVS with Nuclear Application -- Formal Analysis of Extended Well-Clear Boundaries for Unmanned Aircraft -- Formal Validation and Verification Framework and Models for Model-Based and Adaptive Control Systems -- Code Generation and Synthesis -- Automated Synthesis of Safe Autonomous Vehicle Control Under Perception Uncertainty -- Obfuscator Synthesis for Privacy and Utility -- Code Generation Using A Formal Model of Reference Counting -- EventB2Java: A Code Generator for Event-B -- Model Checking and Verification -- A Modular Way to Reason About Iteration -- Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Reachability Analysis -- Gray-box Learning of Serial Compositions of Mealy Machines -- Hierarchical Verification of Quantum Circuits -- Correctness and Certification -- Semantics for Locking Specifications -- From Design Contracts to Component Requirements Verification -- A Hybrid Architecture for Correct-by-Construction Hybrid Planning and Control.
• Publisher Details: Switzerland : Springer
• Publication Date: 2016
• Extent: 1 online resource (xix, 396 pages), illustrations
• Subjects: 004.01/51; Computer science; Formal methods (Computer science) -- Congresses; Formal methods (Computer science); Computers -- Programming Languages -- General; Mathematics -- Logic; Computers -- Operating Systems -- General; Computers -- Programming -- General; Programming & scripting languages: general; Mathematical theory of computation; Operating systems; Computer programming / software development; Software engineering; Operating systems (Computers); Logic design; Computers -- Software Development & Engineering -- General; Software Engineering; Electronic books; Conference papers and proceedings; Electronic books
• Languages: English
• ISBNs: 9783319406480; 3319406485; 3319406477; 9783319406473
• Related ISBNs: 9783319406473
• Notes: Note: Online resource; title from PDF title page (SpringerLink, viewed June 14, 2016).
• Access Rights: Legal Deposit; Only available on premises controlled by the deposit library and to one user at any one time; The Legal Deposit Libraries (Non-Print Works) Regulations (UK).
• Access Usage: Restricted: Printing from this resource is governed by The Legal Deposit Libraries (Non-Print Works) Regulations (UK) and UK copyright law currently in force.