Developers routinely use GenAI tools (large language models enriched in various ways) to generate useful components of programs, such as regular expressions. While pleasant and often effective, this can easily lead to subtle bugs. The developer may have been unclear in their specification, they may not fully understand the language of the output, there may be systematic misconceptions suffered by the user and perhaps even embedded in the language model, and so on. Responsible use of GenAI requires humans in the loop. To be effective, the human interaction must be both meaningful and moderate. We accomplish this as follows. First, we generate multiple candidate expressions instead of one. We then use formal language containment properties to generate distinguishing concrete scenarios that illustrate the differences between the candidates. We then have users rate these concrete scenarios. This process converges in a few steps, while also giving the user insight into any lack of clarity on their part. We have built a tool, pick, that implements this iterative process. We apply it to three formal languages with the necessary properties: regexes, linear temporal logic, and access-control policies. We show through experiments that pick is a significant improvement over showing users the candidate expressions, and also helps catch situations where no output is a match.

Problem planning is a fundamental programming skill, and aids students in decomposing tasks into manageable subtasks. While feedback on plans is beneficial for beginners, providing this in a scalable and timely way is an enormous challenge in large courses.

students to learn in order to succeed in an increasingly data-driven world. Foundational data literacy skills currently live in a number of subjects across K-12 (e.g., data collection and analysis in science classes, statistical calculations in mathematics/statistics, data visualization and communication in civics/social studies), however, a growing number of schools and districts are introducing stand-alone data science (DS) courses. Given the centrality of computing and programming in the contemporary practice of DS, many of these courses include topics historically reserved for computer science (CS) classes. Further, many CS courses include dedicated time for DS topics (e.g., AP Computer Science Principles' unit on Data). In many ways, DS educators and CS educators are working towards the same ends in complementary ways. However, at other times, the two disciplines are in tension, especially given the scarcity of time in K-12 student schedules for non-core subjects. This panel will explore what DS education and CS education can learn from each other, how each can contribute and advance the goals of the other, and how these two intertwined disciplines can productively live alongside each other in K-12 settings.

Program planning is the process of splitting a problem description into subtasks that can be solved independently, then composed into a solution. While much has been written about planning since the 1980s, little research looks at modern contexts such as programs to process data tables. Tool support for this sort of planning is even rarer. As part of a project to develop such tools, we have run two studies to try to identify steps, representations, and interactions that would support novice university students in planning and programming multi-task programs that process data tables. This experience report describes our observations so far, while also raising questions about how to make planning useful for students.

Myriad projects and efforts are underway to infuse more content on ethical and socially-responsible computing into Computer Science curricula. Talks and papers on these projects largely focus on case studies and examples that can be included in assignments. This paper instead takes a pedagogic perspective. Drawing on papers on ethics-based design from multiple computing disciplines, as well as frameworks for identifying security threats, we designed a framework for identifying a variety of social threats in the kinds of programs that university students develop in their first two years of study. The framework is unique in centering around architectural components of applications, rather than stakeholders and values.

When novice programming students already know one programming language and have to learn another, what issues do they run into? We specifically focus on one or both languages being functional, varying along two axes: syntax and semantics. We report on problems, especially persistent ones. This work can be of immediate value to educators and also sets up avenues for future research.

Many efforts are underway to have computing curricula prepare students to anticipate adverse social impacts of computing. Much of the attention currently focuses on introductory CS courses and machine learning courses, often framed around bias that arises around algorithmic decision-making systems. The presenters on this panel have instead focused on ways to weave responsible-computing content into data structures and introductory algorithms courses. They have done so at different levels, ranging from second-semester introductory courses (so-called CS2) up through upper-undergraduate or early graduate courses. Each panelist will describe their perspective on how responsible computing fits into their course and present an illustrative assignment or lecture from their course. The goal of the session is to inspire other CS faculty to work similar content into corresponding courses at their own institutions, while also fostering a community of practice for responsible computing in core CS courses beyond machine learning.

We propose that secondary-school data-science curricula should be based on four key ingredients: two are technical (programming and statistics, with visualization sitting at their intersection), while two are human-facing (meaningful domains, and civic responsibility). We describe their relationship and argue for their importance.

Model-finders, such as SAT/SMT-solvers and Alloy, are used widely both directly and embedded in domain-specific tools. They support both conventional verification and, unlike other verification tools, property-free exploration. To do this effectively, they must produce output that helps users with these tasks. Unfortunately, the output of model-finders has seen relatively little rigorous human-factors study. Conventionally, these tools tend to show one satisfying instance at a time. Drawing inspiration from the cognitive science literature, we investigate two aspects of model-finder output: how many instances to show at once, and whether all instances must actually satisfy the input constraints. Using both controlled studies and open-ended talk-alouds, we show that there is benefit to showing negative instances in certain settings; the impact of multiple instances is less clear. Our work is a first step in a theoretically grounded approach to understanding how users engage cognitively with model-finder output, and how those tools might better support users in doing so.

Motivation. Higher-order functions are a standard and increasingly central component in many kinds of modern programming, including data science and Web development. Yet little research has been devoted to student learning or understanding of this topic.

CS departments in the USA have used various models for teaching about ethics, including standalone ethics courses and expert-designed assignments. At Brown University, we are trying a different approach: a group of undergraduate teaching assistants dedicated to socially-responsible practices in computing work with faculty to integrate content into multiple assignments both across a course and across the curriculum. This "responsible computing" initiative has resulted in a variety of assignments added to 13 different courses in the past year. This paper describes the program's design, sample assignments, results of an internal evaluation, and refinements we are making to the model. We contrast our model to others from the literature in hopes of expanding the collection of curricular ideas for designing education in responsible computing.

Integrating computing into other subjects promises to address many challenges to offering standalone CS courses in K-12 contexts. Integrated curricula must be designed carefully, however, to both meet learning objectives of the host discipline and to gain traction with teachers. We describe the multi-year evolution of Bootstrap, a curriculum for integrating computing into middle- and high-school mathematics. We discuss the initial design and the various modifications we have made over the years to better support math instruction, leading to our goal of using integrated curricula to cover standards in both math and CS. We provide advice for others aiming for integration and raise questions for CS educators about how we might better support learning in other disciplines.

SIGCSE is packed with teaching insights and inspiration. However, we get these insights and inspiration from hearing our colleagues talk about their teaching. Why not just watch them teach? This session does exactly that. Six exceptional educators will present their favorite piece of innovative lecture content just as they would to their students. The moderator, Colleen Lewis, will describe the central pedagogical move within the innovation and how this connects to education research. The goal of the session is to inspire SIGCSE attendees by highlighting innovative instruction by exceptional educators. The specific content of the innovative instruction may be applicable for some attendees, and the discussion of the underlying pedagogical move within each innovation can be applied across the attendees' teaching.

Data that correspond to real-world scenarios can often be organized in several different ways in a database or program. Appreciating the differences between them and choosing an organization that addresses a system's needs are valuable and necessary computing skills. Unfortunately, little of the computing-education literature seems to deal with this topic.

Cognitive theories of how programmers produce code suggest that novices' approaches are primarily driven by the retrieval of previously-learned plans. These plans can be high-level, focusing on task decomposition and composition, or low-level, focusing on code implementations. These theories, however, do not describe how novices move between high-level tasks and low-level code, especially when faced with novel problems. Understanding these transitions can help concretely tease out why and where novices struggle and how they use their knowledge of plans and design techniques when they get stuck. We studied this by conducting think-alouds with CS1 students at two universities as they solved multi-task programming problems with unfamiliar components. Our analysis paid particular attention to a series of design techniques that the students had been explicitly taught in their respective courses. We identified patterns of high- and low-level thinking that relate to students' success on the problems, and propose a concrete framework of high- and low-level work that summarizes the transitions that we observed.

Policymakers believe that preparing all students from the earliest grades to high school for a new future of STEM+Computing (STEM+C) integration involves teaching them not only the science and math central to these areas, but also how computational thinking is integral to STEM disciplines. This panel brings together four researchers who focus on research and development of interdisciplinary approaches to the integration of computing within STEM teaching and learning for preK-12 students. They will share the most impactful, practical, and promising approaches to STEM+C integration, their pros and cons, challenges, and key insights to successful STEM+C integration at all grade levels.

The 32 chapters of the 2019 Cambridge Handbook of Computing Education Research synthesize the existing research in computing education and propose new directions for future research. An author from each chapter will summarize their chapter with auto-advancing slides. Attendees will be introduced to the breadth of content in the new handbook and can identify chapters of interest. This fits uniquely as a special session, and will likely be informative, inspiring, and overwhelming.

Prior studies suggest that novice programmers approach problems by retrieving previously-learned plans. These plans can be high-level (encompassing decomposition and composition of tasks) or low-level (focused mainly on code). What happens when novices face programming problems that compose tasks in new ways or that involve tasks they haven't seen before? How do they move between high-level tasks and low-level code? What does this suggest about how to teach programming?

In many universities, Teaching Assistants (TAs) are an important part of students' educational experience. This is especially true in early courses, where students may suffer from inexperience and anxiety, and find fellow students more accessible than professors.

Generating questions to engage and measure students is often challenging and time-consuming. Furthermore, these questions do not always transfer well between student populations due to differences in background, course emphasis, or ambiguity in the questions or answers. We introduce a contributing student pedagogy activity facilitated by machine learning that can generate questions with associated answer-reasoning sets. We call this process Adaptive Tool-Driven Conception Generation. A tool implementing this process has been deployed, and it explicitly optimizes the process for questions that divide student opinion. In a study involving arrays in Java, this novel process: generates questions similar to expert-designed questions, produces novel questions that identify potential student misconceptions, and provides statistical estimates of the prevalence of misconceptions. This process allows the generation of quiz and discussion questions with less expert effort, facilitates a subprocess in the creation of concept inventories, and also raises the possibility of running reproduction studies relatively cheaply.

Instructors routinely use automated assessment methods to evaluate the semantic qualities of student implementations and, sometimes, test suites. In this work, we distill a variety of automated assessment methods in the literature down to a pair of assessment models. We identify pathological assessment outcomes in each model that point to underlying methodological flaws. These theoretical flaws broadly threaten the validity of the techniques, and we actually observe them in multiple assignments of an introductory programming course. We propose adjustments that remedy these flaws and then demonstrate, on these same assignments, that our interventions improve the accuracy of assessment. We believe that with these adjustments, instructors can greatly improve the accuracy of automated assessment.

Data Science is at the center of many current curricular efforts. It is emerging as an integrated field that has far-reaching and important applications, from news media to policy making to business. While these applications can provide compelling uses of computer science techniques, an introduction to one is not an introduction to the other. How do topics like data structures and program design emerge from data science applications? How do we transition from data science applications to computer science topics? How can data science be integrated into other contexts with little overhead? This workshop presents assignments and curricula designed to answer these questions, and tools that support them.

Bootstrap:Algebra is a curricular module designed to integrate introductory computing into an algebra class; the module aims to help students improve on various essential learning outcomes from state and national algebra standards. In prior work, we published initial findings about student performance gains on algebra problems after taking Bootstrap. While the results were promising, the dataset was not large, and had students working on algebra problems that had been scaffolded with Bootstrap's pedagogy. This paper reports on a more detailed study with (a) data from more than three times as many students, (b) analysis of performance changes in incorrect answers, (c) some problems in which the Bootstrap scaffolds have been removed, and (d) an IRT analysis across the elements of Bootstrap's program-design pedagogy. Our results confirm that students improve on algebraic word problems after completing the module, even on unscaffolded problems. The nature of incorrect answers to symbolic-form questions also appears to improve after Bootstrap.

Game programming projects are concrete and motivational for students, especially when used to teach more abstract concepts such as algebra. These projects must have open-ended elements to allow for creativity, but too much freedom makes it hard to reach specific learning outcomes. How many degrees of freedom do students need to make a game feel like one they genuinely designed? What kinds of personalization do they undertake of their games? And how do these factors correlate with their prior game-playing experience or with their identified gender? This paper studies these questions in the concrete setting of the Bootstrap:Algebra curriculum. In this curriculum, students are only given four parameters they can customize and only a few minutes in which to do so. Our study shows that despite this very limited personalization, students still feel a strong sense of ownership, originality, and pride in their creations. We also find that females find videogame creation just as satisfying as males, which contradicts some prior research but may also reflect the nature of games created in this curriculum and the opportunities it offers for self-expression.

We evaluate a notional machine for recursion based on algebraic substitution. To do this, we decompose recursion into a progression of function call patterns, parameter name reuse, and data structure complexity. At each stage, we test students' ability to trace programs using substitution. We evaluate the correctness of their traces along multiple dimensions, finding that students generally do well, and also observe shortcuts and identify misconceptions. For comparison, we also have students trace two problems using a traditional, imperative notional machine. Even though the substitution model is unwieldy to use with compound data, students still perform better with it than with the traditional notional machine.

When functional programming is used in studies of the Rainfall problem in CS1, most students seem to perform fairly well. A handful of students, however, still struggle, though with different surface-level errors than those reported for students programming imperatively. Prior research suggests that novice programmers tackle problems by refining a high-level program schema that they have seen for a similar problem. Functional-programming students, however, have often seen multiple schemas that would apply to Rainfall. How do novices navigate these choices? This paper presents results from a talk-aloud study in which novice functional programmers worked on Rainfall. We describe the criteria that drove students to select, and sometimes switch, their high-level program schema, as well as points where students realized that their chosen schema was not working. Our main contribution lies in our observations of how novice programmers approach a multi-task planning problem in the face of multiple viable schemas.

Scope, aliasing, mutation, and parameter passing are fundamental programming concepts that interact in subtle ways, especially in complex programs. Research has shown that students have substantial misconceptions on these topics. But this research has been done largely in CS1 courses, when students' programming experience is limited and problems are necessarily simple. What happens later in the curriculum? Does more programming experience iron out these misconceptions naturally, or are interventions required?

When students are faced with a programming problem unlike any they have solved before, prior research suggests that they develop code backwards from essential computations in the problem. Some curricula, however, teach students to first write scaffolding code based on the type of the input data. How do these two approaches interact? We gave CS1 students who were taught to write scaffolding code a programming problem unlike any they had seen before. We found that while students put essential computations into the scaffolds, they often overuse affordances of the scaffolds in ways that lead to plan-composition errors. We propose that steering students away from on-the-fly decomposition while programming could help avoid some of these errors.

Plan composition is an important but under-studied topic in programming education. Most studies were done three decades ago, under assumptions that miss important issues that today's students must confront. This paper presents rationale and details for a modernized study of plan composition that accommodates a broader range of programming languages and problem features. Our study design has two novelties: the problems require students to deal with data-processing challenges (such as noisy data), and the questions ask students to not only produce but also evaluate programs. We present preliminary results from using our study in multiple courses from different linguistic paradigms. We discuss several future studies that are prompted by these results.

In in-flow peer review, students provide feedback to one another on intermediate artifacts on their way to a final submission. Prior work has studied examples and tests as a potentially useful initial artifact for review. Unfortunately, large test suites are onerous to produce and especially to review. We instead propose the notion of a sweep, an artificially constrained set of tests that illustrates common and interesting behavior. We present experimental data across several courses that show that sweeps have reasonable quality, and are also a good target for peer review; for example, students usually (over half the time) suggest new tests to one another in a review.

Bootstrap teaches students to create their own videogames using a programming approach that directly reinforces state and national algebra standards. Used in classrooms across the country, Bootstrap is proving successful at transferring skills from programming to algebra word problems in 8th and 9th grade students. Due to the algebraic foundation for both content and pedagogy, math teachers with limited programming experience find the curriculum highly approachable; many offer it as a module within an algebra course. Bootstrap is a prefix to a higher-level computer science curriculum called Program by Design that emphasizes data-driven design and testing (with or without the videogame focus). In this BOF, current and potential users of these curricula will discuss the connections between introductory computing education and algebra education, share best practices for teaching and moving beyond these curricula, and generate ideas for future evolution of both curricula. The two facilitators will adapt the format as needed to support the interests of the participants.

Many educators have tried to leverage computing or programming to help improve students' achievement in mathematics. However, several hopes of performance gains---particularly in algebra---have come up short. In part, these efforts fail to align the computing and mathematical concepts at the level of detail typically required to achieve transfer of learning. This paper describes Bootstrap, an early-programming curriculum that is designed to teach key algebra topics as students build their own videogames. We discuss the curriculum, explain how it aligns with algebra, and present initial data showing student performance gains on standard algebra problems after completing Bootstrap.

Many studies have used Soloway's Rainfall problem to explore plan composition and programming errors by novice programmers. Few of these have explored students from CS1 courses that use functional programming. The concepts and programming styles commonly taught in such courses give CS1 students more viable plan-composition options than in traditional imperative CS1 courses. Using data from five functional-language CS1 courses at four schools, we show that our students choose different high-level structures and make fewer low-level errors compared to results of other Rainfall studies. We discuss the potential role of language in these results and raise various questions that could further explore these effects.

Test-first development and peer review have been studied independently in computing courses, but their combination has not. We report on an experiment in which students in two courses conducted peer review of test suites while assignments were in progress. We find strong correlation between review ratings and staff-assessed work quality, as well as evidence that test suites improved during the review process. Student feedback suggests that reviewing had some causal impact on these improvements. We describe several lessons learned about administering and assessing peer-review within test-first development.

Peer review is effective for teaching students to evaluate approaches to problems, fostering collaboration, and assessing other students' work. Peer review often happens after assignments are turned in, on complete artifacts that other students have created. We've been experimenting with a different style of peer review, which we call in-flow reviewing, in which programming assignments are broken into reviewable stages. After students complete each stage they review one anothers' work, allowing for feedback early on in the assignment. We've built a system, dubbed Captain Teach, for exploring in-flow reviewing for both programming and written assignments. In our demonstration and tutorial, we will show what the student experience looks like for a Captain Teach assignment, explain the interface that instructors have for creating assignments in Captain Teach, outline some of the mechanisms for anonymously assigning reviews and distributing feedback, and discuss future directions for the tool.

Computing educators have used peer review in various ways in courses at many levels. Few of these efforts have applied peer review to multiple deliverables (such as specifications, tests, and code) within the same programming problem, or to assignments that are still in progress (as opposed to completed). This paper describes CaptainTeach, a programming environment enhanced with peer-review capabilities at multiple stages within assignments in progress. Multi-stage, in-flow peer review raises many logistical and pedagogical issues. This paper describes CaptainTeach and our experience using it in two undergraduate courses (one first-year and one upper-level); our analysis emphasizes issues that arise from the conjunction of multiple stages and in-flow reviewing, rather than peer review in general.

Scenario-finding tools such as Alloy are widely used to understand the consequences of specifications, with applications to software modeling, security analysis, and verification. This paper focuses on the exploration of scenarios: which scenarios are presented first, and how to traverse them in a well-defined way. We present Aluminum, a modification of Alloy that presents only minimal scenarios: those that contain no more than is necessary. Aluminum lets users explore the scenario space by adding to scenarios and backtracking. It also provides the ability to find what can consistently be used to extend each scenario. We describe the semantic basis of Aluminum in terms of minimal models of first-order logic formulas. We show how this theory can be implemented atop existing SAT-solvers and quantify both the benefits of minimality and its small computational overhead. Finally, we offer some qualitative observations about scenario exploration in Aluminum.

We present the Program by Design introductory CS curriculum through the lenses of graphics, animations, algebra, and data structures. Animations programming is popular for CS1, but many such curricula lack clean paths into CS2. Program by Design is different. Using and reinforcing concepts from algebra, students learn to write animations (including standard topics such as model/view separation and event-handling), then move seamlessly into working with structured data, lists, trees, and objects. The curriculum emphasizes design, testing, and writing maintainable programs, without losing the engagement of animations. The workshop uses lectures and hands-on exercises to provide high- school and college teachers an overview of the approach. See www.programbydesign.org. Laptop Optional.

We posit that functional programmers employ a notion called expression integrity to understand programs. We attempt to study the extent to which both novices and experts use this notion as they program, discuss the difficulties that arise in measuring this, and offer some observational findings.

We present a programming environment called WeScheme that runs in the Web browser and supports interactive development. WeScheme programmers can save programs directly on the Web, making them accessible from everywhere. As a result, sharing of programs is a central focus that WeScheme supports seamlessly. The environment also leverages the existing presentation media and program run-time support found in Web browsers, thus making these easily accessible to students and leveraging their rapid engineering improvements. WeScheme is being used successfully by students, and is especially valuable in schools that have prohibitions on installing new software or lack the computational demands of more intensive programming environments.

Good error messages are critical for novice programmers. Re-cognizing this, the DrRacket programming environment provides a series of pedagogically-inspired language subsets with error messages customized to each subset. We apply human-factors research methods to explore the effectiveness of these messages. Unlike existing work in this area, we study messages at a fine-grained level by analyzing the edits students make in response to various classes of errors. We present a rubric (which is not language specific) to evaluate student responses, apply it to a course-worth of student lab work, and describe what we have learned about using the rubric effectively. We also discuss some concrete observations on the effectiveness of these messages.

Policy authors typically reconcile several different mental models and goals, such as enabling collaboration, securing information, and conveying trust in colleagues. The data underlying these models, such as which roles are more trusted than others, isn't generally used to define policy rules. As a result, policy-management environments don't gather this information; in turn, they fail to exploit it to help users check policy decisions against their multiple perspectives. We present a model of triangulating authoring environments that capture the data underlying these different perspectives, and iteratively sanity-check policy decisions against this information while editing. We also present a tool that consumes instances of the model and automatically generates prototype authoring tools for the described domain.

Abstract Many computer science departments are debating the role of programming languages in the curriculum. These discussions often question the relevance and appeal of programming-languages content for today's students. In our experience, domain-specific, “little languages” projects provide a compelling illustration of the importance of programming-language concepts. This paper describes projects that prototype mainstream applications such as PowerPoint, TurboTax, and animation scripting. We have used these exercises as modules in non-programming languages courses, including courses for first year students. Such modules both encourage students to study linguistic topics in more depth and provide linguistic perspective to students who might not otherwise be exposed to the area.

No abstract available.

Alloy specifications are used to define lightweight models of systems. We present Alchemy, which compiles Alloy specifications into implementations that execute against persistent databases. Alchemy translates a subset of Alloy predicates into imperative update operations, and it converts facts into database integrity constraints that it maintains automatically in the face of these imperative actions.

Bus and interconnect protocols contain a few core operations (such as read and write transfers) whose behaviors interleave to form complex executions. Specifications of the core operations should be flexible enough that simple composition operators suffice for capturing most interleavings, even in the presence of common hardware issues such as glitches. Oliveira and Hu proposed a form of pipelined regular expressions to specify atomic protocol compositions, but they abstracted away clocking and glitches. This paper uses the AMBA-2 specification to argue that a loosely-synchronized form of regular expressions handles such timing subtleties while retaining the simplicity of Oliveira and Hu's pipelined compositions.

Programs are increasingly organized around features, which are encapsulated using aspects and other linguistic mechanisms. Despite their growing popularity amongst developers, there is a dearth of techniques for computer-aided verification of programs that employ these mechanisms. We present the theoretical underpinnings for applying model checking to programs (expressed as state machines) written using these mechanisms. The analysis is incremental, examining only components that change rather than verifying the entire system every time one part of it changes. Our technique assumes that the set of pointcut designators is known statically, but the actual advice can vary. It handles both static and dynamic pointcut designators. We present the algorithm, prove it sound, and address several subtleties that arise, including cascading advice application and problems of circular reasoning.

This roadmap describes ways that researchers in four areas---specification languages, program generation, correctness by construction, and programming languages---might help further the goal of verified software. It also describes what advances the "verified software" grand challenge might anticipate or demand from work in these areas. That is, the roadmap is intended to help foster collaboration between the grand challenge and these research areas.A common goal for research in these areas is to establish language designs and tool architectures that would allow multiple annotations and tools to be used on a single program. In the long term, researchers could try to unify these annotations and integrate such tools.

Sensitive data are increasingly available on-line through the Web and other distributed protocols. This heightens the need to carefully control access to data. Control means not only preventing the leakage of data but also permitting access to necessary information. Indeed, the same datum is often treated differently depending on context.System designers create policies to express conditions on the access to data. To reduce source clutter and improve maintenance, developers increasingly use domain-specific, declarative languages to express these policies. In turn, administrators need to analyze policies relative to properties, and to understand the effect of policy changes even in the absence of properties.This paper presents Margrave, a software suite for analyzing role-based access-control policies. Margrave includes a verifier that analyzes policies written in the XACML language, translating them into a form of decision-diagram to answer queries. It also provides semantic differencing information between versions of policies. We have implemented these techniques and applied them to policies from a working software application.

Aspect-oriented programming has become an increasingly important means of expressing cross-cutting program abstractions. Despite this, aspects lack support for computer-aided verification. We present a technique for verifying aspect-oriented programs (expressed as state machines). Our technique assumes that the set of pointcut designators is known statically, but that the actual advice can vary. This calls for a modular technique that does not require repeated analysis of the entire system every time a developer changes advice. We present such an analysis, addressing several subtleties that arise. We also present an important optimization for handling multiple pointcut designators. We have implemented a prototype verifier and applied it to some simple but interesting cases.

Feature-oriented programming organizes programs around features rather than objects, thus better supporting extensible, product-line architectures. Programming languages increasingly support this style of programming, but programmers get little support from verification tools. Ideally, programmers should be able to verify features independently of each other and use automated compositional reasoning techniques to infer properties of a system from properties of its features. Achieving this requires carefully designed interfaces: they must hold sufficient information to enable compositional verification, yet tools should be able to generate this information automatically because experience indicates programmers cannot or will not provide it manually. We present a model of interfaces that supports automated, compositional, feature-oriented model checking. To demonstrate their utility, we automatically detect the feature-interaction problems originally found manually by R. Hall in an email suite case study.

Feature-oriented software designs capture many interesting notions of cross-cutting, and offer a powerful method for building product-line architectures. Each cross-cutting feature is an independent module that fundamentally yields an open system from a verification perspective. We describe desiderata for verifying such modules through model checking and find that existing work on the verification of open systems fails to address most of the concerns that arise from feature-oriented systems. We therefore provide a new methodology for verifying such systems. To validate this new methodology, we have implemented it and applied it to a suite of modules that exhibit feature interaction problems. Our model checker was able to automatically locate ten problems previously found through a laborious simulation-based effort.

Most existing modular model checking techniques betray their hardware roots: they assume that modules compose in parallel. In contrast, collaboration-based software designs, which have proven very successful in several domains, are sequential in the simplest case. Most interesting collaboration-based designs are really quasi-sequential compositions of parallel compositions. These designs demand and inspire new verification techniques. This paper presents algorithms that exploit the software's modular decomposition to verify collaboration-based designs. Our technique can verify most properties locally in the collaborations; we also characterize when a global state space construction is unavoidable. We have validated our proposal by testing it on several designs.