NASA
JPL
Caltech
NASA JPL Logo
NASA Logo

NASA Formal Methods 2022 - Schedule

Tuesday, May 24 Wednesday, May 25 Thursday, May 26 Friday, May 27

Tuesday May 24th, 2022: NFM Tutorials

07:55 - 08:00 Welcome
08:00 - 08:45 Tutorial 1
Chair: Klaus Havelund
Edwin Brady: "Total Functional Programming with Idris 2"
08:45 - 09:00 Break
09:00 - 09:45 Tutorial 1
Chair: Klaus Havelund
Edwin Brady: "Total Functional Programming with Idris 2" (cont)
09:45 - 10:15 Break
10:15 - 11:00 Tutorial 2
Chair: Nicolas Rouquette
Leonardo de Moura and Sebastian Ullrich: "An Introduction to the Lean 4 theorem prover and programming language"
11:00 - 11:15 Break
11:15 - 12:00 Tutorial 2
Chair: Nicolas Rouquette
Leonardo de Moura and Sebastian Ullrich: "An Introduction to the Lean 4 theorem prover and programming language" (cont)
12:00 - 13:30 Lunch Break
13:30 - 14:15 Tutorial 3
Chair: Ivan Perez
Anastasia Mavridou: "Capturing and Analyzing Requirements with FRET"
14:15 - 14:30 Break
14:30 - 15:15 Tutorial 3
Chair: Ivan Perez
Anastasia Mavridou: "Capturing and Analyzing Requirements with FRET" (cont)
15:15 - 15:45 Break
15:45 - 16:30 Tutorial 4
Chair: Jyo Deshmukh
Ankush Desai: "Formally Reasoning about Distributed Systems using P"
16:30 - 16:45 Break
16:45 - 17:30 Tutorial 4
Chair: Jyo Deshmukh
Ankush Desai: "Formally Reasoning about Distributed Systems using P" (cont)

Wednesday May 25th, 2022: NFM (Main Conference Day 1)

07:55 - 08:00 Welcome
08:00 - 09:00 Keynote 1
Chair: Ivan Perez
Steve Chien: Formal Methods for Trusted Space Autonomy, Boon or Bane?
09:00 - 09:30 Break
09:30 - 10:30 Auto­nomous & Cyber-Physical Systems
Chair: Chuchu Fan

