|
I'm interested in the interplay between the logics that people use when solving problems and the formal logics used to encode those problems in software. While my early career focused on problems in the formal verification of hardware and software systems, these problems shared a common theme of exploring a human perspective on or representation of a software task. I am now pushing that theme further, to really study how human reasoning styles interact with software tools that attempt to encode aspects of human reasoning. I remain interested in verification, but much more as a means than as an end.
I'm most interested in problems that explore how to make software support the way people reason in practice. This area has both logical and cognitive dimensions. Ideally, I want my work to help build tools that work with, rather than against, how people think through problems in practice.
I am always on the lookout for motivated undergraduate and graduate students. My work requires background in discrete math and logic, experience implementing software tools, and interest (but not necessarily background) in human aspects of computing. See the pages on IQP/MQP projects or RAships for more information.
Current Projects (publications)
Back Burner Projects
Access-control policies have grown beyond simple access-control lists. Modern policies involve hundred of rules and classes of users. They are increasingly written in domain-specific policy languages and are composed of multiple fragments written by different authors. Furthermore, policies run in the context of sophisticated application programs, which can affect the data on which policy decisions depend. All of these factors make policy authoring and maintenance complicated and error-prone.
Shriram Krishnamurthi, Dan Dougherty and I are building models and tools for formally analyzing access-control policies in the context of application programs. In addition to conventional property-based verification, we are interested in analyses that help authors understand policies in the absense of formal properties. Semantic policy differencing (aka change-impact analysis) is one example: given two policies, it computes the sets of program events and access requests that lead to different decisions under those policies.
The Margrave policy analyzer supports query analysis, property verification, and change-impact analysis for basic role-based access control policies (that can be encoded in propositional logic). Our more recent work considers richer policies as captured in Datalog and their interactions with application programs. We are interested in supporting realistic applications and policy languages, such as the OASIS standard XACML language (which Margrave supports). Details are in our publications.
Diagrams are an important tool in problem solving. In domains ranging from mathematics to architecture to political science to engineering, people develop and communicate ideas through diagrams. This pervasive use in such widespread areas has inspired much research into the nature of diagrammatic reasoning. This research generally takes one of two perspectives: the cognitive or the logical. The cognitive perspective explores diagrams' role in human thought processes. The logical perspective explores the mathematical nature of diagrammatic representations. These perspectives are complementary, and help paint a broad picture of diagrammatic reasoning.
Relatively little work, however, has presented a computational perspective of diagrammatic reasoning. Such a view is sorely lacking. A plethora of computer-based tools support problem solving in a variety of domains. Recognizing the cognitive advantages of visual information, many of these tools employ graphical or visual interfaces in order to attract and support users. Beneath the interface, however, these tools generally translate the diagrams into existing textual representations before running the problem solving algorithms. This approach is sound if the translation is sound, but could the computer-based algorithms operate more effectively on the diagrammatic representations themselves? The computational view on diagrammatic reasoning addresses precisely this question by exploring the potential computational benefits, or computational efficacy of diagrammatic representations. Such work treats diagrams as data structures and studies the algorithms that those data structures engender.
I'm studying the computational efficacy of timing diagrams in the context of formal verification. Timing diagrams have a different expressive power than other common logics for specifying temporal properties (such as LTL); these differences lead to more efficient verification algorithms for timing diagrams. I am trying to characterize the expressive power of various forms of timing diagrams (relative to proposed hardware specification languages) and develop verification algorithms that exploit these expressive differences. I hope to use these results to identify when designers and tools can manipulate specifications diagrammatically instead of textually. My present focus is on using timing diagrams to capture and reason about bus protocols.
Many of the problems that plague software arise from a mismatch between the real world of requirements and the hermetic world of programming. Programmers have long relied on class- or actor-based notions of modularity. The real world, however, discriminates between systems based on their features, caring less for how a programmer implements the features. (For instance, a police officer using a two-way radio cares about whether it supports the features of notification silencing and message dispatching; how these features impact the underlying radio communication, display, and database software---the actors---is not of interest.) This mismatch is telling, because virtually any interesting feature impacts (or ``cross-cuts'') several actors, scattering its implementation through the codebase. This scattering is a prime culprit in complicating software evolution, maintenance, and even validation.
In the past few years, several researchers have had considerable success specifying and building software systems by composing modules that encapsulate features, rather than actors (aspect-oriented programming is the best-publicized example of this work). This post-object-oriented technique immediately helps match the system to its requirements, and aids in its subsequent maintenance. Yet, this alone cannot suffice. We cannot consider a technique for building software complete, or even acceptable, without an accompanying methodology and toolkit for validation. Furthermore, the validation techniques must be as conveniently integrated into the development process as separate compilation to make users willing to apply them: that is, they must also be modular.
Shriram Krishnamurthi (Brown University) worked on modular feature-oriented specification and verification methodologies. We have developed a theory of compositional verification for feature-oriented programs; we are able to verify (model check) features individually, derive constraints that are sufficient to preserve these properties when features are composed, then check that features respect each others' constraints upon composition. Details are available in our publications.