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.

Software is multidimensional; it has many representations besides the
program source. These include formal specifications, test suites,
documentation and even the development history. As software evolves,
these dimensions must stay consistent and reflect each other as
thoroughly as possible. In practice, however, while these are usually
consistent when first created, they tend to receive unequal attention
and therefore gradually become inconsistent. Programmers thus
typically rely on the source code to the exclusion of most other
dimensions.

This project's goal is to help programmers cope with software
evolution by viewing the dimensions of software as constraints on one
another. The project proposes a constraint representation common to
the different software dimensions. Software evolution then becomes a
process of maintaining consistency between constraints. These
constraints also help programmers identify high-level features in
their system, and generate rationales to document design decisions.

The escalating costs of software maintenance give the project
immediacy and its results high significance. It will have immediate
impact by developing tools for programmers to use. It will have
effect over the long term by employing these tools in educational
settings so future developers have a better appreciation for the
importance of maintaining the multiple dimensions of software.

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.

0305949/0306269

Matthias Felleisen (Northeastern University)
Shriram Krishnamurthi (Brown University)

Over the past few years, the Web has evolved from a static medium into a dynamic one. Many Web sites now enter into interactive dialogs with consumers. Unfortunately, the existing technology for building
interactive Web services is inherently flawed. As a result, many Web programs are broken and cannot keep up with consumers' actions in Web browsers.

The investigators propose to investigate the foundations of Web services. Specifically, they will develop models of interactions on the Web; they will use the models to study common errors in interactive Web
programs; and they intend to develop protection mechanisms against such errors.

The proposers also intend to translate their theoretical designs into working prototypes. They intend to use their existing server and Web programming infrastructure to implement type systems and run-time checks
for CGI scripting (`a la Perl) and servlet programming (`a la Java). They will port some existing Web applications (including conference management, workshop registration) to this new software infrastructure and will thus test the practical validity of their efforts. Consequently, they expect to improve the quality of an increasingly critical medium of communication and commerce.

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.

ABSTRACT
0447509
Shriram Krishnamurthi
Brown University

CAREER: Formal Verification of Aspect-Oriented Software

Module systems have grown significantly in scope and sophistication. The most recent innovations have been in the space of so-called aspects, which provide modularity mechanisms that blur the line between static and dynamic composition. The creation of innovative module mechanisms gives programmers new powers, but in turn also makes it possible for them to introduce ever more subtle errors into software. This potential for new kinds of errors places a greater burden on verification techniques. These techniques have, however,
failed to keep pace with advances in software modularity.

This proposal will advance the state of research in computer-aided verification for the forms of modularity introduced by aspects. It will generate new theories of modular verification that address the different styles of aspect modularities. This work is, therefore, an instance of a larger research program that seeks synergies in the confluence of software engineering, programming languages and computer-aided verification.

The proposal will also have significant broader impact. It will lead to tools that will benefit the software development community. It will generate a new design for programming languages courses. Finally, it will produce a course designed to teach computing to students of the social sciences.

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.

Computers are becoming essential in all disciplines. Researchers in the social sciences rely on the availability of large data repositories and the general availability of data over the Web. Researchers in the humanities are increasingly looking to analyze the growing number of electronic corpora. Workers in all fields are making use of new ways to publish data and of to interact with colleagues and others using electronic media. Moreover, more and more jobs and companies are relying on the understanding and processing of information. Modern companies as diverse as Google, WalMart, Amazon, and Goldman Sachs all owe their success in large part to their ability to evaluate and act on available information. It is estimated that in the next ten years, over twelve million people in the U.S. workforce will consider programming their primary job, which is far more than the current or near-term number of computer science majors. To address these needs, to better prepare students for careers involving information processing, to prepare
tomorrow?s researchers in the humanities and social sciences, and to prepare tomorrow?s workers for an information-based world, computer science needs to reach out beyond its traditional audience and even beyond the sciences. This project focuses on disciplines that have traditionally
been neglected by computer scientists, harnessing the growing revolution in applying computing to social artifacts. Second, it will result in a novel, application-driven, on-demand presentation of computing material, coming to topics like machine-learning and data-mining very early, rather than late, in the curriculum. Third, the development of a curriculum arranged in concentric rings of growing commitment, where a student who stops early will still get a meaningful education. It will provide the proper foundation for the growing use of computing and cyberinfrastructure in the humanities and social sciences. It will ultimately train such students have been relegated to with the tools to make their own non-trivial contributions to cyberinfrastructure. It will result in more women and minorities, groups traditionally underrepresented in computing, working with and using computation and cyberinfrastructure. Finally, it will enable students to wed their deep social and humanistic insights to tools that can enable them to build wonderful inventions that have the power to greatly enrich society.

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.

