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
- Title:
- 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)
- Main Title:
- NASA formal methods : 8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings
- 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 -- CodeRequirements 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. … (more)
- 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.
- View Content:
- Available online (eLD content is only available in our Reading Rooms) ↗
- Physical Locations:
- British Library HMNTS - ELD.DS.356486
- Ingest File:
- 01_317.xml