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 |