Shriram Krishnamurthi - US grants

This project emphasizes the principles of problem solving and program design using Scheme. Students learn to solve problems in a systematic manner and are able to use those skills in many domains, not just computing. The pedagogical approach is based on the belief that the conventional approach to computer science in high school is inappropriate, and, with an emphasis on code generation and successive modification by steps, is more consistent with computer science from the early 1980s. The emphasis on grammar rules is inconsistent with current methods. The results-dated methodologies have been that secondary schools have small computer science enrollments and encounter diminishing interest even by the more mathematically inclined students.

The project is based on the introductory computer science curriculum developed at Rice University, and the PIs have tested these methods in high schools and found the students to be more receptive and to learn more about computational problem solving. The approximately 310 participating teachers learn a dramatically different and more applicable approach through workshops at Northeastern University, Adelphi University, Brown University, the University of Utah, and Worcester Polytechnic Institute. Teachers are introduced to the new content, approaches and software. A central Web repository is maintained for distribution and exchange. The teachers receive forty contact hours and extensive follow-up activities and supports plus 3 graduate credits.

0305950
Krishnamurthi, Shriram, -
Brown University
Collaborative Research: Compositional Verification of Software Product
Lines as Open Systems

0305834
Fisler, Kathryn, -
Worcester Polytechnic Institute
Collaborative Research: Compositional Verification of Software Product
Lines as Open Systems

A product line is a family of related software products built from a common set of components, where each component typically implements a distinguishable feature. While product lines have many demonstrated
software engineering benefits, they pose a nontrivial challenge for traditional methods of testing and validation. Prior work, including case studies, has developed compositional techniques for automated
verification of temporal logic formulae over product lines. The case studies have revealed the need for techniques that handle open system verification sensitive to (a) propositions that evolve over time and
across features, and (b) propositions that behave differently depending on whether they model control or data. This project, a collaboration between Brown University and Worcester Polytechnic Institute, extends prior work to handle these issues using a particular combination of propositional, temporal, and 3-valued logic constraints. The combined representations lead to lightweight preservation checks, a crucial part of keeping product-line verification tractable. The work includes both theoretical work and
experimental validation. The project both contributes to advancing an important software development methodology and narrows the gap between the areas of software engineering and computer-aided
verification. The work involves undergraduate students and will have impact through classroom contact at several levels.

ABSTRACT
0429492
Shriram Krishnamurthi
Brown University

As programs evolve, their code becomes increasingly tangled by the addition of both programmers and requirements. This mosaic quality complicates program comprehension and maintenance. The lack of
quality documentation in most systems further complicates this process.

A new developer is likely to approach a system with the same mindset as a user, viewing the system as a collection of features, not in terms of its internal structure. The proposed research thus describes
program fragments in terms of the features they impact, so developers can assess the effect their changes are likely to have and, in particular, be alerted to unexpected consequences. It will do this by exploiting information provided in the program's test suites.

The proposal should result in tools to help programmers such as a better, ``semantic'' code browser; an assistant to generate better version-control documentation; and an analysis of test suite dependencies. It will also study questions that facilitate future programming language design. Broader impact will include introducing new, related ideas into software engineering education and training undergraduates to conduct research.

Access-control policies have grown from simple matrices to non-trivial specifications in their own right: they are written, separately from the applications that use them, in domain-specific languages; they are often composed of (sometimes geographically distributed) fragments, which are combined using semantically rich policy-combination operators; and they consult a dynamic environment comprised of information from many sources including the underlying application and the operating environment of the system. These features make policies hard to get right, in part because policy authors must understand how their policies will interact with an environment that is constantly changing.

Policy authors thus need increasingly strong tools to help understand the effects of their policies. These tools must support common authoring scenarios. Authors often have a policy that "works" and a new policy that encapsulates a desired change. Testing can foster confidence that the changes do what is desired, but generally miss effects that weren't expected. For such scenarios, it is far more useful to employ a process such as change-impact analysis, which semantically compares two policies while respecting the dynamic nature of the environment. Traditional property-based analyses such as formal verification, while useful, do not support this scenario.

This project is developing the theoretical foundations and prototype tools for analyzing realistic access-control policies in their dynamic environments. The tools support both property-based verification and property-free analyses such as change-impact analysis for industrial standard policy languages (such as XACML). The novel components of this project are its fine-grained and rich model of the dynamic environment and its focus on property-free analyses that accommodate common authoring scenarios.

Project Abstract:

