NASA Formal Methods

Front Matter....Pages I-XI
An Automata-Theoretic Approach to Modeling Systems and Specifications over Infinite Data....Pages 1-18
Learning from Faults: Mutation Testing in Active Automata Learning....Pages 19-34
Parametric Model Checking Timed Automata Under Non-Zenoness Assumption....Pages 35-51
Multi-timed Bisimulation for Distributed Timed Automata....Pages 52-67
Auto-Active Proof of Red-Black Trees in SPARK....Pages 68-83
Analysing Security Protocols Using Refinement in iUML-B....Pages 84-98
On Learning Sparse Boolean Formulae for Explaining AI Decisions....Pages 99-114
Event-Based Runtime Verification of Temporal Properties Using Time Basic Petri Nets....Pages 115-130
Model-Counting Approaches for Nonlinear Numerical Constraints....Pages 131-138
Input Space Partitioning to Enable Massively Parallel Proof....Pages 139-145
Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations....Pages 146-162
Modular Model-Checking of a Byzantine Fault-Tolerant Protocol....Pages 163-177
Improved Learning for Stochastic Timed Models by State-Merging Algorithms....Pages 178-193
Verifying Safety and Persistence Properties of Hybrid Systems Using Flowpipes and Continuous Invariants....Pages 194-211
A Relational Shape Abstract Domain....Pages 212-229
Floating-Point Format Inference in Mixed-Precision....Pages 230-246
A Verification Technique for Deterministic Parallel Programs....Pages 247-264
Systematic Predicate Abstraction Using Variable Roles....Pages 265-281
HyPro: A C++ Library of State Set Representations for Hybrid Systems Reachability Analysis....Pages 282-287
SPEN: A Solver for Separation Logic....Pages 288-294
From Hazard Analysis to Hazard Mitigation Planning: The Automated Driving Case....Pages 295-301
Event-B at Work: Some Lessons Learnt from an Application to a Robot Anti-collision Function....Pages 302-309
Reasoning About Safety-Critical Information Flow Between Pilot and Computer....Pages 310-326
Compositional Falsification of Cyber-Physical Systems with Machine Learning Components....Pages 327-341
Verifying a Class of Certifying Distributed Programs....Pages 342-356
Compact Proof Witnesses....Pages 357-372
Qualification of a Model Checker for Avionics Software Verification....Pages 373-388
SpeAR v2.0: Formalized Past LTL Specification and Analysis of Requirements....Pages 389-403
Just Formal Enough? Automated Analysis of EARS Requirements....Pages 404-419
Back Matter....Pages 420-426
....Pages 427-434