The growth of the Internet means everyone from system administrators to casual users are regularly confronted with making decisions on how to share data. Research suggests that even experts struggle to make these decisions accurately using current access-control mechanisms. As users start to share information across social and professional applications, usable access-control mechanisms that help prevent such semantic errors are all the more urgent. This project develops an interactive authoring paradigm that helps users identify and clarify policy inconsistencies before they turn into semantic errors. The envisioned tools examine policies and their consequences during authoring, alert users to potential inconsistencies (such as isolated documents shared more globally than most others), and ask questions in order to eliminate ambiguities.

The challenge in building such proactive authoring tools lies in knowing what inconsistencies and issues to track without overwhelming a user with too much interaction. The proposal therefore combines user studies with tool building and evaluation. The intellectual merit of this project lies in its marriage of research on user behavior and logical tools to produce a new paradigm of policy authoring. Broader impacts come from building tools for mainstream end-users, guided by ethnographic studies of social-network users. For further information see the project web site at the URL: http://www.margrave-tool.org/

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.

Modern Web browsers provide a "private browsing" mode, wherein the browser does not record the user's behavior such as which sites they visited. This mode is valuable to users of all stripes, from the privacy-conscious to those those worried about persecution by totalitarian regimes. Browser implementers therefore take great care to try to ensure these modes function correctly. However, modern browsers are highly extensible: users can install extensions to customize their browser, and millions have done so. Unfortunately, it is technically challenging for browsers to automatically flag which extensions are privacy-preserving and which are not, so browsers currently do not attempt to offer such guidance -- leaving users to fend for themselves.

This work presents a type system for verifying whether extensions violate private browsing mode. The types distinguish Safe values (that may always be used in private mode) from Unsafe ones (that may lead to privacy violations). The type system is engineered to be
"lightweight": extensions that never perform unsafe actions should type check without changes, and extension authors must only annotate their extension code when an unsafe action is used. Extensions that pass this check are accompanied by a guarantee that they do not perform privacy-violating actions, and are thus safe to install in private-browsing mode.

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.

Computer networks use switches, routers, and other devices to process and forward traffic. In a traditional network, these devices coordinate to agree on how traffic should be forwarded. Software-defined networks (SDN) replace this distributed control with a logically centralized controller program which dictates forwarding behavior to each device by installing rules which can include instructions to send certain traffic to the controller for processing or notification. Incorrect rules can lead to the controller missing vital notifications, giving it an incorrect view of the network's state and potentially harming network functionality. On the other hand, if traffic is sent to the controller needlessly, performance can suffer.

This project is developing Flowlog, a tierless SDN programming language. A tierless language unifies the disparate layers of programming for SDNs: the controller program itself, switch forwarding rules, and the controller's internal state. Flowlog safely handles rule-management on the switches automatically, without any intervention from the programmer. This not only simplifies development, but also prevents the above bugs that can arise from manual rule-installation. Finally, Flowlog programs can interact with arbitrary other programs, even those not written in Flowlog. Since a failure in a controller program can compromise the entire network, program reliability is of central importance. Thus, Flowlog is designed to enable automatic reasoning about programs, and the project is building in support for program verification (both for a specific network and in general), differential analysis, fault-tolerance testing, and even automated repair of errant programs.

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 a project to create a flexible, language agnostic software library that makes text and block programming tools accessible to visually-impaired users. Screen-readers, the most common affordable tool for presenting text to those who can't read it directly, have difficulties presenting source code which is symbol-heavy and navigated best not as a list of words, but as an abstract syntax tree (AST). This project will produce a collection of JavaScript libraries that annotate source code with structural descriptions suitable for presentation by screen readers.

JavaScript was chosen because web-based environments address common technical and logistical challenges in schools. They place fewer demands on IT staff for installation and maintenance, and enable students to work outside of school without manually transferring files. Web-based software is also easier to upgrade and evolve on the developer's end. Being the lingua-franca for cloud-based UIs, the browser's Document Object Model (DOM) is currently receiving significant attention when it comes to accessibility and thus, by using the DOM to display our IDE, we can leverage these investments now and in the future. The libraries created in this project will be used to make two web-based environments--WeScheme and code.pyret.org--accessible, and those environments will be used in conducting usability testing with visually-impaired users.

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.

Software reliability is increasingly vital in modern life. The power grid, the cars we drive, our hospitals, and even our food production rely heavily on software to function. The risk of errors can be mitigated by tools, called model finders, that produce concrete examples to help software developers understand their system. However, most such tools suffer from the principle that you get precisely what you ask for, but sometimes not what you really want or need. This project works to improve the effectiveness of model-finding tools, both by increasing their explanatory power and improving presentation of examples. The tools developed in the project will be applicable to a wide range of users and domains, including formal-methods education.