Without their realizing it, end-users have been turned into authors of access-control policies. Everywhere from Google to Facebook to Microsoft HealthVault and beyond, these policies are usually hidden behind simple user interfaces, but ultimately the users are responsible for setting and then taking responsibility for the consequences of these policies. Indeed, the apparent simplicity of the interfaces sometimes belie the significance of the outcomes.

Because applications are a black-box to end-users, it becomes difficult for users to predict the consequences of an action. Users see only their view of the world, but their access-control decisions affect the views of others. End-users need tools to determine the effect of their decisions, with special emphasis on the effect of policy changes. This project is developing user-friendly means to browse and investigate the details of these effects and changes. The underlying techniques are firmly grounded in theory, resulting in formal accuracy guarantees rather than approximate answers. The tools themselves summarize information in ways that account for the cognitive expectations and biases of users.

The broader impact of this project comes from the focus on end-users rather than programmers and other technical users. Some end-users are too eager to embrace new technologies without fully appreciating their consequences, while others are too tentative due to their concern about (sometimes imaginary) problems they might create. The tools from this project help the former become more cautious, and the latter more confident. The net result should be a more savvy, yet vastly more inclusive, Cyber society.

Over the last decade, scripting languages have assumed a huge role. Initially web developers used Perl and Python to enrich the content of web servers; later Ruby on Rails took the scene by storm. Over the same period, JavaScript has become the dominant language on the client side of the web. Additionally, the popularity of scripting language has inspired developers to use them for the construction of many other kinds of systems, including mission-critical real-time systems.

While scripting languages are productive tools for the exploration of design ideas, their use also introduces several new kinds of problems into the software cycle. Most basically, scripting languages tend to lack a type system, which tends to raise the debugging and maintenance costs for systems. Worse, even though scripting languages tend to be safe, their flexible primitive operations induce difficult-to-predict behavior in programs and thus creates novel kinds of security holes. At the same time, scripting languages do not come with a well-defined semantics, making it nearly impossible to validate the soundness of a program analysis for safety or security properties.

In response to these observations, this proposal promises to re-engineer the semantics of scripting languages. Specifically, the PIs propose to investigate the construction of executable semantics for three scripting languages: JavaScript, Python, and Racket. They will use the language-level test suites to check that the semantics model the implementations adequately. In addition, the PIs will use the semantics to design and validate type systems and program analyses for these scripting languages.

Over the long run, the proposal should impact the world at large in three ways. First, the type systems and analyses for scripting languages should help software developers improve the safety of their software and reduce their maintenance cost. Second, the semantics for the scripting languages will help researchers validate their ideas concerning program analyses. Finally, the PIs will develop a process for semantic re-engineering that should be useful to many additional scripting language communities.

Application stores use sophisticated user interfaces to help users understand the permissions sought by applications. Unfortunately, these interfaces are complex and may fail to address their goal of helping users give informed consent. As a result, users may inadvertently surrender private information or open themselves up to security attacks.

This project tackles the problem of improving the nature of information provided by these interfaces. It focuses both on new interface designs that will better represent this information, and on techniques to bootstrap the provision of that information. On the user interface side, it designs new interfaces that help untrained users recognize the security and privacy consequences of the sought permissions. To populate this information, it posits the use of crowdsourcing to obtain information at scale about the suitability of permissions. The goal is to eventually populate an application store with this information to encourage adoption and additional feedback from users. The project will study how effectively and accurately crowdsourcing can be used to gather this information.

As computing has become such an integral part of the STEM disciplines, the STEM+Computing Partnership (STEM+C) program advances the integration of computational approaches in STEM teaching and learning and how this integration can improve STEM learning, engagement, persistence, and computational thinking. Computational Thinking (CT) is a relatively new educational focus and a clear need for learners as a 21st century skill. This proposal tackles this challenging new area at the high school level by leveraging a curriculum designed to integrate mathematics and computing to improve learning in both to understand how learning these two subjects together can lead to improvement in both students' understanding and teachers' perceptions of and knowledge about these subjects. Understanding the ways that learning mathematics impacts learning computing and vice-versa is an important research goal. Learning computing is vital for preparing today's students for the many job opportunities available in this area. In addition, the project will train over 600 teachers in diverse schools in using this curriculum, leading to a strong possible impact on improving learning and retention in STEM and computing.

