NASA Formal Methods

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