Days: Tuesday, June 4th Wednesday, June 5th Thursday, June 6th
View this program: with abstractssession overviewtalk overview
8:30: Safety Briefing
8:35: Welcome from NASA Leadership
8:45: Welcome from NFM Chairs
Autonomy Challenges for Future NASA Science and Exploration Missions
Butler Hine NASA Ames Research Center
| 10:30 | Structure-guided Cube-and-conquer for MaxSAT (abstract) PRESENTER: Max Bannach |
| 10:55 | Tackling the polarity initialization problem in SAT solving using a genetic algorithm (abstract) PRESENTER: Sabrine Saouli |
| 11:20 | Formalization of asymptotic convergence for Stationary Iterative Methods (abstract) PRESENTER: Jean-Baptiste Jeannin |
| 11:45 | Distributional Probabilistic Model Checking (abstract) PRESENTER: Lu Feng |
Session Chair: Douglas Smith
| 14:00 | Quantitative Input Usage Static Analysis (abstract) PRESENTER: Denis Mazzucato |
| 14:25 | Verifying a C implementation of Derecho's coordination mechanism using VST and Coq (abstract) PRESENTER: Ramana Nagasamudram |
| 14:50 | Verification of Scapegoat Trees using Dafny (abstract) PRESENTER: Jiapeng Wang |
| 15:15 | Real Arithmetic in TLAPM (abstract) PRESENTER: Ovini V.W. Gunasekera |
| 16:00 | Model Refinement (abstract) PRESENTER: Douglas Smith |
| 16:25 | Symmetry-based Abstraction Algorithm for Accelerating Symbolic Control Synthesis (abstract) PRESENTER: Hussein Sibai |
| 16:50 | SMT-Based Aircraft Conflict Detection and Elimination (abstract) PRESENTER: Saswata Paul |
View this program: with abstractssession overviewtalk overview
Formal Verification and Run-time Monitoring for Learning-Enabled Autonomous Systems
Corina S. Pasareanu Carnegie Mellon University Silicon Valley, NASA Ames Research Center
| 10:30 | Towards formal verification of neural networks in cyber-physical systems (abstract) PRESENTER: Federico Rossi |
| 10:55 | Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems (abstract) PRESENTER: Yuhao Zhou |
| 11:20 | Approximate Conformance Verification of Deep Neural Networks (abstract) PRESENTER: Habeeb P |
Participants in the Tools Demonstration Session will give a 5 minute lightning talk to introduce their tools.
Panel: Trusted Autonomy for Space and Aviation
Guillaume P. Brat NASA Ames Research Center, Huafeng Yu U.S. Department of Transportation, Darren Cofer Collins Aerospace, Marco Pavone Stanford, Jean-Guillaume Durand Xwing
The panel will discuss challenges associated with the verification and validation (V&V) of machine learning components in critical systems in domains including aviation, automotive, space, and many others.
View this program: with abstractssession overviewtalk overview
Safety under uncertainty: Automotive standards for AI safety and research perspectives
Simon Burton, Centre for Assuring Autonomy, University of York, UK
| 10:30 | Tree-Based Scenario Classification. A Formal Framework for Measuring Domain Coverage when Testing Autonomous Systems (abstract) PRESENTER: Till Schallau |
| 10:55 | Validation of Reinforcement Learning Agents and Safety Shields with ProB (abstract) PRESENTER: Fabian Vu |
| 11:20 | Contract-driven Runtime Adaptation (abstract) PRESENTER: Eunsuk Kang |
| 11:45 | Topllet: An Optimized Engine for Answering Metric Temporal Conjunctive Queries (abstract) PRESENTER: Lukas Westhofen |
| 12:00 | A Formal Verification Framework for Runtime Assurance (abstract) PRESENTER: Lauren White |
| 14:00 | Robotics: A New Mission for FRET Requirements (abstract) PRESENTER: Anastasia Mavridou |
| 14:25 | The Control Barrier Function Toolbox (abstract) PRESENTER: Andrew Schoer |
| 14:40 | SMT-Based Dynamic Multi-Robot Task Allocation (abstract) PRESENTER: Victoria Marie Tuck |
| 15:05 | Safe Planning through Incremental Decomposition of Signal Temporal Logic Specifications (abstract) PRESENTER: Parv Kapoor |
| 16:00 | Structuring Formal Methods into the Undergraduate Computer Science Curriculum (abstract) PRESENTER: Ramnath Sarnath |
| 16:15 | Integrated Contract-based Unit and System Testing for Component-based Systems (abstract) PRESENTER: Jason Belt |
| 16:40 | Verifying PLC Programs via Monitors: Extending the Integration of FRET and PLCverif (abstract) PRESENTER: Xaver Fink |