----------------------------------------- Call for Participation: NFM 2025 -----------------------------------------
The 17th NASA Formal Methods Symposium ---------------- 30 Years of Formal Methods at NASA June 11-13, Williamsburg, Virginia, United States of America https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fshemesh.larc.nasa.gov%2Fnfm2025%2F&data=05%7C02%7Com%40openmath.org%7C693146feef2e4cb588e408dd88ab0fc8%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638816990490036775%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=0pCHxIbD1UYw7%2FYFSd8A1WIPwnubqrN%2FV1dus4GMPvI%3D&reserved=0 <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fshemesh.larc.nasa.gov%2Fnfm2025%2F&data=05%7C02%7Com%40openmath.org%7C693146feef2e4cb588e408dd88ab0fc8%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638816990490052527%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=jXI6CmiNO8rcu49UNFd8ZRNbrp4ZzyURPkSCsSmdtV4%3D&reserved=0> Keynote speakers ---------------- Darren Cofer (Collins Aerospace) Emina Torlak (Amazon Web Services) Natasha Neogi and Paul Miner (NASA) The program of symposium is available at: https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fshemesh.larc.nasa.gov%2Fnfm2025%2Fprogram.html&data=05%7C02%7Com%40openmath.org%7C693146feef2e4cb588e408dd88ab0fc8%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638816990490061507%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=lEqfkPGggkiQ5sfcMj52HAmQ%2BGVOe5v6Hi73Sdbe3Ys%3D&reserved=0 <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fshemesh.larc.nasa.gov%2Fnfm2025%2Fprogram.html&data=05%7C02%7Com%40openmath.org%7C693146feef2e4cb588e408dd88ab0fc8%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638816990490070180%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=HWDf3X%2FtFcOpvl4b9xoYNUKW0Qg55JmC9hBbVVL%2B%2BYY%3D&reserved=0> Attendance to the symposium is free, but all attendees must register in order to participate. Registrations is open at: https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fshemesh.larc.nasa.gov%2Fnfm2025%2Fregistration.html&data=05%7C02%7Com%40openmath.org%7C693146feef2e4cb588e408dd88ab0fc8%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638816990490078996%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=xCAxbvvZMxQvkqXVqEQNaedNXKLxmkvgXjv54B3tSUk%3D&reserved=0 <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fshemesh.larc.nasa.gov%2Fnfm2025%2Fregistration.html&data=05%7C02%7Com%40openmath.org%7C693146feef2e4cb588e408dd88ab0fc8%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638816990490088165%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=I2esIlWgmuya0zWq3zdrsw6Ytx9glx78HAEEMguwxjQ%3D&reserved=0> The symposium will be held at the College of William and Mary at Sadler Center 200 Stadium Drive Williamsburg, VA 23186 For more information about travel and lodging options, see https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fshemesh.larc.nasa.gov%2Fnfm2025%2Fvenue.html&data=05%7C02%7Com%40openmath.org%7C693146feef2e4cb588e408dd88ab0fc8%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638816990490097461%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=8qWZfcjLxhEtMqSMFWI3hgnrihnZ%2FKo2mq0msJHps%2FQ%3D&reserved=0 <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fshemesh.larc.nasa.gov%2Fnfm2025%2Fvenue.html&data=05%7C02%7Com%40openmath.org%7C693146feef2e4cb588e408dd88ab0fc8%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638816990490106992%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=JwpsIWT3h8IP80fxBiFtoDDfSgZ%2FQRJIOd3uCKqzt%2F4%3D&reserved=0> List of Accepted Papers ---------------- * Arthur Amorim, Max Taylor, Trevor Kann, William Harrison, Gary Leavens, and Lance Joneckis. Enforcing MAVLink Safety & Security Properties Via Refined Multiparty Session Types * Ziggy Attala, Fang Yan, Simon Foster, Ana Cavalcanti, and Jim Woodcock. Process-Algebraic Semantics for Verifying Intelligent Robotic Control Software * Alexis Aurandt, Phillip Jones, and Kristin Yvonne Rozier. Towards a Safe, Verified Runtime Monitor for Embedded Systems: R2U2 in Embedded Rust * Mauricio Ayala-Rincón, Thaynara Arielly de Lima, Maria Júlia Dias Lima, Mariano Moscato, and Temur Kutsia. Verification of an Anti-Unification Algorithm in PVS * Max Bannach, Jai Grover, and Markus Hecher. Strong Structural Bounds for MaxSAT: The Fine Details of Using Neuromorphic and Quantum Hardware Accelerators * Calvin Beck, Hanxi Chen, and Steve Zdancewic. Vellvm: Formalizing the Informal LLVM (Experience Report) * Andrea Bombarda, Silvia Bonfanti, Angelo Gargantini, and Nico Pellegrinelli. Eliminating Flakiness: Deterministic Control for Validating Nondeterministic Asmeta Specifications * Matías Brizzio, Felipe Gorostiaga, Cesar Sanchez, and Renzo Degiovanni. Mode-based Reactive Synthesis * Pranav Ghorpade, Nathalie Bertrand, Sasha Rubin, Bernhard Scholz, and Pavle Subotic. Reusable Formal Verification of DAG-based Consensus Protocols * Andreas Katis, Anastasia Mavridou, and Thomas Pressburger. A Streamlined, Formal Approach to Requirements-based Testing * Elias Khalife, Pierre-Loic Garoche, and Mazen Farhood. Formally Proving Invariant Systemic Properties of Control Programs Using Ghost Code and Integral Quadratic Constraints * Edward Kim, Devan Shanker, Varun Bharadwaj, Hongbeen Park, Jinkyu Kim, Hazem Torfah, Daniel Fremont, and Sanjit Seshia. Querying Labeled Time Series Data with Scenario Programs * Ignacio D. Lopez-Miguel, Borja Fernández Adiego, Matias Salinas, and Christine Betz. Formal Verification as a Service: A CERN-GSI Case Study * Sumio Morioka, Satoshi Obana, and Maki Yoshida. Formal Verification of Composite Field Multipliers for Information-Theoretically Secure Radio Communication in Spacecraft Control * Mathis Niehage, Carina da Silva, Anne Remke, and Arnd Hartmanns. Rare Event Simulation for Stochastic Hybrid Systems using Symbolic Importance Functions * Carlos Olarte, Daniel Osorio, Carlos Ramirez, and Camilo Rocha. Algorithmic Analysis of Event-B in Rewriting Logic * Jainta Paul, Stefan Mitsch, and Luis Garcia. HyTwin: A Formal Semantics for Digital Twin Interventions in ICS Based on Time-to-Violation * Alec Rosentrater, Zili Wang, Katherine Kosaian, and Kristin Yvonne Rozier. Language Partitioning for Mission-time Linear Temporal Logic * Nafiz Sadman, Nastaran Kianersi, and Sean Kauffman. Visualizing Temporal Interval Hierarchies * Mohit Tekriwal and Matthew Sottile. Mechanized RS274 semantics for additive manufacturing * Benjamin Valpey, Xinyi Li, Sreepathi Pai, and Ganesh Gopalakrishnan. An SMT Formalization of Mixed-Precision Matrix Multiplication (Modeling Three Generations of Tensor Cores) * Sarat Chandra Varanasi, Baoluo Meng, Robert Lorch, Abha Moitra, Kit Siu, Saswata Paul, Michael During, Neha Beniwal, and Nikita Visnevski. TRACE: Toolkit for Requirements Analysis, Capture, and Elicitation * Jian Xiang and Stephen Chong. Extending Dynamic Logics with First-Class Relational Reasoning * Michal Šedý and Lukáš Holík. Automata Size Reduction by Procedure Finding Organizing Committee ---------------- Conference Chair * Laura Titolo<https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flauratitolo.github.io%2F&data=05%7C02%7Com%40openmath.org%7C693146feef2e4cb588e408dd88ab0fc8%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638816990490117231%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=3rc08vjvp7umFHq9EZKdDK4kxvGFTqbxHStGG1naVrk%3D&reserved=0> (CodeMetal) Program Committee Chairs * Aaron Dutle<https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fshemesh.larc.nasa.gov%2Fpeople%2Famd&data=05%7C02%7Com%40openmath.org%7C693146feef2e4cb588e408dd88ab0fc8%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638816990490333731%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=0JBUYBHGMnu5RjTNi6iMKpTatL%2BYc2%2BV%2FpVsRxebCYg%3D&reserved=0> (NASA) * Laura Humphrey (NASA) Local Organization * Yifan Sun<https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.wm.edu%2Fas%2Fcomputerscience%2Fpeople%2Fsun_yifan.php&data=05%7C02%7Com%40openmath.org%7C693146feef2e4cb588e408dd88ab0fc8%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638816990490351675%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=YfBqD6a36Q6dmSu8IMnnKdbDYAt1Xmg0s%2Fosy6hQ6kk%3D&reserved=0> (William & Mary) * Mariano Moscato<https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmarianomoscato.github.io%2F&data=05%7C02%7Com%40openmath.org%7C693146feef2e4cb588e408dd88ab0fc8%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638816990490361418%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=8mIdowWzlOb8mKt9gxlXvdhI%2Bdh6LIOiQ97%2FjhkxhbU%3D&reserved=0> (AMA Inc.) Publicity * J Tanner Slagel<https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fshemesh.larc.nasa.gov%2Fpeople%2Fjts&data=05%7C02%7Com%40openmath.org%7C693146feef2e4cb588e408dd88ab0fc8%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638816990490371580%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=V545EMlCHjOX3p%2BJiW514EAoAExFJzol8AzoGBikFq4%3D&reserved=0> (NASA) Contact -------- Email: nfm2025 [at] easychair [dot] org Web: https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fshemesh.larc.nasa.gov%2Fnfm2025%2Findex.html&data=05%7C02%7Com%40openmath.org%7C693146feef2e4cb588e408dd88ab0fc8%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638816990490381116%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=gWw3bGBfsv0admzLiHSZrC5aJ28BgTNvW5Z93HyavgE%3D&reserved=0 - loc-home<https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fshemesh.larc.nasa.gov%2Fnfm2025%2Findex.html%23loc-home&data=05%7C02%7Com%40openmath.org%7C693146feef2e4cb588e408dd88ab0fc8%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638816990490390688%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=XzwJl8AB4kSKdIHeEeEUIcIwlqhdtLG4%2BwvEdes%2B6bg%3D&reserved=0> <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fshemesh.larc.nasa.gov%2Fnfm2025%2Findex.html&data=05%7C02%7Com%40openmath.org%7C693146feef2e4cb588e408dd88ab0fc8%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638816990490400219%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=jK%2BMOmb2Avy9pYfLspV%2FN3TOOJJNHkycYJZ8%2F%2BvWWow%3D&reserved=0 - loc-home<https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fshemesh.larc.nasa.gov%2Fnfm2025%2Findex.html%23loc-home&data=05%7C02%7Com%40openmath.org%7C693146feef2e4cb588e408dd88ab0fc8%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638816990490409970%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=6a2ZzNijfOvmBTLpn6HNXSkP16xNhVfsV93LwD1aVSQ%3D&reserved=0>> Sincerely, Tanner [NASA Meatball Logo]<https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.nasa.gov%2F&data=05%7C02%7Com%40openmath.org%7C693146feef2e4cb588e408dd88ab0fc8%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638816990490419302%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=hkEYwnbo%2FQ3udEoSaFTh5mj4S4EJbg6MtG9jAM2rOZo%3D&reserved=0> J Tanner Slagel Research Computer Scientist Safety Critical Avionics Systems Branch NASA Langley Research Center j.tanner.sla...@nasa.gov<mailto:j.tanner.sla...@nasa.gov>
--- To opt-out from this mailing list, send an email to fm-announcements-requ...@lists.nasa.gov with the word 'unsubscribe' as subject or in the body. You can also make the request by contacting fm-announcements-ow...@lists.nasa.gov
_______________________________________________ Om mailing list Om@openmath.org https://mailman.openmath.org/cgi-bin/mailman/listinfo/om
