Schedule

All times are US Eastern Time / New York.

If you need to contact the session chairs, please reach out to nfm2021@easychair.org.

Wednesday May 26th, 2021 (Streamed in YouTube)
10:00 - 10:15	Welcome
10:15 - 11:15	Keynote: Erika Abraham Chair: Mariano Moscato	SMT Solving: Past, Present and Future
11:15 - 11:30	Break
11:30 - 12:00	Uncertainty and Stochastic Systems Chair: Susmit Jha	Online Shielding for Stochastic Systems
12:00 - 12:30		Balancing Wind and Batteries: Towards Predictive Verification of Smart Grids
12:30 - 13:00		Scalable Reliability Analysis by Lazy Verification
13:00 - 13:30		Robustifying CPS Controller Specifications Against Perceptual Uncertainty
13:30 - 14:00	Break
14:00 - 14:30	Formal Proofs Chair: Mauricio Ayala-Rincón	A formal proof of the Lax equivalence theorem for finite difference schemes
14:30 - 15:00		Efficient Verification of Optimized Code: Correct High-speed Curve25519
15:00 - 15:30		Polygon Merge: A Geometric Algorithm Verified Using PVS
15:30 - 15:45	Break
15:45 - 16:05	Short papers Chair: Nico Rosner	Integrating Runtime Verification into a Sounding Rocket Control System
16:05 - 16:25		Towards verifying SHA256 in OpenSSL with the Software Analysis Workbench
16:25 - 16:45		On the Effectiveness of Signal Rescaling in Hybrid System Falsification
16:45 - 17:00	Break
17:00 - 18:00	Keynote: Cristina Cifuentes Chair: César Muñoz	The Flavour of Real-World Vulnerability Detection and Intelligent Configuration

Thursday May 27th, 2021 (Streamed in YouTube)
10:00 - 10:15	Opening
10:15 - 11:15	Keynote: Azadeh Farzan Chair: Laura Titolo	Composing Proofs From Program Behaviours
11:15 - 11:30	Break
11:30 - 12:00	Verification Chair: Pierre-loic Garoche	Verification of Functional Correctness of Code Diversification Techniques
12:00 - 12:30		Runtime Verification of Generalized Test Tables
12:30 - 13:00		nnenum: Verification of ReLU Neural Networks with Optimized Abstraction Refinement
13:00 - 13:30		Verifying min-plus Computations with Coq
13:30 - 14:00	Break
14:00 - 15:00	Keynote: Rob Manning Chair: Ivan Perez	The Challenge of Designing Reliable Complex Mars Landers and Rovers
15:00 - 15:15	Break
15:15 - 15:45	Applied Formal Methods Chair: Kristin Rozier	Minimum-Violation Traffic Management for Urban Air Mobility
15:45 - 16:15		Good fences make good neighbors: designing a formally verified predictive geofence
16:15 - 16:45		Integrating Formal Verification and Assurance: An Inspection Rover Case Study

Friday May 28th, 2021 (Streamed in YouTube)
10:00 - 10:15	Opening
10:15 - 11:15	Keynote: Matthew Dwyer Chair: Aaron Dutle	Distribution-aware Validation of Neural Networks
11:15 - 11:30	Break
11:30 - 12:00	Distributed Systems Chair: Alwyn Goodloe	Verification of Eventual Consensus in Synod Using a Failure-Aware Actor Model
12:00 - 12:30		An Infrastructure for Faithful Execution of Remote Attestation Protocols
12:30 - 13:00		On Symmetry and Quantification: A New Approach to Verify Distributed Protocols
13:00 - 13:30		Quasi-Equal Clock Reduction On-the-Fly
13:30 - 14:00	Break
14:00 - 14:30	Synthesis and Verification Chair: Cristina Seceleanu	Specification Decomposition for Reactive Synthesis
14:00 - 15:00		Program Sketching using Lifted Analysis for Numerical Program Families
15:00 - 15:30		Recursive Variable-Length State Compression for Multi-Core Software Model Checking
15:30 - 16:00	Closing remarks

