Room InformationNo extra information available
Program

You're viewing the program in a time zone which is different from your device's time zone change time zone

Tue 4 Jun

Displayed time zone: Pacific Time (US & Canada) change

09:00 - 10:00
Keynote Talk #1NFM 2024 at Ballroom
Chair(s): Nathan Benz NASA Ames Research Center
09:00
60m
Keynote
Autonomy Challenges for Future NASA Science and Exploration MissionsKeynote
NFM 2024
Butler Hine NASA Ames Research Center
10:30 - 12:30
Advances in Solver Technology NFM 2024 at Ballroom
Chair(s): Ivan Perez NASA Ames Research Center
10:30
25m
Talk
Structure-guided Cube-and-conquer for MaxSAT
NFM 2024
Max Bannach European Space Agency, Advanced Concepts Team, Markus Hecher MIT
10:55
25m
Talk
Tackling the polarity initialization problem in SAT solving using a genetic algorithm
NFM 2024
Sabrine Saouli Sorbonne Université (LIP6), Souheib Baarir EPITA (LRE), Claude Dutheillet LIP6 Universite Pierre et Marie Curie
11:20
25m
Talk
Formalization of asymptotic convergence for Stationary Iterative Methods
NFM 2024
Mohit Tekriwal Lawrence Livermore National Laboratory, Joshua Miller University of Michigan, Ann Arbor, Jean-Baptiste Jeannin University of Michigan at Ann Arbor
11:45
25m
Talk
Distributional Probabilistic Model Checking
NFM 2024
Ingy Elsayed-Aly University of Virginia, David Parker University of Oxford, Lu Feng University of Virginia
12:30 - 14:00
Lunch BreakNFM 2024 at Ballroom
12:30
90m
Lunch
Lunch Break
NFM 2024

14:00 - 15:30
FM for Program Analysis and Verification NFM 2024 at Ballroom
Chair(s): Douglas Smith Kestrel Institute
14:00
25m
Talk
Quantitative Input Usage Static Analysis
NFM 2024
Denis Mazzucato INRIA & École Normale Supérieure | Université PSL, Marco Campion INRIA & École Normale Supérieure | Université PSL, Caterina Urban Inria & École Normale Supérieure | Université PSL
14:25
25m
Talk
Verifying a C implementation of Derecho's coordination mechanism using VST and Coq
NFM 2024
Ramana Nagasamudram Stevens Institute of Technology, Lennart Beringer Princeton University, Ken Birman Cornell University, Mae Milano Princeton University, David Naumann Stevens Institute of Technology
14:50
25m
Talk
Verification of Scapegoat Trees using Dafny
NFM 2024
Jiapeng Wang East China Normal University, Sini Chen East China Normal University, Huibiao Zhu East China Normal University
15:15
15m
Talk
Real Arithmetic in TLAPM
NFM 2024
Ovini V.W. Gunasekera Lancaster University, Andrew Sogokon Lancaster University, Antonios Gouglidis Lancaster University, Neeraj Suri
16:00 - 17:30
SMT-based Assurance of Behavioral SpecificationsNFM 2024 at Ballroom
Chair(s): Kristin Yvonne Rozier Iowa State University
16:00
25m
Talk
Model Refinement
NFM 2024
Douglas Smith Kestrel Institute, Srinivas Nedunuri Sandia National Laboratories
16:25
25m
Talk
Symmetry-based Abstraction Algorithm for Accelerating Symbolic Control Synthesis
NFM 2024
Hussein Sibai Washington University in St. Louis, Sacha Huriot Washington University in St. Louis, Tyler Martin Washington University in St. Louis, Murat Arcak University of California, Berkeley
16:50
25m
Talk
SMT-Based Aircraft Conflict Detection and Elimination
NFM 2024
Saswata Paul GE Research, Baoluo Meng GE Research, Christopher Alexander GE Research

Wed 5 Jun

Displayed time zone: Pacific Time (US & Canada) change

