Kathi photo Kathi Fisler
Research Professor, Computer Science
Associate Director of the CS Undergraduate Program
Co-Director, Bootstrap
(previously Professor, WPI Computer Science)

CIT 309 | 401-863-7607 | kfisler@cs.brown.edu

Brown PLT

I'm interested in various facets of how people learn and use formal systems. My current focus is computing education, with an emphasis on how programming languages impact learning and pedagogy in computing. I've also worked on diagrammatic logics for hardware design (late 1990s), modular verification of feature-oriented programs (early 2000s), and reasoning about access-control and privacy policies (mid-late 2000s). Those projects emphasized formal systems over human reasoning. My work in computing education tilts the balance, but is part of the same broad theme.

I have been heavily involved in outreach for K-12 computing education since the late 1990s.

Current Projects

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 immplementations. 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.