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 | Autonomous & 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 | Autonomous 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 | Autonomous 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 Bonakdarpour |
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 Specifications 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 | Software Verification: 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 | Monitoring & Hyperproperties Chair: Alessandro 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 Sankaranarayanan: 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 | Verification Methods 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 |