NFM 2021

menu

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