NASA Logo, National Aeronautics and Space Administration

NFM Program

Workshops

Monday, May 11th, 2020

AI Safety Workshop

Friday, May 15th, 2020

Cryptographic Proofs Workshop

Main Conference

Schedule

**Times are indicated in PDT (California time)


Tuesday, May 12th, 2020
Time Event Title
8:00 am - 8:15 am Opening Remarks
8:15 am - 9:15 am Keynote 1 Invited Speaker: Byron Cook (Amazon/UCL)
Title: Automated Reasoning at Amazon
Moderator: Ritchie Lee (NASA Ames)
9:15 am - 9:30 am Break
9:30 am - 11:00 am Session 1 Learning and Formal Synthesis
Session Chair: Michael Lowry (NASA Ames)
11:00 am - 11:15 am Break
11:15 am - 12:05 pm Session 2 Formal Methods for DNNs
Session Chair: Mariano Moscato (NASA Langley)
12:05 pm - 12:45 pm Break
12:45 pm - 1:45 pm Keynote 2 Invited Speaker: David Dill (Facebook/Stanford)
Title: A formal verifier for the Libra blockchain Move language
Moderator: Anastasia Mavridou (NASA Ames/SGT)
1:45 pm - 2:00 pm Break
2:00 pm - 3:30 pm Session 3 High Assurance Systems
Session Chair: Klaus Havelund (NASA JPL)
Wednesday, May 13th, 2020
Time Event Title
8:15 am - 9:15 am Keynote 3 Invited Speaker: Dana Schulze (NTSB)
Title: Improving Design Assurance Through Accident/Incident Lessons Learned
Moderator: Misty Davies (NASA Ames)
9:15 am - 9:30 am Break
9:30 am - 11:00 am Session 4 Requirement Specification and Testing
Session Chair: Aaron Dutle (NASA Langley)
11:00 am - 11:15 am Break
11:15 am - 12:05 pm Session 5 Validation and Solvers
Session Chair: Alessandro Cimatti (FBK)
12:05 pm - 12:45 pm Break
12:45 pm - 1:45 pm Keynote 4 Invited Speaker: Sanjit Seshia (UC Berkeley)
Title: Verified Artificial Intelligence and Autonomy
Moderator: Susmit Jha (SRI)
1:45 pm - 2:00 pm Break
2:00 pm - 3:30 pm Session 6 Solvers and Program Analysis
Session Chair: Corina Pasareanu (NASA Ames/SGT/CMU)
3:30 pm - 4:00 pm Special Session Introducing SAE G-34/EUROCAE WG-114
Session Chair: Mark Roboff (DXC Technology)
Thursday, May 14th, 2020
Time Event Title
8:15 am - 9:15 am Keynote 5 Invited speaker: Vandi Verma (NASA JPL)
Title: Operable NASA Robots on Mars and Beyond
Moderator: Dimitra Giannakopoulou (NASA Ames)
9:15 am - 9:30 am Break
9:30 am - 11:00 am Session 7 Verification and Timed Systems
Session Chair: Alwyn Goodloe (NASA Langley)
11:00 am - 11:15 am Break
11:15 am - 12:25 pm Session 8 Autonomy and Other Applications
Session Chair: Natasha Neogi (NASA Langley)
12:25 pm - 1:00 pm Break
1:00 pm - 2:00 pm Keynote 6 Invited speaker: Leonard Bouygues (Google Loon)
Title: Evolving airspace regulations and systems to enable large scale, highly automated operations in the stratosphere
Moderator: Guillaume Brat (NASA Ames)
2:00 pm - 2:15 pm Break
2:15 pm - 3:45 pm Session 9 Hybrid and Cyber-Physical Systems
Session Chair: Daniel Genin (JHUAPL)
3:45 pm - 4:00 pm Closing Remarks


Sessions


Session 1: Learning and Formal Synthesis
Session Chair: Michael Lowry (michael.r.lowry@nasa.gov)
  • "From Passive to Active: Learning Timed Automata Efficiently," Bernhard K. Aichernig, Andrea Pferscher, and Martin Tappler
  • "Generating Correct-by-Construction Distributed Implementations from Formal Maude Designs," Si Liu, Atul Sandur, Jose Meseguer, Peter Ölveczky, and Qi Wang
  • "Parameter Synthesis and Robustness Analysis of Rule-Based Models," Matej Troják, David Šafránek, Lukrécia Mertová, and Lubos Brim

Session 2: Formal Methods for DNNs
Session Chair: Mariano Moscato (mariano.m.moscato@nasa.gov)
  • "PaRoT: A Practical Framework for Robust Deep Neural Network Training," Edward Ayers, Francisco Eiras, Majd Hawasly, and Iain Whiteside
  • "Simplifying Neural Networks using Formal Verification," Sumathi Gokulanathan, Alexander Feldsher, Adi Malca, Clark Barrett, and Guy Katz

