NFM 2024: 16TH NASA FORMAL METHODS SYMPOSIUM
PROGRAM

Days: Tuesday, June 4th Wednesday, June 5th Thursday, June 6th

Tuesday, June 4th

View this program: with abstractssession overviewtalk overview

08:30-09:00 Session 1: Welcome Session

8:30: Safety Briefing

8:35: Welcome from NASA Leadership

8:45: Welcome from NFM Chairs

09:00-10:00 Session 2: Keynote Talk #1

Autonomy Challenges for Future NASA Science and Exploration Missions

Butler Hine NASA Ames Research Center

10:00-10:30Coffee Break
10:30-12:30 Session 3: Advances in Solver Technology
Chair:
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)
11:45
Distributional Probabilistic Model Checking (abstract)
PRESENTER: Lu Feng
12:30-14:00Lunch Break
14:00-15:30 Session 4: FM for Program Analysis and Verification

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)
14:50
Verification of Scapegoat Trees using Dafny (abstract)
PRESENTER: Jiapeng Wang
15:15
Real Arithmetic in TLAPM (abstract)
15:30-16:00Coffee Break
16:00-17:30 Session 5: SMT-based Assurance of Behavioral Specifications
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
Wednesday, June 5th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 7: Keynote Talk #2

Formal Verification and Run-time Monitoring for Learning-Enabled Autonomous Systems

Corina S. Pasareanu Carnegie Mellon University Silicon Valley, NASA Ames Research Center

10:00-10:30Coffee Break
10:30-11:45 Session 8: FM for Learning-enabled Systems
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
11:45-12:20 Session 9: Tools Lightening Session

Participants in the Tools Demonstration Session will give a 5 minute lightning talk to introduce their tools.

Chair:
12:30-14:00Lunch Break
14:00-15:30 Session 10: Panel Session: Panel: Trusted Autonomy for Space and Aviation

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.

15:30-16:00Coffee Break
Thursday, June 6th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 12: Keynote Talk #3

Safety under uncertainty: Automotive standards for AI safety and research perspectives

Simon Burton, Centre for Assuring Autonomy, University of York, UK

Chair:
10:00-10:30Coffee Break
10:30-12:30 Session 13: FM for Automotive Systems
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
12:30-14:00Lunch Break
14:00-15:30 Session 14: FM for Robotics
14:00
Robotics: A New Mission for FRET Requirements (abstract)
14:25
The Control Barrier Function Toolbox (abstract)
PRESENTER: Andrew Schoer
14:40
SMT-Based Dynamic Multi-Robot Task Allocation (abstract)
15:05
Safe Planning through Incremental Decomposition of Signal Temporal Logic Specifications (abstract)
PRESENTER: Parv Kapoor
15:30-16:00Coffee Break
16:00-16:55 Session 15: FM for Software Engineering
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