NASA Formal Methods 2024 (series) /
NASA Formal Methods 2024 Program
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Tue 4 JunDisplayed time zone: Pacific Time (US & Canada) change
Tue 4 Jun
Displayed time zone: Pacific Time (US & Canada) change
08:30 - 09:00 | |||
08:30 15mTalk | Welcome from NASA Leadership / Dave Alfano, Chief of Intelligent Systems Division NFM 2024 | ||
08:45 15mTalk | Welcome from NFM Chairs NFM 2024 | ||
09:00 - 10:00 | |||
09:00 60mKeynote | Autonomy Challenges for Future NASA Science and Exploration MissionsKeynote NFM 2024 Butler Hine NASA Ames Research Center | ||
10:30 - 12:30 | |||
10:30 25mTalk | Structure-guided Cube-and-conquer for MaxSAT NFM 2024 | ||
10:55 25mTalk | 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 25mTalk | 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 25mTalk | 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 | |||
12:30 90mLunch | 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 25mTalk | 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 25mTalk | 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 25mTalk | 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 15mTalk | Real Arithmetic in TLAPM NFM 2024 Ovini V.W. Gunasekera Lancaster University, Andrew Sogokon Lancaster University, Antonios Gouglidis Lancaster University, Neeraj Suri | ||
15:30 - 16:00 | Afternoon BreakNFM 2024 | ||
15:30 30mBreak | Afternoon Break NFM 2024 | ||
16:00 - 17:30 | SMT-based Assurance of Behavioral SpecificationsNFM 2024 at Ballroom Chair(s): Kristin Yvonne Rozier Iowa State University | ||
16:00 25mTalk | Model Refinement NFM 2024 | ||
16:25 25mTalk | 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 25mTalk | SMT-Based Aircraft Conflict Detection and Elimination NFM 2024 | ||
Wed 5 JunDisplayed time zone: Pacific Time (US & Canada) change
Wed 5 Jun
Displayed time zone: Pacific Time (US & Canada) change
09:00 - 10:00 | |||
09:00 60mKeynote | 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 | |||
10:00 30mCoffee break | Morning Break NFM 2024 | ||
10:30 - 11:45 | |||
10:30 25mTalk | 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 25mTalk | Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems NFM 2024 | ||
11:20 25mTalk | Approximate Conformance Verification of Deep Neural Networks NFM 2024 | ||
11:45 - 12:20 | |||
11:45 35mTalk | 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 | |||
12:30 90mLunch | 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 90mPanel | 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 | ||
15:30 - 16:00 | Afternoon BreakNFM 2024 | ||
15:30 30mBreak | Afternoon Break NFM 2024 | ||
16:00 - 17:30 | |||
16:00 90mDemonstration | Tool Demonstration Session NFM 2024 Nija Shi NASA Ames Research Center, 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 | ||
Thu 6 JunDisplayed time zone: Pacific Time (US & Canada) change
Thu 6 Jun
Displayed time zone: Pacific Time (US & Canada) change
09:00 - 10:00 | |||
09:00 60mKeynote | 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 | |||
10:00 30mCoffee break | Morning Break NFM 2024 | ||
10:30 - 12:30 | |||
10:30 25mTalk | 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 25mTalk | 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 25mTalk | 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 15mTalk | 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 15mTalk | 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 | |||
12:30 90mLunch | Lunch Break NFM 2024 | ||
14:00 - 15:30 | |||
14:00 25mTalk | 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 15mTalk | 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 25mTalk | 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 25mTalk | 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 | ||
15:30 - 16:00 | Afternoon BreakNFM 2024 | ||
15:30 30mBreak | Afternoon Break NFM 2024 | ||
16:00 - 16:55 | |||
16:00 15mTalk | Structuring Formal Methods into the Undergraduate Computer Science Curriculum NFM 2024 | ||
16:15 25mTalk | 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 15mTalk | 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 15mDay closing | Closing Session / NFM 2025 NFM 2024 | ||