Alwyn E. Goodloe

I am a computer scientist working in Formal Methods group of the Safety Critical Avionics Systems Branch at NASA's Langley Research Center.

Research

My primary research focus is in the area of formal methods applied to safety critical systems. In particular, my recent research has been in the areas of

• Protocol verification
• Runtime verification
• Verification of Numerical Programs
• Functional Programming
• Interactive theorem proving with PVS
• Test generation from formal specifications
• Generating Java code from PVS specifications
• Fault-tolerant computing
• Verification of algorithms for air space management

My doctoral research was conducted under the direction of Carl A. Gunter and primarily focused in the area of network security and I still have a strong interest in network security, configuration, and analytics. I also conducted some work in embedded systems. My masters thesis in math was in computer algebra.

Education

• Ph.D. Computer and Information Science, University of Pennsylvania, 2008
• MSE Computer and Information Science, University of Pennsylvania, 2000
• MSc Mathematics, George Mason University, 1992

European Summer Schools

• NATO Summer School on Models, Algebras, and Logics, Marktoberdorf, Germany, July 2002.
• European Education Forum Summer School on Specification, Refinement, and Verification, Turku, Finland, August 2002.

Selected Papers

• L. Pike, N.Wegmann, S. Niller, and A. Goodloe. Copilot: Monitoring Embedded Systems, in Innovations in Systems and Software Engineering, Volume 9, Issue 4, 2013.
• A. Goodloe, C. Munoz, F.Kirchner, and L. Correson. Verification of Numerical Programs: From Real Numbers to Floating Point Numbers, in Proceedings of 5th NASA Formal Methods Symposium (NFM 2013), Lecture Notes in Computer Science, Vol. 7871, pp. 441-446, May 2013.
• L. Pike, N.Wegmann, S. Niller, and A. Goodloe. Experience Report: A Do-It-Yourself High-Assurance Compiler, International Conference on Functional Programming (ICFP), 2012.
• A. Goodloe and C. Munoz. Compositional Verification of a Communication Protocol for a Remotely Operated Aircraft, Science of Computer Programming, Volume 78, Issue 7, pp. 813-827, 2013*. This paper is an extended version of the conference publication in Lecture Notes in Computer Science, Volume 5825, November 2009.
• L. Pike and A. Goodloe. Copilot: A Hard Real-Time Runtime Monitor. To appear in Proceedings of 1st International Conference on Runtime Verification. 2010.
• A. Goodloe and L. Pike. Toward Monitoring Fault-Tolerant Embedded Systems. In Proceedings of 1st International Workshop on Software Health Management. 2009.
• A. Goodloe and C. Pasareanu and D. Bushnell and P. Miner. Test Generation Framework for Distributed Fault-Tolerant Algorithms. In Proceedings of Automated Formal Methods. 2009.
• A. Goodloe and C. A. Gunter. Completeness of Discovery Protocols. In Proceedings of ACM Workshop on Assurable and Usable Security Configuration. 2009.
• A. Goodloe and C. Munoz. Compositional Verification of a Communication Protocol for a Remotely Operated Vehicle. In Proceedings of Formal Methods and Industrial and Critical Systems. Lecture Notes on Computer Science 5825,Springer-Verlag. 86--101. 2009.
• A. Goodloe and C.A. Gunter. Reasoning about Concurrency for Security Tunnels.In 20th IEEE Computer Security Foundations Symposium. July 2007.
• A. Goodloe, M. Jacobs, G. Shah, and C.A. Gunter. L3A: A Protocol for Layer Three Accounting. In Proceedings of the First Workshop on Secure Network Protocols (NPSEC), 2005.
• A. Goodloe, C. A. Gunter, and M.-O. Stehr. Formal Prototyping in Early Stages of Protocol Design. In Proceedings of the Workshop on Issues in the Theory of Security (WITS'05). The ACM Digital Library, 2005.
• A. Goodloe, M. McDougall, C.A. Gunter, and R. Alur. Predictable Programs in Barcodes. In Proceedings of International Conference on Compilers, Architecture and Synthesis of Embedded Systems (CASES), 298-303, 2002.
• A. Goodloe, M. McDougall, C.A. Gunter, and R. Alur. Predictable Programs in Barcodes. In Proceedings of International Conference on Compilers, Architecture and Synthesis of Embedded Systems (CASES), 298-303, 2002.
• A. Goodloe and P. Loustaunau. An Abstract Data Type Development of Graded Rings, In Proceedings of the International Symposium on the Design and Implementation of Symbolic Computation Systems (DISCO), Lecture Notes in Computer Science 721, 192-202, 1992.

Technical Reports

• A. Goodloe and L. Pike. Monitoring Distributed Real-Time Systems: A Survey and Future Directions. NASA Technical Report. 2010.
• C. Munoz and A. Goodloe. Design and Verification of a Distributed Communication Protocol. NASA Technical Report. 2008.
• A. Goodloe, M. McDougall, C. A. Gunter, and M.-O. Stehr. Designand Analysis of Sectrace: A Protocol to Set Up Security Associations in IPsec. CIS Department Technical Report, University of Pennsylvania, 2004.
• A. Goodloe, M. McDougall, C. A. Gunter, T. Hiller, and P. McCann. Authenticated Traversal. CIS Department Technical Report, University of Pennsylvania, 2002.

My dissertation and research papers in network security can be found on the tunnel calculus page at the Illinois Security Lab.