09:00 - 10:00
Keynote Talk #2NFM 2024 at Ballroom
Chair(s): Divya Gopinath NASA Ames (KBR Inc.)
09:00
60m
Keynote
Formal Verification and Run-time Monitoring for Learning-Enabled Autonomous SystemsKeynote
NFM 2024
Corina S. Pasareanu Carnegie Mellon University Silicon Valley, NASA Ames Research Center
10:00 - 10:30
Morning BreakNFM 2024 at Ballroom
10:00
30m
Coffee break
Morning Break
NFM 2024

10:30 - 11:45
FM for Learning-enabled Systems NFM 2024 at Ballroom
Chair(s): Misty Davies NASA
10:30
25m
Talk
Towards formal verification of neural networks in cyber-physical systems
NFM 2024
Federico Rossi Università di Pisa, Dipartimento di Ingegneria dell'Informazione, Cinzia Bernardeshi Università di Pisa, Dipartimento di Ingegneria dell'Informazione, Marco Cococcioni Università di Pisa, Dipartimento di Ingegneria dell'Informazione, Maurizio Palmieri Università di Pisa, Dipartimento di Ingegneria dell'Informazione
10:55
25m
Talk
Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems
NFM 2024
Yuhao Zhou , Stavros Tripakis Northeastern University
11:20
25m
Talk
Approximate Conformance Verification of Deep Neural Networks
NFM 2024
Habeeb P Indian Institute of Science, Bangalore., Pavithra Prabhakar Kansas State University
11:45 - 12:20
Tools Lightning SessionNFM 2024 at Ballroom
Chair(s): Nija Shi NASA Ames Research Center

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

11:45
35m
Talk
Tools Lightning Talks
NFM 2024
Lukas Westhofen DLR e.V. Institute of Systems Engineering for Future Mobility, Ovini V.W. Gunasekera Lancaster University, Andrew Schoer MIT Lincoln Laboratory, Xaver Fink CERN, Andreas Katis KBR / NASA Ames Research Center, Victoria Marie Tuck University of California, Berkeley, Federico Rossi Università di Pisa, Dipartimento di Ingegneria dell'Informazione
12:30 - 14:00
Lunch BreakNFM 2024 at Ballroom
12:30
90m
Lunch
Lunch Break
NFM 2024

14:00 - 15:30
PanelNFM 2024 at Ballroom
Chair(s): Guillaume P. Brat NASA Ames Research Center

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.

14:00
90m
Panel
Panel: Trusted Autonomy for Space and Aviation
NFM 2024
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

Thu 6 Jun

Displayed time zone: Pacific Time (US & Canada) change

09:00 - 10:00
Keynote Talk #3NFM 2024 at Ballroom
Chair(s): Nija Shi NASA Ames Research Center
09:00
60m
Keynote
Safety under uncertainty: Automotive standards for AI safety and research perspectivesKeynote
NFM 2024
Simon Burton Centre for Assuring Autonomy, University of York, UK
10:00 - 10:30
Morning BreakNFM 2024 at Ballroom
10:00
30m
Coffee break
Morning Break
NFM 2024

