J Tanner Slagel

Dr. Slagel is a member of the Safety Critical Avionics Systems branch where he applies formal methods to assure safety- and mission-critical systems of interest to NASA, particularly systems involving uncrewed aircraft systems. He has been the lead researcher for an effort called Properly Assured Implementation of Differential Dynamic Logic for hybrid Program Verification and Specification (PlaidyPVS) and is the PI of the TACP CAS Aerial AId activity focused on enabling and assuring perception engines needed for medical UAS use-cases. Before joining NASA, Tanner completed his doctorate focused on inverse problems and large-scale optimization in the Mathematics Department at Virginia Tech. He started at NASA in the Summer of 2018 as a summer intern and joined NASA as a full-time Civil Servant August 2019.

Recent Publications

2024

J Tanner Slagel, Lauren White, Aaron Dutle, César Muñoz, and Nicolas Crespo, A Formal Verification Framework for Runtime Assurance, Proceedings of the 16th NASA Formal Methods Symposium (NFM 2024), Lecture Notes in Computer Science, Vol. 14627, pp. 322-328. BibTeX Reference.

Lauren White, Laura Titolo, J. Tanner Slagel, and César Muñoz, A Temporal Differential Dynamic Logic Formal Embedding, Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2024), London, UK, 2024. BibTeX Reference.

2023

J Tanner Slagel, Mariano Moscato, Lauren White, César Muñoz, Swee Balachandran, and Aaron Dutle, Embedding Differential Dynamic Logic in PVS,Proceedings of the 18th International Workshop on Logical and Semantic Frameworks, with Applications, 2023. BibTeX Reference.

2022

J Tanner Slagel, César Muñoz, Swee Balachandran, Mariano M. Moscato, Aaron Dutle, Paolo Masci, and Lauren White, Towards an implementation of differential dynamic logic in PVS, Proceedings of the 11th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis (SOAP 2022), 2022.. BibTeX Reference.

2021

J Tanner Slagel, Lauren White, and Aaron Dutle, Formal verification of semi-algebraic sets and real analytic functions, Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proof, pp. 278-290, 2021. BibTeX Reference.

2020