|
JONATHAN ALDRICH
Assistant Professor
Institute for Software Research International
www
My research applies language and program analysis technology to the
challenges of designing, building, and evolving software systems. I
address these challenges using formal techniques in the context of
mainstream programming systems such as Java. To evaluate my work, I
perform exploratory case studies on real applications. These studies
assess both the usability of the techniques I develop and the engineering
tradeoffs that they entail.
Software Architecture represents the high-level structure of a software
system, and can be used to build, analyze, and evolve software more
effectively. My work on the ArchJava project was the first to provide
a rigorous, compile-time guarantee that an object-oriented software
system conforms to a specification of architectural structure. Initial
case studies on real programs suggest that ArchJava is practical and
provides engineering benefits during software evolution. I am currently
extending ArchJava to specify and enforce richer architectural properties,
such as the temporal sequence of architectural events. With David Garlan,
I am also exploring more effective ways to formally model and analyze
software architecture in the presence of dynamism and multiple views.
Lightweight Formal Methods show great promise for helping software
engineers write secure software, avoid defects, and achieve 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. For example, an ownership type system
we are developing will provide the first lightweight, flexible general
way to modularly reason about programs with state. We would like to
build on this type system to support modular model checking of object-oriented
programs. Language design can also aid in checking object protocols,
such as the required ordering of calls to a socket-based communication
library. Finally, I am interested in lightweight verification tools
for embedded and real-time systems, which are notoriously hard to build
and maintain.
Objects and Aspects are emerging programming language paradigms that
support programs with cleaner designs that are easier to evolve. My
current work focuses on ways to make these languages more expressive
while also providing better human and automated reasoning capabilities.
For example, I am developing the first module system for aspect-oriented
programming languages that will allow a library provider to verify
properties of their implementation that will continue to hold even
if clients write aspects that affect the library. Other projects include
better language and tool support for error handling, and a novel object
model that supports both dynamic inheritance and multiple dispatch.
|