10:30 - 12:30
FM for Automotive SystemsNFM 2024 at Ballroom
Chair(s): Michael R. Lowry NASA Ames Research Center
10:30
25m
Talk
Tree-Based Scenario Classification. A Formal Framework for Measuring Domain Coverage when Testing Autonomous Systems
NFM 2024
Till Schallau TU Dortmund University, Stefan Naujokat TU Dortmund University, Fiona Kullmann TU Dortmund University, Falk Howar TU Dortmund University
10:55
25m
Talk
Validation of Reinforcement Learning Agents and Safety Shields with ProB
NFM 2024
Fabian Vu Heinrich-Heine-Universität, Jannik Dunkelau Heinrich-Heine-Universität, Michael Leuschel University of Düsseldorf
11:20
25m
Talk
Contract-driven Runtime Adaptation
NFM 2024
Eunsuk Kang Carnegie Mellon University, Akila Ganlath Toyota InfoTech Labs, Shatadal Mishra Toyota Motor North America R&D, InfoTech Labs, Florin Baiduc Woven by Toyota, Inc., Nejib Ammar Toyota Motor North America R&D, InfoTech Labs
11:45
15m
Talk
Topplet: An Optimized Engine for Answering Metric Temporal Conjunctive Queries
NFM 2024
Lukas Westhofen DLR e.V. Institute of Systems Engineering for Future Mobility, Christian Neurohr DLR e.V. Institute of Systems Engineering for Future Mobility, Danel Neider TU Dortmund University, Jean Christoph Jung TU Dortmund University
12:00
15m
Talk
A Formal Verification Framework for Runtime Assurance
NFM 2024
J Tanner Slagel NASA Langley Research Center, Lauren White NASA, Aaron Dutle NASA Langley Research Center, Cesar Munoz NASA, Nicolas Crespo NASA
12:30 - 14:00
Lunch BreakNFM 2024 at Ballroom
12:30
90m
Lunch
Lunch Break
NFM 2024

14:00 - 15:30
FM for RoboticsNFM 2024 at Ballroom
Chair(s): Johann Schumann KBR / NASA
14:00
25m
Talk
Robotics: A New Mission for FRET Requirements
NFM 2024
Gricel Vázquez University of York, UK, Anastasia Mavridou KBR / NASA Ames Research Center, Marie Farrell The University of Manchester, Thomas Pressburger NASA Ames Research Center, Radu Calinescu University of York, UK
14:25
15m
Talk
The Control Barrier Function Toolbox
NFM 2024
Andrew Schoer MIT Lincoln Laboratory, Helena Teixeira-Dasilva Washington University in St. Louis, Christian So Boston University, Makai Mann MIT Lincoln Laboratory, Roberto Tron Boston University
14:40
25m
Talk
SMT-Based Dynamic Multi-Robot Task Allocation
NFM 2024
Victoria Marie Tuck University of California, Berkeley, Pei-Wei Chen University of California, Berkeley, Georgios Fainekos Toyota Research Institute of North America, Bardh Hoxha Toyota Motor North America, Research & Development, Hideki Okamoto Toyota Motor North America, Research & Development, S. Shankar Sastry University of California, Berkeley, Sanjit A. Seshia University of California at Berkeley
15:05
25m
Talk
Safe Planning through Incremental Decomposition of Signal Temporal Logic Specifications
NFM 2024
Parv Kapoor Carnegie Mellon University, Eunsuk Kang Carnegie Mellon University, Romulo Meira-Goes The Pennsylvania State University
16:00 - 16:55
FM for Software EngineeringNFM 2024 at Ballroom
Chair(s): Sandy Lozito NASA Ames Research Center
16:00
15m
Talk
Structuring Formal Methods into the Undergraduate Computer Science Curriculum
NFM 2024
16:15
25m
Talk
Integrated Contract-based Unit and System Testing for Component-based Systems
NFM 2024
John Hatcliff Kansas State University, Jason Belt Kansas State University, Robby Kansas State University, David Hardin Collins Aerospace
16:40
15m
Talk
Verifying PLC Programs via Monitors: Extending the Integration of FRET and PLCverif
NFM 2024
Xaver Fink CERN, Anastasia Mavridou KBR / NASA Ames Research Center, Andreas Katis KBR / NASA Ames Research Center, Borja Fernandez Adiego CERN
16:55 - 17:10
Closing Session / NFM 2025NFM 2024 at Ballroom
Chair(s): Nathan Benz NASA Ames Research Center, Divya Gopinath NASA Ames (KBR Inc.), Nija Shi NASA Ames Research Center
16:55
15m
Day closing
Closing Session / NFM 2025
NFM 2024

Thu 6 Jun

Displayed time zone: Pacific Time (US & Canada) change