NASA Formal Methods: 7th International Symposium, Nfm 2015, Pasadena, Ca, Usa, April 27-29, 2015, Proceedings by Klaus HavelundNASA Formal Methods: 7th International Symposium, Nfm 2015, Pasadena, Ca, Usa, April 27-29, 2015, Proceedings by Klaus Havelund

NASA Formal Methods: 7th International Symposium, Nfm 2015, Pasadena, Ca, Usa, April 27-29, 2015…

byKlaus HavelundEditorGerard Holzmann, Rajeev Joshi

Paperback | April 9, 2015

Pricing and Purchase Info

$104.74 online 
$110.50 list price save 5%
Earn 524 plum® points

Prices and offers may vary in store

Quantity:

In stock online

Ships free on orders over $25

Not available in stores

about

This book constitutes the refereed proceedings of the 7th International Symposium on NASA Formal Methods, NFM 2015, held in Pasadena, CA, USA, in April 2015.

The 24 revised regular papers presented together with 9 short papers were carefully reviewed and selected from 108 submissions. The topics include model checking, theorem proving; SAT and SMT solving; symbolic execution; static analysis; runtime verification; systematic testing; program refinement; compositional verification; security and intrusion detection; modeling and specification formalisms; model-based development; model-based testing; requirement engineering; formal approaches to fault tolerance; and applications of formal methods.

Title:NASA Formal Methods: 7th International Symposium, Nfm 2015, Pasadena, Ca, Usa, April 27-29, 2015…Format:PaperbackDimensions:458 pagesPublished:April 9, 2015Publisher:Springer-Verlag/Sci-Tech/TradeLanguage:English

The following ISBNs are associated with this title:

ISBN - 10:3319175238

ISBN - 13:9783319175232

Look for similar items by category:

Reviews

Table of Contents

Moving Fast with Software Verification.- Developing Verified Software Using Leon.- Timely Rollback: Specification and Verification.- Sum of Abstract Domains.- Reachability Preservation Based Parameter Synthesis for Timed Automata.- Compositional Verification of Parameterised Timed Systems.- Requirements Analysis of a Quad-Redundant Flight Control System.- Partial Order Reduction and Symmetry with Multiple Representatives.- Statistical Model Checking of Ad Hoc Routing Protocols in Lossy Grid Networks.- Efficient Guiding Strategies for Testing of Temporal Properties of Hybrid Systems.- First-Order Transitive Closure Axiomatization via Iterative Invariant Injections.- Reachability Analysis Using Extremal Rates.- Towards Realizability Checking of Contracts Using Theories.- Practical Partial Order Reduction for CSP.- A Little Language for Testing.- Detecting MPI Zero Buffer Incompatibility by SMT Encoding.- A Falsification View of Success Typing.- Verified ROS-Based Deployment of Platform-Independent Control Systems.- A Rigorous Approach to Combining Use Case Modelling and Accident Scenarios.- Are We There Yet? Determining the Adequacy of Formalized Requirements and Test Suites.- A Greedy Approach for the Efficient Repair of Stochastic Models.- Integrating SMT with Theorem Proving for Analog/Mixed-Signal Circuit Verification.- Conflict-Directed Graph Coverage.- Shape Analysis with Connectors.- Automated Conflict-Free Concurrent Implementation of Timed Component-Based Models.- Formal API Specification of the PikeOS Separation Kernel.- Data Model Bugs.- Predicting and Witnessing Data Races Using CSP.- A Benchmark Suite for Hybrid Systems Reachability Analysis.- Generalizing a Mathematical Analysis Library in Isabelle/HOL.- A Tool for Intersecting Context-Free Grammars and Its Applications.- UFIT: A Tool for Modeling Faults in UPPAAL Timed Automata.- Blocked Literals Are Universal.- Practical Formal Verification of Domain-Specific Language Applications.- Reporting Races in Dynamic Partial Order Reduction.