I'm interested in various facts of how people learn and use formal systems. I pay particular attention to the interplay between the logics that people use when solving problems and the formal logics and languages used to encode those problems in software. 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. My work has continued to look at ways in which human reasoning interacts with software tools that encode that reasoning. My current focus is on computing education, particularly the interaction between the languages we use and how we learn to construct programs.
I am always on the lookout for motivated undergraduate and graduate students. See the pages on IQP/MQP projects or RAships for more information.
Current Projects (publications)
Older or Back Burner Projects
How can we teach K-12 students about computing and programming in a way that fits with both the learning goals and logistical constraints of schools? CS educators have generally accepted animations and blocks languages as critical tools, but there has been less research on the pedagogy that should accompany those tools.
Bootstrap teaches students to build their own videogames while reinforcing algebra (as defined in both state and Common-Core standards for math education). Our choice of language and curricular structure are designed explicitly to reinforce algebraic concepts, while simultaneously teaching programming. Bootstrap was designed by Emmanual Schanzer, and now involves a larger team.
As part of this project, we develop curricula, train teachers to use the curriculum, evaluate the impact on algebra education, and produce online materials for self-learners (in progress, summer 2012 -- check back in fall 2102!). Students on this project can help us develop software and run evaluations to understand the impact of our approach.
Plan composition---the process of interleaving code for different tasks in a single program---has been a theme in computing education research starting in the 1980s. Several classic papers and projects show that students struggle to compose plans for seemingly straightforward problems coming out of CS1. The papers in this area share some linguistic assumptions and constraints, however, that appear to force students into compositions that are harder to get right. It is therefore worth asking what sorts of differences we see in plan composition ability across students who learned to program in different styles of programming languages.
As a long-time fan of functional programming, I started this work by exploring how plan composition skills manifest in students who use functional programming in CS1. I am in the early stages of some cross-linguistic projects (with collaborators who favor other programming styles) that hope to tease out the affect of programming language and constructs taught on plan composition.
More generally, I am interested in reviewing various classic results from computing education that were done only in control-heavy imperative programming to see whether the results hold in different styles.
How do we tailor programming environments to beginning programmers? Most programming tools target either professional programmers or raw novices (through blocks-based programming). How do we support the beginning programmer who is learning in textual languages (either as a first experience, or following on experience in a blocks-based language)?
Shriram Krishnamurthi and I are studying effective error message for beginning programmers in textual languages. We explore student responses to programming errors through combinations of studying their code edits, talk-aloud and observational studies, and quizzes on what error messages mean. Our goal is to understand how to effectively present errors from the perspectives of both students' cognitive models of programming and the user-interface choices within tools.
This work lives within the broader DrRacket project, which provides programming environments that also support early programmers. Our most recent work is using WeScheme, a web-based programming environment (built by Danny Yoo) in the spirit of DrRacket. Students on this project help us understand how students respond to errors and help us build and evaluate new error-message mechanisms in programming tools.
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.