The project will investigate the ways that learning mathematics and programming mutually influence each other. The project uses the Bootstrap curriculum in which students program videogames. Bootstrap is a function-based computing language that targets important algebraic concepts. The curriculum is designed around key mathematical practice standards to help teachers incorporate it into their existing courses. The research on student learning will focus on: 1) which of the intended concepts transfer from Bootstrap to algebra, 2) the type of scaffolding that best supports this transfer, and 3) the aspects of the curriculum that contribute to that transfer. The research on teachers will focus on: 1) the effect of using Bootstrap on teacher perceptions of connections between math and computing, 2) the aspects of the curriculum's pedagogical style and the professional development provided that affect teachers skill and confidence level teaching computing, and 3) possible differential effects for teachers whose primary area was mathematics or computing prior to using Bootstrap. In addition to the 200 teachers the project team has already trained, they will train an additional 600 teachers over the course of the project. During the project, they will collect teacher data from at least 100 teachers in each year for Years 2 and 3 of the project and student data from 20 of those teachers' classes.

Brown University proposes to create lightweight data science curricula for K-12. Data science can be roughly defined as "programming + statistics" and thus has two points of control: how much programming is needed, and how much statistics is used. The term "lightweight" here is not used pejoratively but to connote an approach that is aligned with the CS for All Initiative's goal of scaling CS education to all schools and all students. This project will limit mathematics to "naïve" statistics rather than depending on continuous mathematics. For programming, the curriculum will create support that requires no more sophistication than required by CS Principles curricula, and perhaps even less. Finally, it will also be light on setup, using Google Sheets as the primary "database" system, lifting a big administrative burden on teachers and schools, and enabling elegant user interfaces that are already familiar to many students and teachers.

The programming support will be embedded into Pyret, a pedagogic programming language, extending it with direct support for tables and tabular operations. This will allow students to write concise programs using constructs designed to be evocative of SQL. To increase access to younger students and to limit typing, the PIs will incorporate a dual-mode block-and-text interface into Pyret. In order to engage more students, the work will include support for curricular personalization, allowing students to pick out the topics that they are interested in, and find the corresponding questions they want to ask about these data. The PIs will provide curated datasets, as well as means for teachers to find other similar data, to help students who need suggestions to get started. Finally, building on previous work of the PI and others, project will involve some preliminary investigation on whether providing high-level constructs and letting teachers teach "to the constructs" will naturally lead to better plan composition.

Integrating computing and mathematics appeals to various stakeholders for a variety of reasons. For the mathematics education community, computing offers an application of mathematics concepts that may strengthen teachers' and students' mathematical understanding; for the computer science (CS) education community, integration enables equitable access to computing education for all students; for state boards and districts, integration accommodates staffing and curricular constraints while targeting core learning objectives in multiple disciplines. Bootstrap is a nationally-deployed curriculum that integrates computer science and algebra. Bootstrap's current professional development (PD) program for math teachers is a 3-day in-person event which assumes that teachers are somewhat facile with algebraic functions. Both Bootstrap and the National Council for Teachers of Mathematics (NCTM) have observed that some teachers have a weak command of functions. School districts would prefer a shorter in-person PD to reduce staffing costs and increase flexibility. This project will use a hybrid PD model to address both needs. Simultaneously, the project will research ways to tailor the online content to be effective for teachers who differ in their understanding of functions, goals for pursuing PD, and interest in mathematics, computing, math/CS integration, and student thinking. This Researcher-Practitioner Partnership team includes Bootstrap; NCTM (specifically its Math Forum team, which has expertise in on-line training); Brown University; Swarthmore College; the Oklahoma State Division of Secondary Mathematics and Computing Education and school districts in Texas. A total of 270 middle-school math teachers---a majority from rural areas or serving Native American or Hispanic students in our partnering regions---will participate in Bootstrap PD under this project. Assuming typical adoption rates, these teachers should reach 6,000 students within the project period alone. Building Bootstrap content into the Math Forum will expose thousands of NCTM's teachers to the potential of integrated math/CS curricula.

The team will use design-based research to develop and deploy a hybrid PD model and online support community for Bootstrap teachers, augment Bootstrap PD to reinforce teachers' understanding of algebraic functions, and conduct quasi-experimental studies to inform the design of different pathways through the PD. This project will study how to develop teachers' understanding of CS while also strengthening their math proficiency. In particular, the project will explore the possibilities for CS to improve teachers' understanding of algebraic functions. The project also will study ways in which teachers' interest can be made visible and useful in improving engagement and learning in integrated CS and mathematics PD. The results should apply to integrative programs beyond Bootstrap, suggesting strategies to tailor PD to serve more teachers.