This project explores a unique melding of model-search and proof-search that has henceforth been unexplored. The contributions of this project include: (1) well defined notions of "Must this be here?" and "Why is this here?" for model finding in first-order logic with transitive closure, along with algorithms for answering these questions; (2) novel approaches to navigating between models and selecting which models to present, based on the concept of coverage from other formal methods sub-fields; and (3) extensions to the widely-used Alloy Analyzer that realize these ideas and make them available to the community.

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.

Programming is a rigorous and intellectually demanding activity. Programmers are expected to provide instructions to a black box device, whose behavior is very different from their own, to accomplish complex tasks. Even seasoned professionals can find this challenging, and beginners often struggle to do it. These problems are greatly amplified when a program has errors or produces incorrect output. A major obstacle is for the programmer to understand how the computer works at a level that is useful for expressing their needs and correcting their programs. The intellectual merits are to evaluate existing models of programming systems, and to define new ones that enable programmers to better understand the computer's execution. The project's broader significance and importance are to make effective programming more accessible to a much broader range of people, including those who intend to apply computing in other data-intensive domains.

Concretely, the research examines the use of programming language semantics as explanatory tools for non-technical users. Existing semantics provide rich explanations of behavior, but are expressed in highly technical terms that require significant expertise to understand and use. Furthermore, they have not been tested through application to actual debugging tasks. Therefore, this work intends to open up investigation into the human factors aspects of programming language semantics, understanding how well they perform in different settings, and potentially defining new semantics forms that are better suited to a broad range of programmers. The work will specifically focus on functional programming with an eye towards its role in data science curricula, which are of value across a broad spectrum of disciplines.

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.

Security and design flaws in artificial intelligence (AI) algorithms and computer systems can leave our personal information, including sensitive data such as medical records, dangerously exposed, or can give rise to biases that disadvantage or threaten parts of the population. The ability to successfully find these security and design flaws before they cause harm depends on qualified engineers, researchers, and policymakers who understand threats to computer systems and algorithms. However, threat-modeling is typically taught only in advanced Computer Science courses, which come late in the curriculum and which not all students elect to take. This project investigates whether earlier and continued exposure to material on threat modeling and a mindset called "adversarial thinking" improves students' ability to recognize and address challenges in privacy, cybersecurity, and new AI technologies. Adversarial thinking refers to adopting the perspective of an adversary who seeks to exploit weaknesses in a system, algorithm, or model. The resulting course materials and findings will be disseminated, and the findings are expected to motivate changes in the approach to computer science curricula.

The project proposes to develop material on adversarial thinking and integrate it into courses at the introductory, intermediate, and advanced level of Brown University?s computer science curriculum. The project team will measure students' performance and progression within each course as well as across courses. The data collected will help answer the project?s central research question: do students who encounter adversarial thinking early in and repeatedly throughout their computer science education show improved ability to recognize and address threats and flaws in computer systems security and AI models? The project will impact academic computer science education through pedagogical methods, skills, and recommendations for curricular structures that help prepare students for the complexities, risks, and opportunities of new technologies.

This project is supported by a special initiative of the Secure and Trustworthy Cyberspace (SaTC) program to foster new, previously unexplored, collaborations between the fields of cybersecurity, artificial intelligence, and education. The SaTC program aligns with the Federal Cybersecurity Research and Development Strategic Plan and the National Privacy Research Strategy to protect and preserve the growing social and economic benefits of cyber systems while ensuring security and privacy.

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.

In computer science, formal methods refer to mathematical approaches to make predictions about a software or hardware system. Formal methods play an increasingly vital role in developing secure and reliable systems. However, formal methods tend to be abstract and use methods and notations that are not part of many computing curricula. As a result, there is a need to research and develop approaches to effectively train cybersecurity students to use formal methods. The current proposal focuses on creating pedagogical tools centered around programming environments. The approach will be evaluated across a broad population, from college students to industrial programmers, to ensure the results will be as broadly applicable as possible. In addition, all products will be made freely available to other educators.

The primary objective of this project is to have subjects engage with formal methods tools to create, explore, reason about, and verify models. The focus will be on models related to security, such as cryptographic protocols, configuration, authentication, and access control. The project team proposes creating a series of graduated levels of formal languages to match a learning progression and reduce the learning load. This approach will enable students to use domain-specific notations to adopt formal methods within the context of domains they already study. Finally, it will enable students to create domain-specific custom visualizations that greatly reduce the cognitive gap between the output of a generic tool and the problems students want to solve. All these topics will be studied experimentally and evaluated to learn about what approaches are effective and what are not.

This project is supported by the Secure and Trustworthy Cyberspace (SaTC) program, which funds proposals that address cybersecurity and privacy, and in this case specifically cybersecurity education. The SaTC program aligns with the Federal Cybersecurity Research and Development Strategic Plan and the National Privacy Research Strategy to protect and preserve the growing social and economic benefits of cyber systems while ensuring security and privacy.

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.