Josefine Graebener, Apurva Badithela and Richard Murray. Towards Better Test Coverage: Merging Unit Tests for Autonomous Systems (paper #48)


Gilles Nies and Holger Hermanns. Quantification of Battery Depletion Risk Made Efficient (paper #64)


Timothy Wang, Zamira Daw, Pierluigi Nuzzo and Alessandro Pinto. Hierarchical Contract-based Synthesis for Assurance Cases (paper #58)

10:30 - 11:00 Break
11:00 - 12:00 Keynote 2
Chair: Klaus Havelund
Dines Bjorner: An Essence of Domain Engineering - A Basis for Trustworthy Aeronautics and Space Software
12:00 - 13:30 Lunch Break
13:30 - 14:30 Keynote 3
Chair: Mike Hinchey
Daniel Jackson: Formal Methods and the Essence of Software
14:30 - 15:00 Break
15:00 - 16:30 Auto­nomous Systems & Neural Networks: I
Chair: Hoang-Dung Tran

Edoardo Bacci and David Parker. Verified Probabilistic Policies for Deep Reinforcement Learning (paper #73)


Ulices Santa Cruz Leal and Yasser Shoukry. NNLander-VeriF: A Neural Network Formal Verification Framework for Vision-Based Autonomous Aircraft Landing (paper #123)


Usama Mehmood, Sanaz Sheikhi, Stanley Bak, Scott Smolka and Scott Stoller. The Black-Box Simplex Architecture for Runtime Assurance of Autonomous CPS (paper #47)


Yue Meng, Zeng Qiu, Md Tawhid Bin Waez and Chuchu Fan. Case Studies for Computing Density of Reachable States for Safe Autonomous Motion Planning (paper #3)


Marie Farrell, Matt Luckcuck, Oisin Sheridan and Rosemary Monahan. Towards Refactoring FRETish Requirements (Short paper #21)

16:30 - 17:00 Break
17:00 - 18:00 Auto­nomous Systems & Neural Networks: II
Chair: Yasser Shoukry

Stanley Bak and Hoang Dung Tran. Neural Network Compression of ACAS Xu Early Prototype is Unsafe: Closed-Loop Verification through Quantized State Backreachability (paper #55)


Christopher Strong, Sydney Katz, Anthony Corso and Mykel Kochenderfer. ZoPE: A Fast Optimizer for ReLU Networks with Low-Dimensional Inputs (paper #143)


Diganta Mukhopadhyay, Kumar Madhukar and Mandayam Srivas. Permutation Invariance of Deep Neural Networks with ReLUs (paper #41)

19:30 - 22:30 Social dinner at Le Petit Paris, downtown LA (participants are asked to cover their own costs.)

Thursday May 26th, 2022: NFM (Main Conference Day 2)

07:55 - 08:00 Welcome
08:00 - 09:00 Keynote 4
Chair: Klaus Havelund
Julia Lawall: The Coccinelle C-program matching and transformation tool
09:00 - 09:30 Break
09:30 - 10:30 Software Verification: I
Chair: Borzoo Bo­nak­dar­pour

Xaver Fink, Philipp Berger and Joost-Pieter Katoen. Configurable Benchmarks for C Model Checkers (paper #66)


Cong Liu, Junaid Babar, Isaac Amundson, Karl Hoech, Darren Cofer and Eric Mercer. Assume-Guarantee Reasoning with Scheduled Components (paper #34)


Andrea Pferscher and Bernhard K. Aichernig. Stateful Black-Box Fuzzing of Bluetooth Devices Using Automata Learning (paper #62)

10:30 - 11:00 Break
11:00 - 12:00 Software Verification: II
Chair: Alwyn Goodloe

Jad Hamza, Simon Felix, Viktor Kuncak, Ivo Nussbaumer and Filip Schramka. From Verified Scala to STIX File System Embedded Code using Stainless (paper #4)


Etienne Payet, David J. Pearce and Fausto Spoto. On the Termination of Borrow Checking in Featherweight Rust (paper #42)


James Noble, David Streader, Isaac Oscar Gariano and Miniruwani Samarakoon. More Programming Than Programming: Teaching Formal Methods in a Software Engineering Programme (paper #15)

12:00 - 13:30 Lunch Break
13:30 - 14:30 Keynote 5
Chair: Ivan Perez
Alex Summers: The Prusti Project: Formal Verification for Rust
14:30 - 15:00 Break
15:00 - 16:30 Temporal Logic & Timed Spe­ci­fi­ca­tions
Chair: Marie Farrell

Johan Arcile and Étienne André. Zone extrapolations in parametric timed automata (paper #14)


Étienne André, Masaki Waga, Natsuki Urabe and Ichiro Hasuo. Exemplifying parametric timed specifications over signals with bounded behavior (paper #79)


Martin Tappler, Bernhard K. Aichernig and Florian Lorber. Timed Automata Learning via SMT Solving (paper #67)


Alberto Bombardelli and Stefano Tonetta. Asynchronous Composition of Local Interface LTL Properties (paper #75)


Zachary Luppen, Michael Jacks, Nathan Baughman, Muhamed Stilic, Ryan Nasers, Benjamin Hertz, James Cutler, Dae Young Lee and Kristin Yvonne Rozier. Elucidation and Analysis of Specification Patterns in Aerospace System Telemetry (Short paper #113)

16:30 - 17:00 Break
17:00 - 18:00 Model Checking
Chair: Kristin Yvonne Rozier

Satya Prakash Nayak, Daniel Neider, Rajarshi Roy and Martin Zimmermann. Robust Computation Tree Logic (paper #11)


Ruiyang Xu and Karl Lieberherr. On-the-Fly Model Checking with Neural MCTS (paper #35)


Devesh Bhatt, Hao Ren, Anitha Murugesan, Jason Biatek, Srivatsan Varadarajan and Natarajan Shankar. Requirements-Driven Model Checking and Test Generation for Comprehensive Verification (paper #96)

18:00 - 20:00 Program Committee dinner (tentative time) (Note: participation limited to PC members; participants in the PC dinner will be asked to cover their own costs.)

Friday May 27th, 2022: NFM (Main Conference Day 3)

07:55 - 08:00 Welcome
08:00 - 09:00 Keynote 6
Chair: Jyo Deshmukh
Emina Torlak: Solver-Aided Programming for All
09:00 - 09:30 Break
09:30 - 10:30 Soft­wa­re Ve­ri­fi­ca­tion: III
Chair: Alex Summers

Paul Attie. Operational annotations: a new method for sequential program verification (paper #6)


Harold Carr, Christopher Jenkins, Mark Moir, Victor Cacciari Miraldo and Lisandra Silva. Towards Formal Verification of HotStuff-based Byzantine Fault Tolerant Consensus in Agda (paper #30)


Xiaoxin An, Freek Verbeek and Binoy Ravindran. DSV: Disassembly Soundness Validation without Assuming a Ground Truth (paper #54)

10:30 - 11:00 Break
11:00 - 12:00 Mo­ni­to­ring & Hyper­pro­per­ties
Chair: Ales­san­dro Pinto

Oyendrila Dobe, Lukas Wilke, Erika Ábrahám, Ezio Bartocci and Borzoo Bonakdarpour. Probabilistic Hyperproperties with Rewards (paper #97)


Inigo Incer, Albert Benveniste, Alberto Sangiovanni-Vincentelli and Sanjit Seshia. Hypercontracts (paper #102)


Felipe Gorostiaga and Cesar Sanchez. Monitorability of Expressive Verdicts (paper #82)

12:00 - 13:30 Lunch Break
13:30 - 14:30 Keynote 7
Chair: Jyo Deshmukh
Sriram San­ka­ra­na­ra­yanan: Are we there yet? Reachability Analysis for Cyber-Physical Systems
14:30 - 15:00 Break
15:00 - 16:30 Symbolic Analysis
Chair: Stanley Bak

Daniel Basgöze, Matthias Volk, Joost-Pieter Katoen, Shahid Khan and Marielle Stoelinga. BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees (paper #76)


Daisuke Ishii, Takashi Tomita and Toshiaki Aoki. Approximate Translation from Floating-Point to Real-Interval Arithmetic (paper #56)


Baoluo Meng, Arjun Viswanathan, William Smith, Abha Moitra, Kit Siu and Michael Durling. Synthesis of Optimal Defenses for System Architecture Design Model in MaxSMT (paper #147)


Michal Konecny, Sewon Park and Holger Thies. Certified Computation of Nondeterministic Limits (paper #139)


Lieuwe Vinkhuijzen and Alfons Laarman. The Power of Disjoint Support Decompositions in Decision Diagrams (Short paper #127)

16:30 - 17:00 Break
17:00 - 17:30 Ve­ri­fi­ca­tion Me­thods and Tools
Chair: Lucas Bang

Kenny Ballou and Elena Sherman. Incremental Transitive Closure for Zonal Abstract Domain (Short paper #122)


Paolo Masci and Aaron Dutle. Proof Mate: an Interactive Proof Helper for PVS (Short paper #133)


Alexis Aurandt, Phillip Jones and Kristin Yvonne Rozier. Runtime Verification Triggers Real-time, Autonomous Fault Recovery on the CySat-I (Short paper #117)

17:30 - 18:00 Closing remarks

NASA
JPL
Caltech
Site Editors: Klaus Havelund (JPL), Ivan Perez (NIA)