Brown University will explore how to enable math teachers to effectively teach computing online. Bootstrap is a national-scale outreach program that helps K-12 teachers integrate introductory computing into existing classes, such as math, physics, and social studies. Like many programs, Bootstrap has shifted to virtual professional development (PD) for Summer and Fall 2020. Its teachers are also preparing to teach with a combination of remote and socially-distanced instruction. For teachers with limited prior computing background, simultaneously learning and preparing to teach computing in a new (online) format demands significant cognitive overhead. Teachers must learn to effectively use programming tools, but also how to manage attention across these tools, lecture slides, digital worksheets (that would have been on paper for in-person learning), and potentially a videoconference session. With many learners (teachers and students) working on tablets or Chromebooks without external monitors or access to printers, the cognitive demands become considerable. This EAGER project explores how teachers in the integration context experience workload and develop non-cognitive dispositions that are known to impact the effectiveness of virtual PD in computing.

Brown University will seek to understand and mitigate the additional challenges that math teachers face when learning to integrate computing into their courses, both in virtual PD and in virtual teaching. Collected data will be largely qualitative, in the form of surveys, check-in questions embedded in PD sessions, interviews with teachers, and field observations during PD. Surveys will be designed to account for a variety of underlying factors, including cognitive task load, confidence, motivation, and interest. The project will result in case studies, findings about effective design of PD and instruction in virtual contexts, and curricular materials adapted for virtual instructional settings. Revised curricular materials will be freely available online. The assessments and materials will be designed for teachers in various situations, including those teaching remotely, those teaching in person but under student social-distancing, and those in rural areas, who have been requesting virtual PD independently of COVID. The latter, in particular, will make this work relevant even after in-person teaching and learning is able to resume.

This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

Roughly half of the US states have adopted K-12 Computer Science (CS) standards to date. Many districts, however, cannot afford standalone CS classes because they lack funding, available time in the curriculum, and/or a pool of qualified teachers to hire from. Integrating CS into existing courses (e.g., math, science, social studies) is a promising alternative. Rather than computer science being taught as an elective that not all students take, it could be taught more equitably in core courses. Moreover, districts could save resources through this strategy. Integration also showcases how computing is not inward-looking but can impact other disciplines. Unfortunately, very little research guides districts on how students learn CS in integrated contexts or how teachers gain confidence, interest, and skill to teach integrated computing content. This project, a partnership between Bootstrap and the Oklahoma Department of Secondary Education, is studying these questions in the context of integrating CS into Oklahoma's 8th and 9th grade math framework. Because these challenges to introducing CS to schooling are pervasive nationwide, this project can serve as a model for meeting these challenges. The project is also producing research findings on creating effective professional development for teachers new to CS and how these teachers develop their capacity for CS instruction.

This project builds on an existing Research-Practitioner Partnership (RPP) in Oklahoma that has been studying how to prepare math teachers to start integrating computing into their classes. This award expands this ongoing work to prepare teachers to integrate computing in more depth and more extensively, with 135 teachers. Using design research, results from educational psychology, and our findings to date, this project is (a) developing a 2-stage, hybrid professional development program that fosters teachers' confidence and interest in computing (including a variant specifically designed to support rural teachers), (b) adapting lessons from the state math framework to include standards-aligned computing tasks, (c) studying teachers' process of change in thinking about integration, and (d) beginning to study impacts on students. The mixed-methods research draws on surveys and longitudinal interviews with teachers, recordings of classrooms, samples of student work, and data on student assessments. This project is funded by the CS for All: Research and RPPs program.

This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

Formal logics are widely employed in computer science to precisely state a user's intent. These can be used in many different ways: an existing system can be checked to conform to these statements, or a fresh system can even be generated that obeys these intentions. However, humans often have various misconceptions about these logics, which taints any subsequent use of them: if the logical statement means something other than what the human intends, then it is not merely useless, it is actively misleading. The project's novelties are to elucidate these misconceptions and to evaluate methods to correct them. The project's impacts are in aiding education, in the creation of tools to help authors, and also in the design of new formal logics.<br/><br/>Concretely, the project aims to investigate misconceptions in three formal settings: Linear Temporal Logic, the Alloy language (a first-order logic with transitive closure), and in basic structural properties used widely in formal specification (such as transitivity). The project uses a variety of methods to elicit misconceptions, taking into account the need to overcome expert blind spots. The project also employs techniques from the existing misconception literature to overcome the problems that it finds. The resulting study instruments and techniques to address misconceptions would be immediately useful in many settings, and the general flow of the work would be broadly applicable to others who wish to reproduce it for their preferred logics.<br/><br/>This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.