Accepted Papers

Proceedings of the 13th International Symposium on NASA Formal Methods, NFM 2021, are available through the following link

Stanley Bak. nnenum: Verification of ReLU Neural Networks with Optimized Abstraction Refinement.

Sudarshanan Bharadwaj, Tichakorn Wongpiromsarn, Natasha Neogi, Joseph Muffoletto and Ufuk Topcu. Minimum-Violation Traffic Management for Urban Air Mobility.

Hamza Bourbouh, Marie Farrell, Anastasia Mavridou, Irfan Sljivo, Guillaume Brat, Louise Dennis and Michael Fisher. Integrating Formal Verification and Assurance: An Inspection Rover Case Study.

Brett Decker, Benjamin Winters and Eric Mercer. Towards verifying SHA256 in OpenSSL with the Software Analysis Workbench.

Ben Di Vito and Ashlie B. Hocking. Polygon Merge: A Geometric Algorithm Verified Using PVS.

Bernd Finkbeiner, Gideon Geier and Noemi Passing. Specification Decomposition for Reactive Synthesis.

Daniel Genin, Yanni Kouskoulas, Aurora Schmidt, Rosa Wu, Joshua Brule and Anthony Mochado. Good fences make good neighbors: designing a formally verified predictive geofence.

Aman Goel and Karem A. Sakallah. On Symmetry and Quantification: A New Approach to Verify Distributed Protocols.

Benjamin Hertz, Zachary Luppen and Kristin Yvonne Rozier. Integrating Runtime Verification into a Sounding Rocket Control System.

Jae-Won Jang, Freek Verbeek and Binoy Ravindran. Verification of Functional Correctness of Code Diversification Techniques.

Shahid Khan, Joost-Pieter Katoen, Matthias Volk and Marc Bouissou. Scalable Reliability Analysis by Lazy Verification.

Tsutomu Kobayashi, Rick Salay, Ichiro Hasuo, Krzysztof Czarnecki, Fuyuki Ishikawa and Shin-ya Katsumata. Robustifying CPS Controller Specifications Against Perceptual Uncertainty.

Bettina Könighofer, Julian Rudolf, Alexander Palmisano, Martin Tappler and Roderick Bloem. Online Shielding for Stochastic Systems.

Saswata Paul, Gul Agha, Stacy Patterson and Carlos A. Varela. Verification of Eventual Consensus in Synod Using a Failure-Aware Actor Model.

Adam Petz and Perry Alexander. An Infrastructure for Faithful Execution of Remote Attestation Protocols.

Lucien Rakotomalala, Marc Boyer and Pierre Roux. Verifying min-plus Computations with Coq.

Thom S. Badings, Arnd Hartmanns, Nils Jansen and Marnix Suilen. Balancing Wind and Batteries: Towards Predictive Verification of Smart Grids.

Aleksandar S. Dimovski, Sven Apel and Axel Legay. Program Sketching using Lifted Analysis for Numerical Program Families.

Marc Schoolderman, Jonathan Moerman, Sjaak Smetsers and Marko Van Eekelen. Efficient Verification of Optimized Code: Correct High-speed Curve25519.

Mohit Tekriwal, Karthik Duraisamy and Jean-Baptiste Jeannin. A formal proof of the Lax equivalence theorem for finite difference schemes.

Alexander Weigl, Mattias Ulbrich, Shmuel Tyszberowicz and Jonas Klamroth. Runtime Verification of Generalized Test Tables.

Bernd Westphal. Quasi-Equal Clock Reduction On-the-Fly.

Zhenya Zhang, Deyun Lyu, Paolo Arcaini, Lei Ma, Ichiro Hasuo and Jianjun Zhao. On the Effectiveness of Signal Rescaling in Hybrid System Falsification.

Freark van der Berg. Recursive Variable-Length State Compression for Multi-Core Software Model Checking.