Jonathan Aldrich Professor, Affiliated Faculty Website CMU Scholars Page Office 422 TCS Hall Email aldrich@cs.cmu.edu Phone (412) 268-7278 Department Institute for Software Research Computer Science Department: Affiliated Research Interests Formal Methods Programming Languages Security and Privacy Software Engineering Advisees Sean O'Connor Research/Teaching Statement My research goal is to improve the quality and security of software and the productivity of engineers by providing novel ways to express and enforce structural and behavioral aspects of software design within source code, typically through language design and type systems. I both prove formal properties of the systems I develop, and also evaluate their practical benefits via case studies, human subjects experiments, and corpus studies with open source codebases. A Programming Language for Secure Web and Mobile Development. We are currently designing a new programming language called Wyvern that is designed to help in developing highly secure web and mobile applications, while at the same time enhancing developer productivity. Research on this project includes a novel object model and versioned module system that provides a foundation for security, and an extensible language and type system, which supports domain-specific languages for UI layouts, distributed application architectures, and security policies. Lightweight Formal Methods show great promise for helping software engineers write secure software, avoid defects, and achieve high parallel performance and other non-functional goals. I am interested in how language and type system design can be used to more effectively check a range of critical software properties. We are currently developing an approach, for example, that provides a simple typed interface to a parallel library, while using more sophisticated formal methods to prove that subtle concurrency tricks used in the library are correct. This approach may thus be able to provide both high usability and high performance—an elusive combination in past work. More broadly, I am interested in using formal abstractions that capture engineers’ informal reasoning, especially in the presence of challenges such as concurrency and mutable aliased state.
