Aaron M. Dutle

I am a mathematician turned computer scientist working in the Formal Methods group at NASA Langley Research Center, Hampton, VA.

I earned an undergraduate degree in Mathematics, with a second major in Philosophy, from Northern Kentucky University. I earned a Master's degree in Mathematics from Texas A&M University. I earned my doctorate in Mathematics from the University of South Carolina as a student of Joshua Cooper. After graduation, I remained at the University of South Carolina as a post-doctoral fellow studying complex networks under a multi-institution grant from DARPA . My Erdős number is 2.

My primary interests prior to working at NASA were broadly in the fields of Graph Theory and Combinatorics. More specifically, I enjoy studying spectral properties of graphs and hypergraphs; the relationships between random, pseudo-random, and quasi-random combinatorial structures; computational complexity of graph algorithms and algorithms in general; and the use of graphs to model real-world phenomena.

At NASA, there are two separate but intertwined aims of my research. The first is the development and enhancement of formal methods tools and technologies. The second is the use of formal methods tools for the verification of concepts and software related to aerospace applications. The development of new and more powerful tools in formal methods allows for more difficult projects to be undertaken, while the needs of the particular projects also steer the direction of the tools that are being developed.

Publications

• Victor Carreño, Mariano Moscato, Paolo Masci, Aaron Dutle Interpretation and Formalization of the Right-of-Way Rules Proceedings of Formal Aspects of Component Software: 18th International Conference (FACS 2022), Virtual Event, November 10-11, 2022.
• J. Tanner Slagel, César Muñoz, Swee Balachandran, Mariano Moscato, Aaron Dutle, Paolo Masci, 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), San Diego, CA, USA, June 8, 2022.
• Paolo Masci, Aaron Dutle Proof Mate: an Interactive Proof Helper for PVS (tool paper) Proceedings of the 14th NASA Formal Methods Symposium (NFM 2022), Pasadena, CA, USA, May 24–27, 2022.
• Esther Conrad, Laura Titolo, Dimitra Giannakopoulou, Thomas Pressburger, and Aaron Dutle A compositional proof framework for FRETish requirements Proceedings of Certified Programs and Proofs (CPP 2022), Philidelphia, PA, USA, 16-18 January, 2022.
• J. Tanner Slagel, Lauren White, Aaron Dutle Formal Verification of Semi-Algebraic Sets and Real Analytic Functions Proceedings of Certified Programs and Proofs (CPP) 2021, Virtual, 17-19 January, 2021.
• Aaron Dutle, César Muñoz, Esther Conrad, Alwyn Goodloe, Laura Titolo, Ivan Perez, Swee Balachandran, Dimitra Giannakopoulou, Anastasia Mavridou, Thomas Pressburger From Requirements to Autonomous Flight: An Overview of the Monitoring ICAROUS Project Proceedings of the Second Workshop on Formal Methods for Autonomous Systems (FMAS 2020), Virtual, 7th of December 2020, Electronic Proceedings in Theoretical Computer Science 329, pp. 23–30.
• Aaron Dutle, Mariano Moscato, Laura Titolo, César Muñoz, Gregory Anderson, and François Bobot Formal Analysis of the Compact Position Reporting Algorithm Formal Aspects of Computing (2021).
• Anthony Narkawicz, César Muñoz, and Aaron Dutle,Sensor Uncertainty Mitigation and Dynamic Well Clear Volumes in DAIDALUS, Proceedings of the 37th Digital Avionics Systems Conference (DASC 2018), London, England, UK, 2018. (Won best of track, UAV)
• Anthony Narkawicz, César Muñoz, and Aaron Dutle,A Decision Procedure for Univariate Polynomial Systems Based on Root Counting and Interval Subdivision, Journal of Formalized Reasoning, Vol. 11, Number 1, pp. 19-41, 2018
• Thiago Mendoça Ferreira Ramos, César Muñoz, Mauricio Ayala-Rincón, Mariano Moscato, Aaron Dutle, and Anthony Narkawicz,Formalization of the Undecidability of the Halting Problem for a Functional Language, Proceedings of the 25th Workshop on Logic, Language, Information, and Computation (WoLLIC 2018), Lecture Notes in Computer Science, Vol. 10944, pp. 196-209, 2018
• César Muñoz, Anthony Narkawicz, and Aaron Dutle,From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems, Proceedings of the 22nd International Symposium on Formal Methods (FM 2018) - Industry Day, Lecture Notes in Computer Science, Vol. 10951, pp. 647-652, 2018
• Laura Titolo, Mariano Moscato, César Muñoz, Aaron Dutle, and François Bobot,A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm, Proceedings of the 22nd International Symposium on Formal Methods (FM 2018), Lecture Notes in Computer Science, Vol. 10951, pp. 364-381, 2018.
• Mariano Moscato, Laura Titolo, Aaron Dutle and César Muñoz,Automatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis, Computer Safety, Reliability, and Security. SAFECOMP 2017. Lecture Notes in Computer Science, Vol. 10488, pp. 213-229, 2017.
• Anthony Narkawicz, César Muñoz, and Aaron Dutle,The MINERVA Software Development Process, Automated Formal Methods, Menlo Park, California, 2017.
• Aaron Dutle, Mariano Moscato, Laura Titolo and César Muñoz, A Formal Analysis of the Compact Position Reporting Algorithm, , Proceedings of the 9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2017).
• Aaron Dutle, Bill Kay, Graph odometry, Discrete Applied Mathematics, Volume 214, 11 December 2016, Pages 108-115.
• Rania W. Ghatas, Devin P. Jack, Dimitrios Tsakpinis and Michael J. Vincent, James L. Sturdy, César Muñoz, Keith D. Hoffler, Aaron M. Dutle, Robert Myer, Anna M. DeHaven and Tod Lewis, and Keith E. Arthur,Unmanned Aircraft Systems Minimum Operational Performance Standards End-to-End Verification and Validation (E2-V2) Simulation, Technical Memorandum, NASA/TM-2017-20780, January 2017.
• César Muñoz, Aaron Dutle, Anthony Narkawicz, and Jason Upchurch, Unmanned aircraft systems in the national airspace system: a formal methods perspective, ACM SIGLOG News 3, August 2016, Pages 67-76.
• Anthony Narkawicz, César Muñoz, and Aaron Dutle, Coordination Logic for Repulsive Resolution Maneuvers, Proceedings of the 16th AIAA Aviation Technology, Integration, and Operations Conference (ATIO 2016), AIAA-2016-2756, 2016.
• César Muñoz, Anthony Narkawicz, George Hagen, Jason Upchurch, Aaron Dutle, María Consiglio, and James Chamberlain, DAIDALUS: Detect and Avoid Alerting Logic for Unmanned Systems, Proceedings of the 34th Digital Avionics Systems Conference (DASC 2015), Prague, Czech Republic, 2015.
• Anthony Narkawicz, César Muñoz, and Aaron Dutle, Formally-Verified Decision Procedures for Univariate Polynomial Computation Based on Sturm’s and Tarski’s Theorems, Journal of Automated Reasoning, Volume 54, Issue 4, pp. 285-326, 2015.
• Aaron Dutle, César Muñoz, Anthony Narkawicz, and Ricky Butler, Software Validation via Model Animation, Proceedings of the Proceedings of the 9th International Conference on Tests and Proofs (TAP 2015), Lecture Notes in Computer Science, Vol. 9154, pp. 92-108, 2015.
• Éva Czabarka, Aaron Dutle, Travis Johnston, László A. Székely, Abelian Groups Yield Many Large Families for the Diamond Problem, European Journal of Mathematics, Vol. 1, No. 2, Pages 320-328, 2015.
• Joshua Cooper, Aaron Dutle, Computing hypermatrix spectra with the Poisson product formula , Linear and Multilinear Algebra, Vol. 63, No. 5, Pages 956-970, 2015.
• Éva Czabarka, Aaron Dutle, Péter L. Erdős, István Mikloós, On realizations of a Joint Degree Matrix, Discrete Applied Mathematics, Vol. 181, Pages 283–288, Jan 2015.
• Joshua Cooper, Aaron Dutle, Greedy Galois Games, American Mathematical Monthly, Vol. 120, No. 5, Pages 441-451, May 2013.
• Joshua Cooper, Aaron Dutle, Spectra of Uniform Hypergraphs, Linear Algebra and its Applications, Vol. 436, No. 9, Pages 3268-3292, May 2012. (Over 375 Citations according to Google Scholar)

Technical Committee Work

• Member of RTCA Special Committee 228, Minimum Operational Performance Standards for Unmanned Aircraft Systems.
• Member of RTCA Special Committee 186, Automatic-Dependent Surveillance Broadcast.
• Member of RTCA Special Committee 147, Traffic Alert and Collision Avoidance System.
• Member of RTCA Special Committee 240, Topics on Software Advancement.

Conference Committee Work

• Member of the Program Committee for:
  • NSV 2020: 13th International Workshop on Numerical Software Verification
  • NFM 2020: 12th Annual NASA Formal Methods Symposium
  • FVPS 2019: 2nd Workshop on Formal Verification of Physical Systems
  • NFM 2019: 11th Annual NASA Formal Methods Symposium
  • CPP 2019: The 8th ACM SIGPLAN International Conference on Certified Programs and Proofs
  • FVPS 2018: Formal Verification of Physical Systems
  • ITP 2017: The Eighth International Conference on Interactive Theorem Proving
• Co-Chair of the Program Committee, along with Mariano Moscato and Laura Titolo, for the 13th NASA formal Methods Symposium (NFM), held in May 2021.
• Co-Chair of the Program Committee, along with César Muñoz, for the 10th NASA formal Methods Symposium (NFM), held in April 2018.