Session 3: High Assurance Systems
Session Chair: Klaus Havelund (klaus.havelund@jpl.nasa.gov)
  • "Neural Simplex Architecture," Dung Phan, Radu Grosu, Nils Jansen, Nicola Paoletti, Scott Smolka and Scott Stoller
  • "Strenghtening Deterministic Policies for POMDPs," Leonore Winterer, Ralf Wimmer, Nils Jansen and Bernd Becker
  • "Benchmarking Software Model Checkers in Automotive Code," Lukas Westhofen, Philipp Berger and Joost-Pieter Katoen

Session 4: Requirement Specification and Testing
Session Chair: Aaron Dutle (aaron.m.dutle@nasa.gov)
  • "Automated Requirements-Based Testing of Black-Box Reactive Systems," Massimo Narizzano, Luca Pulina, Armando Tacchella, and Simone Vuotto
  • "Formal Verification of Parallel Prefix Sum," Mohsen Safari, Wytse Oortwijn, Sebastiaan Joosten, and Marieke Huisman
  • "Specification Quality Metrics Based on Mutation and Inductive Incremental Model Checking," Vassil Todorov, Safouan Taha, and Frédéric Boulanger

Session 5: Validation and Solvers
Session Chair: Alessandro Cimatti (cimatti@fbk.eu)
  • "A Validation Methodology for OCaml-PVS Translation," Xiaoxin An, Amer Tahat, and Binoy Ravindran
  • "On the Usefulness of Clause Strengthening in Parallel SAT Solving," Vincent Vallade, Ludovic Le Frioux, Souheib Baarir, Julien Sopena, and Fabrice Kordon

Session 6: Solvers and Program Analysis
Session Chair: Corina Pasareanu (corina.pasareanu@west.cmu.edu)
  • "Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL," Ralph Bottesch, Max W. Haslbeck, Alban Reynaud, and René Thiemann
  • "Constraint Caching Revisited," Jan Taljaard, Willem Visser, and Jaco Geldenhuys
  • "Per-Location Simulation," Liyi Li and Elsa Gunter

Session 7: Verification and Timed Systems
Session Chair: Alwyn Goodloe (a.goodloe@nasa.gov)
  • "Sampling Distributed Schedulers for Resilient Space Communication," Pedro R. D'Argenio, Juan A. Fraire, and Arnd Hartmanns
  • "Model Checking Timed Hyperproperties in Discrete-Time Systems," Borzoo Bonakdarpour, Pavithra Prabhakar, and Cesar Sanchez
  • "Verifying Band Convergence for Sampled Control Systems," Ezudheen P, Zahra Rahimi Afzal, Pavithra Prabhakar, Deepak D'Souza, and Meenakshi D'Souza

Session 8: Autonomy and Other Applications
Session Chair: Natasha Neogi (natasha.a.neogi@nasa.gov)
  • "Heterogeneous Verification of an Autonomous Curiosity Rover," Rafael C. Cardoso, Marie Farrell, Matt Luckcuck, Angelo Ferrando, and Michael Fisher
  • "Run-Time Assurance for Learning-Enabled Systems," Darren Cofer, Isaac Amundson, Ramachandra Sattigeri, Arjun Passi, Christopher Boggs, Eric Smith, Limei Gilham, Taejoon Byun, and Sanjai Rayadurgam
  • "hpnmg: A C++ Tool for Model Checking Hybrid Petri Nets with General Transitions," Jannik Hüls, Henner Niehaus, and Anne Remke

Session 9: Hybrid and Cyber-Physical Systems
Session Chair: Daniel Genin (daniel.genin@jhuapl.edu)
  • "A Transformation of Hybrid Petri Nets with Stochastic Firings into a Subclass of Stochastic Hybrid Automata," Carina Pilch, Maurice Krause, Anne Remke, and Erika Ábrahám
  • "Constraining Counterexamples in Hybrid System Falsification: Penalty-Based Approaches," Zhenya Zhang, Paolo Arcaini, and Ichiro Hasuo
  • "Falsification of Cyber-Physical Systems with Constrained Signal Spaces," Benoit Barbot, Nicolas Basset, Thao Dang, Alexandre Donzé, James Kapinski, and Tomoya Yamaguchi

Special Session: Introducing SAE G-34/EUROCAE WG-114 – The standards development committee to solve AI certification!

The joint SAE G-34/EUROCAE WG-114 committee is committed to producing a means of compliance for the certification of safety-critical AI systems for both airborne and ground/ATC platforms. In this presentation, we will introduce the joint committee, review its membership, and discuss the fundamental problem space and our vision for a solution. We will also present our roadmap for standards publication, which is aligned to both the ANSI UAS roadmap and the EASA AI roadmap.

First Gov logo
NASA Logo - nasa.gov