Current Projects
Data-Centric Computing Education
With both computing and data science becoming essential across disciplines, it's time to rethink introductory computer science education. We're developing data-centric computing as a blend of computer science, data science, and data engineering that provides skills to students across campus. We have an op-ed summarizing the goal, an introductory collegiate course, and a textbook (released August 2021). Our decisions are driven by our research in computing education. Our Bootstrap:Data Science curriculum provides a high-school pre-cursor for those starting in K-12.
Program Design and Plan Composition in Computing Education
Programming problems typically contain multiple subtasks, solutions to which must be integrated into a single program. This project explores how novice programmers decompose problems and compose subtask implementations. Our work emphasizes both the impact of programming languages and libraries on planning behavior, and pedagogies for teaching program design, planning, and composition.
Cross-Discipline Transfer of Knowledge in Computing Education
Bootstrap produces a family of curricula that integrate computing education for middle- and high-school students with other disciplines (such as algebra, physics, and social sciences). The research components of this project study the pedagogical techniques and curricular conditions under which knowledge gained through computing transfers back to the host discipline (and vice-versa for teachers).
Notional Machines for Computing Education
Notional machines are the abstract machines that programmers are attempting to control when they write programs. Different programming languages afford different notional machines, which in turn allow different misconceptions about language behavior. We are studying tradeoffs among notional machines and pedagogies for avoiding misconceptions in various CS courses, both intro- and upper-level.
Past Projects
Security Policy Analysis
Analysis of Datalog-based policies, such as those used for access-control and privacy. Our Margrave policy analyzer was a SAT-based engine for verifying properties of policies, as well as for verifying and exploring consequences of changes to policies. We also worked on models of how policies interact with underlying software systems.
Feature-Oriented Software Verification
Features are cohesive, user-facing behaviors of systems. Feature-oriented designs (like aspect-oriented design) modularize code around features. Shriram Krishnamurthi and I developed a theory of compositional verification of feature-based software designs; our approach generated logical constraints as interfaces on features used in open systems (in which not all features were known in advance).
Formal Reasoning with Timing Diagrams
Given a semantics, timing diagrams become a formal representation of system behavior. This project explored semantics and analysis techniques for such specifications. I proved that timing diagram verification is decidable, even though timing diagrams capture some non-context-free languages.