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 AbrahamChair: | SMT Solving: Past, Present and Future |
11:15 - 11:30 | Break | |
11:30 - 12:00 | Uncertainty and Stochastic Systems Chair: | 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: | 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: | 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 CifuentesChair: | 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 FarzanChair: | Composing Proofs From Program Behaviours |
11:15 - 11:30 | Break | |
11:30 - 12:00 | Verification Chair: | 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 ManningChair: | The Challenge of Designing Reliable Complex Mars Landers and Rovers |
15:00 - 15:15 | Break | |
15:15 - 15:45 | Applied Formal Methods Chair: | 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 DwyerChair: | Distribution-aware Validation of Neural Networks |
11:15 - 11:30 | Break | |
11:30 - 12:00 | Distributed Systems Chair: | 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: | 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 |