VLDB 2026 Research / reviewers in the wild / expert
Westley Weimer
dblp:05/4127
· DBLP profile ↗
115ranked-venue papers
9as first author
27since 2021 · last 2025
0000-0001-6749-2204ORCID · verified
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 86 · 9 first-author · 18 since 2021Systems, architecture and hardware · 13 · 2 since 2021Artificial intelligence and machine learning · 11 · 1 first-author · 3 since 2021Security and privacy · 9 · 3 since 2021Graphics, computer vision, multimedia, augmented reality and games · 3Human-computer interaction and ubiquitous computing · 3 · 2 since 2021Computer networks · 2Theory of computation · 1
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | Automatically Mitigating Vulnerabilities in Binary Programs via Partially Recompilable DecompilationabstractVulnerabilities are challenging to locate and repair, especially when source code is unavailable and binary patching is required. Manual methods are time-consuming, require significant expertise, and do not scale to the rate at which new vulnerabilities are discovered. Automated methods are an attractive alternative, and we propose Partially Recompilable Decompilation (PRD) to help automate the process. PRD lifts suspect binary functions to source, available for analysis, revision, or review, and creates a patched binary using source- and binary-level techniques. Although decompilation and recompilation do not typically succeed on an entire binary, our approach does because it is limited to a few functions, such as those identified by our binary fault localization. We evaluate the assumptions underlying our approach and find that, without any grammar or compilation restrictions, up to 79% of individual functions are successfully decompiled and recompiled. In comparison, only 1.7% of the full C-binaries succeed. When recompilation succeeds, PRD produces test-equivalent binaries 93.0% of the time. We evaluate PRD in two contexts: a fully automated process incorporating source-level Automated Program Repair (APR) methods; and human-edited source-level repairs. When evaluated on DARPA Cyber Grand Challenge (CGC) binaries, we find that PRD-enabled APR tools, operating only on binaries, perform as well as, and sometimes better than full-source tools, collectively mitigating 85 of the 148 scenarios, a success rate consistent with the same tools operating with access to the entire source code. PRD achieves similar success rates as the winning CGC entries, sometimes finding higher-quality mitigations than those produced by top CGC teams. For generality, the evaluation includes two independently developed APR tools andC++, Rode0day, and real-world binaries. Pemma Reiter, Hui Jun Tay, Westley Weimer, Adam Doupé, Ruoyu Wang 0001, Stephanie Forrest |
IEEE Trans. Dependable Secur. Comput. | 3 |
| 2025 | The Evolution of Automated Software RepairabstractGenProg implemented a novel method for automatically evolving patches to repair test suite failures in legacy C programs. It combined insights from genetic programming and software engineering. Many of the original design decisions in GenProg were ultimately less important than its impact as an existence proof. In particular, it demonstrated that useful patches for non-trivial bugs and programs could be generated automatically. Since the original publication, research in automated program repair has expanded to consider and evaluate many new methods, contexts and defects. As code synthesis and debugging techniques based on machine learning have become popular, it is informative to consider how views on perennial issues in program repair have changed, or remained static, over time. This retrospective discusses the issues of repair quality (including the role of tests), use cases for automated repairs (including the role of humans), and why these approaches work at all. Claire Le Goues, ThanhVu Nguyen, Stephanie Forrest, Westley Weimer |
IEEE Trans. Software Eng. | 4 |
| 2024 | Causal Relationships and Programming Outcomes: A Transcranial Magnetic Stimulation ExperimentabstractUnderstanding the relationship between cognition and programming outcomes is important: it can inform interventions that help novices become experts faster. Neuroimaging techniques can measure brain activity, but prior studies of programming report only correlations. We present the first causal neurological investigation of the cognition of programming by using Transcranial Magnetic Stimulation (TMS). TMS permits temporary and noninvasive disruption of specific brain regions. By disrupting brain regions and then measuring programming outcomes, we discover whether a true causal relationship exists. To the best of our knowledge, this is the first use of TMS to study software engineering. Hammad Ahmad, Madeline Endres, Kaia Newman, Priscila Santiesteban, Emma Shedden, Westley Weimer |
ICSE | 6 |
| 2024 | High Expectations: An Observational Study of Programming and Cannabis IntoxicationabstractAnecdotal evidence of cannabis use by professional programmers abounds. Recent studies have found that some professionals regularly use cannabis while programming, even for work-related tasks. However, accounts of the impacts of cannabis on programming vary widely and are often contradictory. For example, some programmers claim that it impairs their ability to generate correct solutions, while others claim it enhances creativity and focus. There remains a need for an empirical understanding of the true impacts of cannabis on programming. This paper presents the first controlled observational study of cannabis's effects on programming ability. Based on a within-subjects design with over 70 participants, we find that, at ecologically valid dosages, cannabis significantly impairs programming performance. Programs implemented while high contain more bugs and take longer to write (p < 0.05) --- a small to medium effect (0.22 ≤ d ≤ 0.44). We also did not find any evidence that high programmers generate more divergent solutions. However, programmers can accurately assess differences in their programming performance (r = 0.59), even when under the influence of cannabis. We hope that this research will facilitate evidence-based policies and help developers make informed decisions regarding cannabis use while programming. Wenxin He, Manasvi Parikh, Westley Weimer, Madeline Endres |
ICSE | 3 |
| 2024 | Reducing Malware Analysis Overhead With CoveringsabstractThere is a substantial and growing body of malware samples that evade automated analysis and detection tools. Malware may measure fingerprints (“artifacts”) of the underlying analysis tool or environment, and change their behavior when such artifacts are detected. While analysis tools can mitigate artifacts to reduce exposure, such concealment is expensive and limits scalable automated malware analysis. However, not every sample checks for every type of artifact—analysis efficiency can be improved by mitigating only those artifacts most likely to be used by a sample. Using that insight, we proposeMimosa, a system that identifies a small set of “covering” configurations that collectively and efficiently defeat most malware samples in a corpus.Mimosaidentifies a set of configurations that maximize analysis throughput and detection accuracy while minimizing manual effort, enabling scalable automation for analyzing stealthy malware. We evaluate our approach against a benchmark of 1535 meticulously labeled stealthy malware samples. We further test our approach on an additional set of 1221 stealthy malware samples and successfully analyze nearly 99% of them using only 2 VM backends.Mimosaprovides a practical, tunable method for efficiently deploying malware analysis resources. Michael Sandborn, Zach Stoebner, Westley Weimer, Stephanie Forrest, Ryan E. Dougherty, Jules White, Kevin Leach |
IEEE Trans. Dependable Secur. Comput. | 3 |
| 2024 | Towards a Cognitive Model of Dynamic Debugging: Does Identifier Construction Matter?abstractDebugging is a vital and time-consuming process in software engineering. Recently, researchers have begun using neuroimaging to understand the cognitive bases of programming tasks by measuring patterns of neural activity. While exciting, prior studies have only examined small sub-steps in isolation, such as comprehending a method without writing any code or writing a method from scratch without reading any already-existing code. We propose a simple multi-stage debugging model in which programmers transition between Task Comprehension, Fault Localization, Code Editing, Compiling, and Output Comprehension activities. We conduct a human study of$n=28$participants using a combination of functional near-infrared spectroscopy and standard coding measurements (e.g., time taken, tests passed, etc.). Critically, we find that our proposed debugging stages are both neurally and behaviorally distinct. To the best of our knowledge, this is the first neurally-justified cognitive model of debugging. At the same time, there is significant interest in understanding how programmers from different backgrounds, such as those grappling with challenges in English prose comprehension, are impacted by code features when debugging. We use our cognitive model of debugging to investigate the role of one such feature: identifier construction. Specifically, we investigate how features of identifier construction impact neural activity while debugging by participants with and without reading difficulties. While we find significant differences in cognitive load as a function of morphology and expertise, we do not find significant differences in end-to-end programming outcomes (e.g., time, correctness, etc.). This nuanced result suggests that prior findings on the cognitive importance of identifier naming in isolated sub-steps may not generalize to end-to-end debugging. Finally, in a result relevant to broadening participation in computing, we find no behavioral outcome differences for participants with reading difficulties. Danniell Hu, Priscila Santiesteban, Madeline Endres, Westley Weimer |
IEEE Trans. Software Eng. | 4 |
| 2024 | A Controlled Experiment in Age and Gender Bias When Reading Technical Articles in Software EngineeringabstractOnline platforms and communities are a critical part of modern software engineering, yet are often affected by human biases. While previous studies investigated human biases and their potential harms against the efficiency and fairness of online communities, they have mainly focused on the open source andQ & Aplatforms, such asGitHubandStack Overflow, but overlooked the audience-focused online platforms for delivering programming and SE-related technical articles, where millions of software engineering practitioners share, seek for, and learn from high-quality software engineering articles (i.e.,technical articlesfor SE). Furthermore, most of the previous work has revealed gender and race bias, but we have little knowledge about the effect of age on software engineering practice. In this paper, we propose to investigate the effect of authors’ demographic information (gender and age) on the evaluation of technical articles on software engineering and potential behavioral differences among participants. We conducted a survey-based and controlled human study and collected responses from 540 participants to investigate developers’ evaluation of technical articles for software engineering. By controlling the gender and age of the author profiles of technical articles for SE, we found that raters tend to have more positive content depth evaluations for younger male authors when compared to older male authors and that male participants conduct technical article evaluations faster than female participants, consistent with prior study findings. Surprisingly, different from other software engineering evaluation activities (e.g., code review, pull request, etc.), we did not find a significant difference in the genders of authors on the evaluation outcome of technical articles in SE. Anda Liang, Emerson R. Murphy-Hill, Westley Weimer, Yu Huang 0015 |
IEEE Trans. Software Eng. | 3 |
| 2023 | How Do We Read Formal Claims? Eye-Tracking and the Cognition of Proofs about AlgorithmsabstractFormal methods are used successfully in high-assurance software, but they require rigorous mathematical and logical training that practitioners often lack. As such, integrating formal methods into software has been associated with numerous challenges. While educators have placed emphasis on formalisms in undergraduate theory courses, such courses often struggle with poor student outcomes and satisfaction. In this paper, we present a controlled eye-tracking human study (n = 34) investigating the problem-solving strategies employed by students with different levels of incoming preparation (as assessed by theory coursework taken and pre-screening performance on a proof comprehension task), and how educators can better prepare low-outcome students for the rigorous logical reasoning that is a core part of formal methods in software engineering. Surprisingly, we find that incoming preparation is not a good predictor of student outcomes for formalism comprehension tasks, and that student self-reports are not accurate at identifying factors associated with high outcomes for such tasks. Instead, and importantly, we find that differences in outcomes can be attributed to performance for proofs by induction and recursive algorithms, and that better-performing students exhibit significantly more attention switching behaviors, a result that has several implications for pedagogy in terms of the design of teaching materials. Our results suggest the need for a substantial pedagogical intervention in core theory courses to better align student outcomes with the objectives of mastery and retaining the material, and thus bettering preparing students for high-assurance software engineering. Hammad Ahmad, Zachary Karas, Kimberly Diaz, Amir Kamil, Jean-Baptiste Jeannin, Westley Weimer |
ICSE | 6 |
| 2023 | From Organizations to Individuals: Psychoactive Substance Use By Professional ProgrammersabstractPsychoactive substances, which influence the brain to alter perceptions and moods, have the potential to have positive and negative effects on critical software engineering tasks. They are widely used in software, but that use is not well understood. We present the results of the first qualitative investigation of the experiences of, and challenges faced by, psychoactive substance users in professional software communities. We conduct a the-matic analysis of hour-long interviews with 26 professional pro-grammers who use psychoactive substances at work. Our results provide insight into individual motivations and impacts, including mental health and the relationships between various substances and productivity. Our findings elaborate on socialization effects, including soft skills, stigma, and remote work. The analysis also highlights implications for organizational policy, including positive and negative impacts on recruitment and retention. By exploring individual usage motivations, social and cultural ramifications, and organizational policy, we demonstrate how substance use can permeate all levels of software development. Kaia Newman, Madeline Endres, Westley Weimer, Brittany Johnson |
ICSE | 3 |
| 2023 | A Four-Year Study of Student Contributions to OSS vs. OSS4SG with a Lightweight InterventionabstractModern software engineering practice and training increasingly rely on Open Source Software (OSS). The recent growth in demand for professional software engineers has led to increased contributions to, and usage of, OSS. However, there is limited understanding of the factors affecting how developers, and how new or student developers in particular, decide which OSS projects to contribute to, a process critical to OSS sustainability, access, adoption, and growth. To better understand OSS contributions from the developers of tomorrow, we conducted a four-year study with 1,361 students investigating the life cycle of their contributions (from project selection to pull request acceptance). During the study, we also delivered a lightweight intervention to promote the awareness of open source projects for social good (OSS4SG), OSS projects that have positive impacts in other domains. Using both quantitative and qualitative methods, we analyze student experience reports and the pull requests they submit. Compared to general OSS projects, we find significant differences in project selection (𝑝 < 0.0001, effect size = 0.84), student motivation (𝑝 < 0.01, effect size = 0.13), and increased pull-request acceptance rates for OSS4SG contributions. We also find that our intervention correlates with increased student contributions to OSS4SG (𝑝 < 0.0001, effect size = 0.38). Finally, we analyze correlations of factors such as gender or working with a partner. Our findings may help improve the experience for new developers participating in OSS4SG and the quality of their contributions. We also hope our work helps educators, project leaders, and contributors to build a mutually-beneficial framework for the future growth of OSS4SG. Zihan Fang 0001, Madeline Endres, Thomas Zimmermann 0001, Denae Ford, Westley Weimer, Kevin Leach, Yu Huang 0015 |
ESEC/SIGSOFT FSE | 5 |
| 2023 | Evolving Software: Combining Online Learning with Mutation-Based Stochastic SearchabstractEvolutionary algorithms and related mutation-based methods have been used in software engineering, with recent emphasis on the problem of repairing bugs. In this work, programs are typically not synthesized from a random start. Instead, existing solutions—which may be flawed or inefficient—are taken as starting points, with the evolutionary process searching for useful improvements. This approach, however, introduces a challenge for the search algorithm: what is the optimal number of neutral mutations that should be combined? Too much is likely to introduce errors and break the program while too little hampers the search process, inducing the classic tradeoff between exploration and exploitation. In the context of software improvement, this work considers MWRepair, an algorithm for enhancing mutation-based searches, which uses online learning to optimize the tradeoff between exploration and exploitation. The aggressiveness parameter governs how many individual mutations should be applied simultaneously to an individual between fitness evaluations. MWRepair is evaluated in the context of automated program repair problems, where the goal is repairing software bugs with minimal human involvement. The article analyzes the search space for automated program repair induced by neutral mutations, finding that the greatest probability of finding successful repairs often occurs when many neutral mutations are applied to the original program. Moreover, repair probability follows a characteristic, unimodal distribution. MWRepair uses online learning to leverage this property, finding both rare and multi-edit repairs to defects in the popular Defects4J benchmark set of buggy Java programs. Joseph Renzullo, Westley Weimer, Stephanie Forrest |
ACM Trans. Evol. Learn. Optim. | 2 |
| 2023 | CirFix: Automated Hardware Repair and its Real-World ApplicationsabstractThis article presents CirFix, a framework for automatically repairing defects in hardware designs implemented in languages like Verilog. We propose a novel fault localization approach based on assignments to wires and registers, and a fitness function tailored to the hardware domain to bridge the gap between software-level automated program repair and hardware descriptions. We also present a benchmark suite of 32 defect scenarios corresponding to a variety of hardware projects. Overall, CirFix produces plausible repairs for 21/32 and correct repairs for 16/32 of the defect scenarios. Additionally, we evaluate CirFix's fault localization independently through a human study (n = 41), and find that the approach may be a beneficial debugging aid for complex multi-line hardware defects. Priscila Santiesteban, Yu Huang 0015, Westley Weimer, Hammad Ahmad |
IEEE Trans. Software Eng. | 3 |
| 2022 | CirFix: automatically repairing defects in hardware design codeabstractThis paper presents CirFix, a framework for automatically repairing defects in hardware designs implemented in languages like Verilog. We propose a novel fault localization approach based on assignments to wires and registers, and a fitness function tailored to the hardware domain to bridge the gap between software-level automated program repair and hardware descriptions. We also present a benchmark suite of 32 defect scenarios corresponding to a variety of hardware projects. Overall, CirFix produces plausible repairs for 21/32 and correct repairs for 16/32 of the defect scenarios. This repair rate is comparable to that of successful program repair approaches for software, indicating CirFix is effective at bringing over the benefits of automated program repair to the hardware domain for the first time. Hammad Ahmad, Yu Huang 0015, Westley Weimer |
ASPLOS | 3 |
| 2022 | Improving source-code representations to enhance search-based software repairabstractAutomatically improving and repairing software using search-based methods is an active research topic. Many current systems use existing source code as the ingredients of repairs, either through evolutionary computation derived random mutation or other heuristic operators. However, these code transformation operators are not always well-matched to the granularity of the source code on which they operate. This paper proposes a static source-to-source preprocessing step to produce code with more uniform granularity that exposes relevant program components to the repair process. This approach, called Program Repair Enhancement via Preprocessing (PREP), has been applied to three different repair tools, each of which uses different code transformation operators and search algorithms. In every case, applying PREP before the search allows the tool to repair software defects that were previously unattainable by that tool. PREP finds 88 unique previously-unreported correct repairs across these tools. This result is significant because it is applicable to most search-based software improvement methods, and it addresses the fundamental issue of how to match the granularity of the representation to the granularity of operators. Pemma Reiter, Antonio M. Espinoza, Adam Doupé, Ruoyu Wang 0001, Westley Weimer, Stephanie Forrest |
GECCO | 5 |
| 2022 | Hashing It Out: A Survey of Programmers' Cannabis Usage, Perception, and MotivationabstractCannabis is one of the most common mind-altering substances. It is used both medicinally and recreationally and is enmeshed in a complex and changing legal landscape. Anecdotal evidence suggests that some software developers may use cannabis to aid some programming tasks. At the same time, anti-drug policies and tests remain common in many software engineering environments, sometimes leading to hiring shortages for certain jobs. Despite these connections, little is actually known about the prevalence of, and motivation for, cannabis use while programming. In this paper, we report the results of the first large-scale survey of cannabis use by programmers. We report findings about 803 developers' (including 450 full-time programmers') cannabis usage prevalence, perceptions, and motivations. For example, we find that some programmers do regularly use cannabis while programming: 35% of our sample has tried programming while using cannabis, and 18% currently do so at least once a month. Furthermore, this cannabis usage is primarily motivated by a perceived enhancement to certain software development skills (such as brainstorming or getting into a programming zone) rather than medicinal reasons (such as pain relief). Finally, we find that cannabis use while programming occurs at similar rates for programming employees, managers, and students despite differences in cannabis perceptions and visibility. Our results have implications for programming job drug policies and motivate future research into cannabis use while programming. Madeline Endres, Kevin Boehnke, Westley Weimer |
ICSE | 3 |
| 2022 | START: A Framework for Trusted and Resilient Autonomous Vehicles (Practical Experience Report)abstractFrom delivering groceries and vital medical supplies to driving trucks and passenger vehicles, society is becoming increasingly reliant on autonomous vehicles (AVs), It is therefore vital that these systems be resilient to adversarial actions, perform mission-critical functions despite known and unknown vulnerabilities, and protect and repair themselves during or after operational failures and cyber-attacks. While techniques have been proposed to address individual aspects of software resilience, vulnerability assessment, automated repair, and invariant detection, there is no approach that provides end-to-end trusted and resilient mission operation and repair on AVs. In this paper, we describe our experience of building START,11Software Techniques for Automated Resilience and Trust a framework that provides increased resilience, accurate vul-nerability assessment, and trustworthy post-repair operation in autonomous vehicles. We combine techniques from binary analysis and rewriting, runtime monitoring and verification, auto-mated program repair, and invariant detection that cooperatively detect and eliminate a swath of software security vulnerabilities in cyberphysical systems. We evaluate our framework using an autonomous vehicle simulation platform, demonstrating its holistic applicability to AVs. Kevin Leach, Christopher Steven Timperley, Kevin Angstadt, Anh Nguyen-Tuong, Jason Hiser, Aaron Paulos, Partha P. Pal, Patrick Hurley, Carl Thomas, Jack W. Davidson, Stephanie Forrest, Claire Le Goues, Westley Weimer |
ISSRE | 13 |
| 2022 | Digging into Semantics: Where Do Search-Based Software Repair Methods Search?
Hammad Ahmad, Padraic Cashin, Stephanie Forrest, Westley Weimer |
PPSN (2) | 4 |
| 2022 | Seq2Parse: neurosymbolic parse error repairabstractWe present Seq2Parse, a language-agnostic neurosymbolic approach to automatically repairing parse errors. Seq2Parse is based on the insight that Symbolic Error Correcting (EC) Parsers can, in principle, synthesize repairs, but, in practice, are overwhelmed by the many error-correction rules that are not relevant to the particular program that requires repair. In contrast, Neural approaches are fooled by the large space of possible sequence level edits, but can precisely pinpoint the set of EC-rules that are relevant to a particular program. We show how to combine their complementary strengths by using neural methods to train a sequence classifier that predicts the small set of relevant EC-rules for an ill-parsed program, after which, the symbolic EC-parsing algorithm can make short work of generating useful repairs. We train and evaluate our method on a dataset of 1,100,000 Python programs, and show that Seq2Parse is accurate and efficient : it can parse 94% of our tests within 2.1 seconds, while generating the exact user fix in 1 out 3 of the cases; and useful : humans perceive both Seq2Parse-generated error locations and repairs to be almost as good as human-generated ones in a statistically-significant manner. Georgios Sakkas, Madeline Endres, Philip J. Guo, Westley Weimer, Ranjit Jhala |
Proc. ACM Program. Lang. | 4 |
| 2022 | Eyes on Code: A Study on Developers' Code Navigation StrategiesabstractWhat code navigation strategies do developers use and what mechanisms do they employ to find relevant information? Do their strategies evolve over the course of longer tasks? Answers to these questions can provide insight to educators and software tool designers to support a wide variety of programmers as they tackle increasingly-complex software systems. However, little research to date has measured developers’ code navigation strategies in ecologically-valid settings, or analyzed how strategies progressed throughout a maintenance task. We propose a novel experimental design that more accurately represents the software maintenance process in terms of software complexity and IDE interactions. Using this framework, we conduct an eye-tracking study (n=36) of realistic bug-fixing tasks, dynamically and empirically identifying relevant code areas. We introduce a three-phase model to characterize developers’ navigation behavior supported by statistical variations in eye movements over time. We also propose quantifiable notion of “thrashing” with the code as a navigation activity. We find that thrashing is associated with lower effectiveness. Our results confirm that the relevance of various code elements changes over time, and that our proposed three-phase model is capable of capturing these significant changes. We discuss our findings and their implications for tool designers, educators, and the research community. Zohreh Sharafi, Ian Bertram, Michael Flanagan, Westley Weimer |
IEEE Trans. Software Eng. | 4 |
| 2021 | Relating Reading, Visualization, and Coding for New Programmers: A Neuroimaging StudyabstractUnderstanding how novices reason about coding at a neurological level has implications for training the next generation of software engineers. In recent years, medical imaging has been increasingly employed to investigate patterns of neural activity associated with coding activity. However, such studies have focused on advanced undergraduates and professionals. In a human study of 31 participants, we use functional near-infrared spectroscopy to measure the neural activity associated with introductory programming. In a controlled, contrast-based experiment, we relate brain activity when coding to that of reading natural language or mentally rotating objects (a spatial visualization task). Our primary result is that all three tasks-coding, prose reading, and mental rotation-are mentally distinct for novices. However, while those tasks are neurally distinct, we find more significant differences between prose and coding than between mental rotation and coding. Intriguingly, we generally find more activation in areas of the brain associated with spatial ability and task difficulty for novice coding compared to that reported in studies with more expert developers. Finally, in an exploratory analysis, we also find a neural activation pattern predictive of programming performance 11 weeks later. While preliminary, these findings both expand on previous results (e.g., relating expertise to a similarity between coding and prose reading) and also provide a new understanding of the cognitive processes underlying novice programming. Madeline Endres, Zachary Karas, Xiao-Su Hu, Ioulia Kovelman, Westley Weimer |
ICSE | 5 |
| 2021 | Multiplicative Weights Algorithms for Parallel Automated Software RepairabstractMultiplicative Weights Update (MWU) algorithms are a form of online learning that is applied to multi-armed bandit problems. Such problems involve allocating a fixed number of trials among multiple options to maximize cumulative payoff. MWU is a popular and effective method for dynamically balancing the trade-off between exploring the value of new options and exploiting the information already gained. However, no clear strategy exists to help practitioners choose which of the several algorithmic designs within this family to deploy. In this paper, three variants of parallel MWU algorithms are considered: Two parallel variants that rely on global memory, and one variant that uses distributed memory. The three variants are first analyzed theoretically, and then their effectiveness is assessed empirically on the task of estimating distributions in the context of stochastic search for repairs to bugs in software. Earlier work on APR suffers from various inefficiencies, and the paper shows how to decompose the problem into two stages: one that is embarrassingly parallel and one that is amenable to MWU. We then model the cost of each MWU variant and derive the conditions under which it is likely to be preferred in practice. We find that all three MWU algorithms achieve accuracy above 90% but that there are significant differences in runtime and total cost. When 90% accuracy is sufficient and evaluating options is expensive, such as in our use case, we find that the algorithm that uses global memory and has high communication cost outperforms the other two. We analyze the reasons for this surprising result. Joseph Renzullo, Westley Weimer, Stephanie Forrest |
IPDPS | 2 |
| 2021 | The Early Bird Gets the Worm: Major Retention in CS3abstractEnrollments continue to rise in Computer Science courses, yet fostering inclusive climates and retaining diverse student bodies remain key challenges. Gender ratios remain heavily skewed and many demographics are severely underrepresented. Numerous studies investigate student retention in introductory courses, but few focus on later stages of the CS retention "pipeline", where techniques and findings from earlier courses may no longer apply. Fee Lia Christoph, Westley Weimer, Kevin Angstadt |
ITiCSE (1) | 2 |
| 2021 | An Analysis of Iterative and Recursive Problem PerformanceabstractIteration and recursion are fundamental programming constructs in introductory computer science. Understanding the relationship between contextual factors, such as problem formulation or student background, that relate to performance on iteration and recursion problems can help inform pedagogy. We present the results of a study of 162 undergraduate participants tasked with comprehending iterative, recursive, and tail-recursive versions of CS1 functions. First, we carry out a task-specific analysis, finding that students perform significantly better on the iterative framings of two problems with non-branching numerical computation and significantly better on the recursive framing of another that involves array classification (p < = 0.036). Second, we investigate differences in the most common student mistakes by program framing. We find that students were more likely to produce wrong answers with incorrect types or structures for recursive and tail-recursive program versions. Finally, we investigated correlations between programming performance and background factors including experience, gender, ethnicity, affluence, and spatial ability. We find that the factors relevant to explaining performance are similar for both iterative and recursive problems. While programming experience is the most significant factor, we find that spatial ability, gender, and ethnicity were more relevant for explaining performance than affluence. Madeline Endres, Westley Weimer, Amir Kamil |
SIGCSE | 2 |
| 2021 | To read or to rotate? comparing the effects of technical reading training and spatial skills training on novice programming abilityabstractUnderstanding how to best support and train novice programmers is a critical component of producing better and more diverse software engineers. In this paper, we present the results of a controlled 11-week longitudinal study with 57 CS1 students comparing two skill-based interventions to improve programming performance. The first intervention involves spatial training, an established baseline known to be helpful in engineering contexts. The second intervention is a novel CS-focused technical reading training. Madeline Endres, Madison Fansher, Priti Shah, Westley Weimer |
ESEC/SIGSOFT FSE | 4 |
| 2021 | Connecting the dots: rethinking the relationship between code and prose writing with functional connectivityabstractMedical imaging studies of software engineering have risen in popularity and may reveal the neural underpinnings of coding activities. To date, however, all studies in computer science venues have treated brain regions independently and in isolation. Since most complex neural activity involves coordination among multiple regions, previous analyses may overlook neural behavior. Zachary Karas, Andrew Jahn, Westley Weimer, Yu Huang 0015 |
ESEC/SIGSOFT FSE | 3 |
| 2021 | A Coprocessor-Based Introspection Framework Via Intel Management EngineabstractDuring the past decade, virtualization-based (e.g., virtual machine introspection) and hardware-assisted approaches (e.g., x86 SMM and ARM TrustZone) have been used to defend against low-level malware such as rootkits. However, these approaches either require a large Trusted Computing Base (TCB) or they must share CPU time with the operating system, disrupting normal execution. In this article, we propose an introspection framework called Nighthawk that transparently checks system integrity and monitor the runtime state of target system. Nighthawk leverages the Intel Management Engine (IME), a co-processor that runs in isolation from the main CPU. By using the IME, our approach has a minimal TCB and incurs negligible overhead on the host system on a suite of indicative benchmarks. We use Nighthawk to introspect the system software and firmware of a host system at runtime. The experimental results show that Nighthawk can detect real-world attacks against the OS, hypervisors, and System Management Mode while mitigating several classes of evasive attacks. Additionally, Nighthawk can monitor the runtime state of host system against the suspicious applications running in target machine. Lei Zhou 0023, Fengwei Zhang, Jidong Xiao, Kevin Leach, Westley Weimer, Xuhua Ding, Guojun Wang 0001 |
IEEE Trans. Dependable Secur. Comput. | 5 |
| 2021 | Toward an Objective Measure of Developers' Cognitive ActivitiesabstractUnderstanding how developers carry out different computer science activities with objective measures can help to improve productivity and guide the use and development of supporting tools in software engineering. In this article, we present two controlled experiments involving 112 students to explore multiple computing activities (code comprehension, code review, and data structure manipulations) using three different objective measures including neuroimaging (functional near-infrared spectroscopy (fNIRS) and functional magnetic resonance imaging (fMRI)) and eye tracking. By examining code review and prose review using fMRI, we find that the neural representations of programming languages vs. natural languages are distinct. We can classify which task a participant is undertaking based solely on brain activity, and those task distinctions are modulated by expertise. We leverage insights from the psychological notion of spatial ability to decode the neural representations of several fundamental data structures and their manipulations using fMRI, fNIRS, and eye tracking. We examine list, array, tree, and mental rotation tasks and find that data structure and spatial operations use the same focal regions of the brain but to different degrees: they are related but distinct neural tasks. We demonstrate best practices and describe the implication and tradeoffs between fMRI, fNIRS, eye tracking, and self-reporting for software engineering research. Zohreh Sharafi, Yu Huang 0015, Kevin Leach, Westley Weimer |
ACM Trans. Softw. Eng. Methodol. | 4 |
| 2020 | Accelerating Legacy String Kernels via Bounded Automata LearningabstractThe adoption of hardware accelerators, such as FPGAs, into general-purpose computation pipelines continues to rise, but programming models for these devices lag far behind their CPU counterparts. Legacy programs must often be rewritten at very low levels of abstraction, requiring intimate knowledge of the target accelerator architecture. While techniques such as high-level synthesis can help port some legacy software, many programs perform poorly without manual, architecture-specific optimization. Kevin Angstadt, Jean-Baptiste Jeannin, Westley Weimer |
ASPLOS | 3 |
| 2020 | KShot: Live Kernel Patching with SMM and SGXabstractLive kernel patching is an increasingly common trend in operating system distributions, enabling dynamic updates to include new features or to fix vulnerabilities without having to reboot the system. Patching the kernel at runtime lowers downtime and reduces the loss of useful state from running applications. However, existing kernel live patching techniques (1) rely on specific support from the target operating system, and (2) admit patch failures resulting from kernel faults. We present KSHOT, a kernel live patching mechanism based on x86 SMM and Intel SGX that focuses on patching Linux kernel security vulnerabilities. Our patching processes are protected by hardware-assisted Trusted Execution Environments. We demonstrate that our technique can successfully patch vulnerable kernel functions at the binary-level without support from the underlying OS and regardless of whether the kernel patching mechanism is compromised. We demonstrate the applicability of KSHOT by successfully patching 30 critical indicative kernel vulnerabilities. Lei Zhou 0023, Fengwei Zhang, Jinghui Liao, Zhenyu Ning, Jidong Xiao, Kevin Leach, Westley Weimer, Guojun Wang 0001 |
DSN | 7 |
| 2020 | Trustworthiness Perceptions in Code Review: An Eye-tracking StudyabstractBackground: Automated program repair and other bug-fixing approaches are gaining attention in the software engineering community. Automation shows promise in reducing bug fixing costs. However, many developers express reluctance about accepting machine-generated patches into their codebases. Ian Bertram, Jack Hong, Yu Huang 0015, Westley Weimer, Zohreh Sharafi |
ESEM | 4 |
| 2020 | Neurological divide: an fMRI study of prose and code writingabstractSoftware engineering involves writing new code or editing existing code. Recent efforts have investigated the neural processes associated with reading and comprehending code --- however, we lack a thorough understanding of the human cognitive processes underlying code writing. While prose reading and writing have been studied thoroughly, that same scrutiny has not been applied to code writing. In this paper, we leverage functional brain imaging to investigate neural representations of code writing in comparison to prose writing. We present the first human study in which participants wrote code and prose while undergoing a functional magnetic resonance imaging (fMRI) brain scan, making use of a full-sized fMRI-safe QWERTY keyboard. Ryan Krueger, Yu Huang 0015, Tyler Santander, Westley Weimer, Kevin Leach |
ICSE | 5 |
| 2020 | A Human Study of Comprehension and Code SummarizationabstractSoftware developers spend a great deal of time reading and understanding code that is poorly-documented, written by other developers, or developed using differing styles. During the past decade, researchers have investigated techniques for automatically documenting code to improve comprehensibility. In particular, recent advances in deep learning have led to sophisticated summary generation techniques that convert functions or methods to simple English strings that succinctly describe that code's behavior. However, automatic summarization techniques are assessed using internal metrics such as BLEU scores, which measure natural language properties in translational models, or ROUGE scores, which measure overlap with human-written text. Unfortunately, these metrics do not necessarily capture how machine-generated code summaries actually affect human comprehension or developer productivity. Sean Stapleton, Yashmeet Gambhir, Alexander LeClair, Zachary Eberhart, Westley Weimer, Kevin Leach, Yu Huang 0015 |
ICPC | 5 |
| 2020 | Type error feedback via analytic program repairabstractWe introduce Analytic Program Repair, a data-driven strategy for providing feedback for type-errors via repairs for the erroneous program. Our strategy is based on insight that similar errors have similar repairs. Thus, we show how to use a training dataset of pairs of ill-typed programs and their fixed versions to: (1) learn a collection of candidate repair templates by abstracting and partitioning the edits made in the training set into a representative set of templates; (2) predict the appropriate template from a given error, by training multi-class classifiers on the repair templates used in the training set; (3) synthesize a concrete repair from the template by enumerating and ranking correct (e.g. well-typed) terms matching the predicted template. We have implemented our approach in Rite: a type error reporting tool for OCaml programs. We present an evaluation of the accuracy and efficiency of Rite on a corpus of 4,500 ill-typed Ocaml programs drawn from two instances of an introductory programming course, and a user-study of the quality of the generated error messages that shows the locations and final repair quality to be better than the state-of-the-art tool in a statistically-significant manner. Georgios Sakkas, Madeline Endres, Benjamin Cosman, Westley Weimer, Ranjit Jhala |
PLDI | 4 |
| 2020 | PABLO: Helping Novices Debug Python Code Through Data-Driven Fault LocalizationabstractAs dynamically-typed languages grow in popularity, especially among beginning programmers, there is an increased need to pinpoint their defects. Localization for novice bugs can be ambiguous: not all locations formally implicated are equally useful for beginners. We propose a scalable fault localization approach for dynamic languages that is helpful for debugging and generalizes to handle a wide variety of errors commonly faced by novice programmers. We base our approach on a combination of static, dynamic, and contextual features, guided by machine learning. We evaluate on over 980,000 diverse real user interactions across four years from the popular PythonTutor.com website, which is used both in classes and by non-traditional learners. We find that our approach is scalable, general, and quite accurate: up to 77% of these historical novice users would have been helped by our top-three responses, compared to 45% for the default interpreter. We also conducted a human study: participants preferred our approach to the baseline ($p = 0.018)$, and found it additionally useful for bugs meriting multiple edits. Benjamin Cosman, Madeline Endres, Georgios Sakkas, Leon Medvinsky, Yao-Yuan Yang, Ranjit Jhala, Kamalika Chaudhuri, Westley Weimer |
SIGCSE | 8 |
| 2020 | Biases and differences in code review using medical imaging and eye-tracking: genders, humans, and machinesabstractCode review is a critical step in modern software quality assurance, yet it is vulnerable to human biases. Previous studies have clarified the extent of the problem, particularly regarding biases against the authors of code,but no consensus understanding has emerged. Advances in medical imaging are increasingly applied to software engineering, supporting grounded neurobiological explorations of computing activities, including the review, reading, and writing of source code. In this paper, we present the results of a controlled experiment using both medical imaging and also eye tracking to investigate the neurological correlates of biases and differences between genders of humans and machines (e.g., automated program repair tools) in code review. We find that men and women conduct code reviews differently, in ways that are measurable and supported by behavioral, eye-tracking and medical imaging data. We also find biases in how humans review code as a function of its apparent author, when controlling for code quality. In addition to advancing our fundamental understanding of how cognitive biases relate to the code review process, the results may inform subsequent training and tool design to reduce bias. Yu Huang 0015, Kevin Leach, Zohreh Sharafi, Nicholas McKay, Tyler Santander, Westley Weimer |
ESEC/SIGSOFT FSE | 6 |
| 2020 | The Surprising Creativity of Digital Evolution: A Collection of Anecdotes from the Evolutionary Computation and Artificial Life Research CommunitiesabstractEvolution provides a creative fount of complex and subtle adaptations that often surprise the scientists who discover them. However, the creativity of evolution is not limited to the natural world: Artificial organisms evolving in computational environments have also elicited surprise and wonder from the researchers studying them. The process of evolution is an algorithmic process that transcends the substrate in which it occurs. Indeed, many researchers in the field of digital evolution can provide examples of how their evolving algorithms and organisms have creatively subverted their expectations or intentions, exposed unrecognized bugs in their code, produced unexpectedly adaptations, or engaged in behaviors and outcomes, uncannily convergent with ones found in nature. Such stories routinely reveal surprise and creativity by evolution in these digital worlds, but they rarely fit into the standard scientific narrative. Instead they are often treated as mere obstacles to be overcome, rather than results that warrant study in their own right. Bugs are fixed, experiments are refocused, and one-off surprises are collapsed into a single data point. The stories themselves are traded among researchers through oral tradition, but that mode of information transmission is inefficient and prone to error and outright loss. Moreover, the fact that these stories tend to be shared only among practitioners means that many natural scientists do not realize how interesting and lifelike digital organisms are and how natural their evolution can be. To our knowledge, no collection of such anecdotes has been published before. This article is the crowd-sourced product of researchers in the fields of artificial life and evolutionary computation who have provided first-hand accounts of such cases. It thus serves as a written, fact-checked collection of scientifically important and even entertaining stories. In doing so we also present here substantial evidence that the existence and importance of evolutionary surprises extends beyond the natural world, and may indeed be a universal property of all complex evolving systems. Joel Lehman, Jeff Clune, Dusan Misevic, Christoph Adami, Lee Altenberg, Julie Beaulieu, Peter J. Bentley, Samuel Bernard, Guillaume Beslon, David M. Bryson, Nicholas Cheney, Patryk Chrabaszcz, Antoine Cully, Stéphane Doncieux, Fred C. Dyer, Kai Olav Ellefsen, Robert Feldt, Stephan Fischer 0002, Stephanie Forrest, Antoine Frénoy, Christian Gagné 0001, Leni K. Le Goff, Laura M. Grabowski, Babak Hodjat, Frank Hutter, Laurent Keller, Carole Knibbe, Peter Krcah, Richard E. Lenski, Hod Lipson, Robert MacCurdy, Carlos Maestre, Risto Miikkulainen, Sara Mitri, David E. Moriarty, Jean-Baptiste Mouret, Anh Totti Nguyen, Charles Ofria, Marc Parizeau, David P. Parsons, Robert T. Pennock, William F. Punch, Thomas S. Ray, Marc Schoenauer, Eric Schulte, Karl Sims, Kenneth O. Stanley, François Taddei, Danesh Tarapore, Simon Thibault, Richard A. Watson, Westley Weimer, Jason Yosinski |
Artif. Life | 52 |
| 2019 | Debugging Support for Pattern-Matching Languages and AcceleratorsabstractPrograms written for hardware accelerators can often be difficult to debug. Without adequate tool support, program maintenance tasks such as fault localization and debugging can be particularly challenging. In this work, we focus on supporting hardware that is specialized for finite automata processing, a computational paradigm that has accelerated pattern-matching applications across a diverse set of problem domains. While commodity hardware enables high-throughput data analysis, direct interactive debugging (e.g., single-stepping) is not currently supported. We propose a debugging approach for existing commodity hardware that supports step-through debugging and variable inspection of user-written automata processing programs. We focus on programs written in RAPID, a domain-specific language for pattern-matching applications. We develop a prototype of our approach for both Xilinx FPGAs and Micron's Automata Processor that supports simultaneous high-speed processing of data and interactive debugging without requiring modifications to the underlying hardware. Our empirical evaluation demonstrates low clock overheads for our approach across thirteen applications in the ANMLZoo automata processing benchmark suite on FPGAs. Additionally, we evaluate our technique through a human study involving over 60 participants and 20 buggy segments of code. Our generated debugging information increases fault localization accuracy by 22%, or 10 percentage points, in a statistically significant manner (p=0.013). Matthew Casias, Kevin Angstadt, Tommy Tracy II, Kevin Skadron, Westley Weimer |
ASPLOS | 5 |
| 2019 | Nighthawk: Transparent System Introspection from Ring -3
Lei Zhou 0023, Jidong Xiao, Kevin Leach, Westley Weimer, Fengwei Zhang, Guojun Wang 0001 |
ESORICS (2) | 4 |
| 2019 | Distilling neural representations of data structure manipulation using fMRI and fNIRSabstractData structures permeate many aspects of software engineering, but their associated human cognitive processes are not thoroughly understood. We leverage medical imaging and insights from the psychological notion of spatial ability to decode the neural representations of several fundamental data structures and their manipulations. In a human study involving 76 participants, we examine list, array, tree, and mental rotation tasks using both functional near-infrared spectroscopy (fNIRS) and functional magnetic resonance imaging (fMRI). We find a nuanced relationship: data structure and spatial operations use the same focal regions of the brain but to different degrees. They are related but distinct neural tasks. In addition, more difficult computer science problems induce higher cognitive load than do problems of pure spatial reasoning. Finally, while fNIRS is less expensive and more permissive, there are some computing-relevant brain regions that only fMRI can reach. Yu Huang 0015, Ryan Krueger, Tyler Santander, Xiao-Su Hu, Kevin Leach, Westley Weimer |
ICSE | 7 |
| 2019 | What goes on in your brain when you read and understand code?abstractSummary form only given, as follows. The complete presentation was not made available for publication as part of the conference proceedings. Within the last few years, high-resolution medical imaging technologies have grown in popularity for research in software engineering in general and program comprehension in particular. New approaches such function magnetic resonance imaging (fMRI) and functional near-infrared spectroscopy (fNIRS) complement more established approaches such as eye tracking and electroencephalograms (EEG), helping us to augment unreliable or subjective self-reporting with more objective measures of the neurobiological correlates of software engineering. This keynote summarizes recent exciting results using such techniques, from multiple authors, contrasting them to more traditional studies. We highlight the “game changing” areas of program comprehension that can be more rigorously targeted with these approaches (including expertise, efficiency, and problem difficulty, among others). We also lay out a number of the challenges associated with such studies (including experimental design, statistical analysis, regulatory compliance, reproducibility, and cost, among others). We conclude with a call to arms, surveying compelling ideas and experiments from psychology that have not yet been applied to program comprehension research. Westley Weimer |
ICPC | 1 |
| 2019 | Understanding Automatically-Generated Patches Through Symbolic Invariant DifferencesabstractDeveloper trust is a major barrier to the deployment of automatically-generated patches. Understanding the effect of a patch is a key element of that trust. We find that differences in sets of formal invariants characterize patch differences and that implication-based distances in invariant space characterize patch similarities. When one patch is similar to another it often contains the same changes as well as additional behavior; this pattern is well-captured by logical implication. We can measure differences using a theorem prover to verify implications between invariants implied by separate programs. Although effective, theorem provers are computationally intensive; we find that string distance is an efficient heuristic for implication-based distance measurements. We propose to use distances between patches to construct a hierarchy highlighting patch similarities. We evaluated this approach on over 300 patches and found that it correctly categorizes programs into semantically similar clusters. Clustering programs reduces human effort by reducing the number of semantically distinct patches that must be considered by over 50%, thus reducing the time required to establish trust in automatically generated repairs. Padraic Cashin, Carianne Martinez, Westley Weimer, Stephanie Forrest |
ASE | 3 |
| 2019 | InFix: Automatically Repairing Novice Program InputsabstractThis paper presents InFix, a technique for automatically fixing erroneous program inputs for novice programmers. Unlike comparable existing approaches for automatic debugging and maintenance tasks, InFix repairs input data rather than source code, does not require test cases, and does not require special annotations. Instead, we take advantage of patterns commonly used by novice programmers to automatically create helpful, high quality input repairs. InFix iteratively applies error-message based templates and random mutations based on insights about the debugging behavior of novices. This paper presents an implementation of InFix for Python. We evaluate on 29,995 unique scenarios with input-related errors collected from four years of data from Python Tutor, a free online programming tutoring environment. Our results generalize and scale; compared to previous work, we consider an order of magnitude more unique programs. Overall, InFix is able to repair 94.5% of deterministic input errors. We also present the results of a human study with 97 participants. Surprisingly, this simple approach produces high quality repairs; humans judged the output of InFix to be equally helpful and within 4% of the quality of human-generated repairs. Madeline Endres, Georgios Sakkas, Benjamin Cosman, Ranjit Jhala, Westley Weimer |
ASE | 5 |
| 2019 | Portable Programming with RAPIDabstractAs the hardware found within data centers becomes more heterogeneous, it is important to allow for efficient execution of algorithms across architectures. We present RAPID, a high-level programming language and combined imperative and declarative model for functionally- and performance-portable execution of sequential pattern-matching applications across CPUs, GPUs, Field-Programmable Gate Arrays (FPGAs), and Micron's D480 AP. RAPID is clear, maintainable, concise, and efficient both at compile and run time. Language features, such as code abstraction and parallel control structures, map well to pattern-matching problems, providing clarity and maintainability. For generation of efficient runtime code, we present algorithms to convert RAPID programs into finite automata. Our empirical evaluation of applications in the ANMLZoo benchmark suite demonstrates that the automata processing paradigm provides an abstraction that is portable across architectures. We evaluate RAPID programs against custom, baseline implementations previously demonstrated to be significantly accelerated. We also find that RAPID programs are much shorter in length, are expressible at a higher level of abstraction than their handcrafted counterparts, and yield generated code that is often more compact. Kevin Angstadt, Jack Wadden, Westley Weimer, Kevin Skadron |
IEEE Trans. Parallel Distributed Syst. | 3 |
| 2019 | Automatically Exploring Tradeoffs Between Software Output Fidelity and Energy CostsabstractData centers account for a significant fraction of global energy consumption and represent a growing business cost. Most current approaches to reducing energy use in data centers treat it as a hardware, compiler, or scheduling problem. This article focuses instead on the software level, showing how to reduce the energy used by programs when they execute. By combining insights from search-based software engineering, mutational robustness, profile-guided optimization, and approximate computing, the Producing Green Applications Using Genetic Exploration (PowerGAUGE) algorithm finds variants of individual programs that use less energy than the original. We apply hardware, software, and statistical techniques to manage the complexity of accurately assigning physical energy measurements to particular processes. In addition, our approach allows, but does not require, relaxing output quality requirements to achieve greater non-functional improvements. PowerGAUGE optimizations are validated using physical performance measurements. Experimental results on PARSEC benchmarks and two larger programs show average energy reductions of 14% when requiring the preservation of original output quality and 41% when allowing for human-acceptable levels of error. Jonathan Dorn, Jeremy Lacomis, Westley Weimer, Stephanie Forrest |
IEEE Trans. Software Eng. | 3 |
| 2018 | ASPEN: A Scalable In-SRAM Architecture for Pushdown AutomataabstractMany applications process some form of tree-structured or recursively-nested data, such as parsing XML or JSON web content as well as various data mining tasks. Typical CPU processing solutions are hindered by branch misprediction penalties while attempting to reconstruct nested structures and also by irregular memory access patterns. Recent work has demonstrated improved performance for many data processing applications through memory-centric automata processing engines. Unfortunately, these architectures do not support a computational model rich enough for tasks such as XML parsing. In this paper, we present ASPEN, a general-purpose, scalable, and reconfigurable memory-centric architecture for processing of tree-like data. We take inspiration from previous automata processing architectures, but support the richer deterministic pushdown automata computational model. We propose a custom datapath capable of performing the state matching, stack manipulation, and transition routing operations of pushdown automata, all efficiently stored and computed in memory arrays. Further, we present compilation algorithms for transforming large classes of existing grammars to pushdown automata executable on ASPEN, and demonstrate their effectiveness on four different languages: Cool (object oriented programming), DOT (graph visualization), JSON, and XML. Finally, we present an empirical evaluation of two application scenarios for ASPEN: XML parsing, and frequent subtree mining. The proposed architecture achieves an average 704.5 ns per KB parsing XML compared to 9983 ns per KB in a state-of-the-art XML parser across 23 benchmarks. We also demonstrate a 37.2x and 6x better end-to-end speedup over CPU and GPU implementations of subtree mining. Kevin Angstadt, Arun Subramaniyan 0001, Elaheh Sadredini, Reza Rahimi, Kevin Skadron, Westley Weimer, Reetuparna Das |
MICRO | 6 |
| 2018 | Dynamic witnesses for static type errors (or, Ill-Typed Programs Usually Go Wrong)abstractAbstract Static type errors are a common stumbling block for newcomers to typed functional languages. We present a dynamic approach to explaining type errors by generating counterexample witness inputs that illustrate how an ill-typed program goes wrong. First, given an ill-typed function, we symbolically execute the body to synthesize witness values that make the program go wrong. We prove that our procedure synthesizes general witnesses in that if a witness is found, then for all inhabited input types, there exist values that can make the function go wrong. Second, we show how to extend this procedure to produce a reduction graph that can be used to interactively visualize and debug witness executions. Third, we evaluate the coverage of our approach on two data sets comprising over 4,500 ill-typed student programs. Our technique is able to generate witnesses for around 85% of the programs, our reduction graph yields small counterexamples for over 80% of the witnesses, and a simple heuristic allows us to use witnesses to locate the source of type errors with around 70% accuracy. Finally, we evaluate whether our witnesses help students understand and fix type errors, and find that students presented with our witnesses show a greater understanding of type errors than those presented with a standard error message. Eric L. Seidel, Ranjit Jhala, Westley Weimer |
J. Funct. Program. | 3 |
| 2018 | Specialising Software for Different Downstream Applications Using Genetic Improvement and Code TransplantationabstractGenetic improvement uses automated search to find improved versions of existing software. Genetic improvement has previously been concerned with improving a system with respect to all possible usage scenarios. In this paper, we show how genetic improvement can also be used to achieve specialisation to a specific set of usage scenarios. We use genetic improvement to evolve faster versions of a C++ program, a Boolean satisfiability solver called MiniSAT, specialising it for three different applications, each with their own characteristics. Our specialised solvers achieve between 4 and 36 percent execution time improvement, which is commensurate with efficiency gains achievable using human expert optimisation for the general solver. We also use genetic improvement to evolve faster versions of an image processing tool called ImageMagick, utilising code from GraphicsMagick, another image processing tool which was forked from it. We specialise the format conversion functionality to greyscale images and colour images only. Our specialised versions achieve up to 3 percent execution time improvement. Justyna Petke, Mark Harman, William B. Langdon, Westley Weimer |
IEEE Trans. Software Eng. | 4 |
| 2017 | Decoding the representation of code in the brain: an fMRI study of code review and expertiseabstractSubjective judgments in software engineering tasks are of critical importance but can be difficult to study with conventional means. Medical imaging techniques hold the promise of relating cognition to physical activities and brain structures. In a controlled experiment involving 29 participants, we examine code comprehension, code review and prose review using functional magnetic resonance imaging. We find that the neural representations of programming languages vs. natural languages are distinct. We can classify which task a participant is undertaking based solely on brain activity (balanced accuracy 79%, p <; 0.001). Further, we find that the same set of brain regions distinguish between code and prose (near-perfect correlation, r = 0.99, p <; 0.001). Finally, we find that task distinctions are modulated by expertise, such that greater skill predicts a less differentiated neural representation (r = -0.44, p = 0.016) indicating that more skilled participants treat code and prose more similarly at a neural activation level. Benjamin Floyd, Tyler Santander, Westley Weimer |
ICSE | 3 |
| 2017 | Scotch: Combining Software Guard Extensions and System Management Mode to Monitor Cloud Resource Usage
Kevin Leach, Fengwei Zhang, Westley Weimer |
RAID | 3 |
| 2017 | Connecting Program Synthesis and Reachability: Automatic Program Repair Using Test-Input Generation
ThanhVu Nguyen, Westley Weimer, Deepak Kapur, Stephanie Forrest |
TACAS (1) | 2 |
| 2017 | Learning to blame: localizing novice type errors with data-driven diagnosisabstractLocalizing type errors is challenging in languages with global type inference, as the type checker must make assumptions about what the programmer intended to do. We introduce Nate, a data-driven approach to error localization based on supervised learning. Nate analyzes a large corpus of training data -- pairs of ill-typed programs and their "fixed" versions -- to automatically learn a model of where the error is most likely to be found. Given a new ill-typed program, Nate executes the model to generate a list of potential blame assignments ranked by likelihood. We evaluate Nate by comparing its precision to the state of the art on a set of over 5,000 ill-typed OCaml programs drawn from two instances of an introductory programming course. We show that when the top-ranked blame assignment is considered, Nate's data-driven model is able to correctly predict the exact sub-expression that should be changed 72% of the time, 28 points higher than OCaml and 16 points higher than the state-of-the-art SHErrLoc tool. Furthermore, Nate's accuracy surpasses 85% when we consider the top two locations and reaches 91% if we consider the top three. Eric L. Seidel, Huma Sibghat, Kamalika Chaudhuri, Westley Weimer, Ranjit Jhala |
Proc. ACM Program. Lang. | 4 |
| 2017 | Clarifications on the Construction and Use of the ManyBugs BenchmarkabstractAutomated repair techniques produce variant php interpreters, which should naturally serve as the tested interpreters. However, the answer to the question of what should serve as the testing interpreter is less obvious. php's default test harness configuration uses the same version of the interpreter for both the tested and testing interpreter. However, php may be configured via a command-line argument to use a different interpreter, such as the unmodified defective version, or a separate, manually-repaired version. Claire Le Goues, Yuriy Brun, Stephanie Forrest, Westley Weimer |
IEEE Trans. Software Eng. | 4 |
| 2016 | RAPID Programming of Pattern-Recognition ProcessorsabstractWe present RAPID, a high-level programming language and combined imperative and declarative model for programming pattern-recognition processors, such as Micron's Automata Processor (AP). The AP is a novel, non-Von Neumann architecture for direct execution of non-deterministic finite automata (NFAs), and has been demonstrated to provide substantial speedup for a variety of data-processing applications. RAPID is clear, maintainable, concise, and efficient both at compile and run time. Language features, such as code abstraction and parallel control structures, map well to pattern-matching problems, providing clarity and maintainability. For generation of efficient runtime code, we present algorithms to convert RAPID programs into finite automata. Further, we introduce a tessellation technique for configuring the AP, which significantly reduces compile time, increases programmer productivity, and improves maintainability. We evaluate five RAPID programs against custom, baseline implementations previously demonstrated to be significantly accelerated by the AP. We find that RAPID programs are much shorter in length, are expressible at a higher level of abstraction than their handcrafted counterparts, and yield generated code that is often more compact. In addition, our tessellation technique for configuring the AP has comparable device utilization to, and results in compilation that is up to four orders of magnitude faster than, current solutions. Kevin Angstadt, Westley Weimer, Kevin Skadron |
ASPLOS | 2 |
| 2016 | Dynamic witnesses for static type errors (or, ill-typed programs usually go wrong)abstractStatic type errors are a common stumbling block for newcomers to typed functional languages. We present a dynamic approach to explaining type errors by generating counterexample witness inputs that illustrate how an ill-typed program goes wrong. First, given an ill-typed function, we symbolically execute the body to synthesize witness values that make the program go wrong. We prove that our procedure synthesizes general witnesses in that if a witness is found, then for all inhabited input types, there exist values that can make the function go wrong. Second, we show how to extend the above procedure to produce a reduction graph that can be used to interactively visualize and debug witness executions. Third, we evaluate the coverage of our approach on two data sets comprising over 4,500 ill-typed student programs. Our technique is able to generate witnesses for 88% of the programs, and our reduction graph yields small counterexamples for 81% of the witnesses. Finally, we evaluate whether our witnesses help students understand and fix type errors, and find that students presented with our witnesses show a greater understanding of type errors than those presented with a standard error message. Eric L. Seidel, Ranjit Jhala, Westley Weimer |
ICFP | 3 |
| 2016 | Towards Transparent IntrospectionabstractThere is a growing need for the dynamic analysis of sensitive systems thatdo not support traditional debugging or emulation environments. Analysiscan alter program behavior, necessitating transparency. For example, asthe cat and mouse game between malware authors and malware analystsprogresses, malicious software can increasingly detect and confounddebuggers. Analysts must understand variable values, stack traces, andfactors influencing dynamic behavior, but recent malware samples leverageany piece of information or artifact available that signals the presence ofa debugger or emulator. In this work, we advance the state-of-the-art for transparent programanalysis by introducing a low-artifact introspection technique. Ourapproach uses hardware-assisted live memory snapshots ofprocess execution on native targets (e.g., x86 processors), coupledwith static reasoning about programs. We produce high-fidelity data and control flow information with minimaldetectable artifacts that could influence benign subject behavior or beleveraged for anti-analysis. We evaluate our system using two hardwareimplementations (x86-supported System Management Mode and PCI-basedSlotScreamer devices) and two software configurations (benign and evasiveprograms). We also analyze the theoretical and practical limitations of our technique. We discuss an expert case study in which we apply our technique to amalware reverse engineering task. Finally, we present results of a human study in which 30 participantsperformed debugging tasks using information provided by our approach, ourtool was as useful as a gdb baseline, but applies transparently. Our dynamic analysis approach permitstransparent introspection to access previously-unavailable informationabout a process's internal state with minimal instrumentation artifacts. Kevin Leach, Chad Spensky, Westley Weimer, Fengwei Zhang |
SANER | 3 |
| 2015 | Deep Parameter OptimisationabstractWe introduce a mutation-based approach to automatically discover and expose `deep' (previously unavailable) parameters that affect a program's runtime costs. These discovered parameters, together with existing (`shallow') parameters, form a search space that we tune using search-based optimisation in a bi-objective formulation that optimises both time and memory consumption. We implemented our approach and evaluated it on four real-world programs. The results show that we can improve execution time by 12\% or achieve a 21\% memory consumption reduction in the best cases. In three subjects, our deep parameter tuning results in a significant improvement over the baseline of shallow parameter tuning, demonstrating the potential value of our deep parameter extraction approach. Fan Wu 0009, Westley Weimer, Mark Harman, Yue Jia 0001, Jens Krinke |
GECCO | 2 |
| 2015 | Modeling readability to improve unit testsabstractWriting good unit tests can be tedious and error prone, but even once they are written, the job is not done: Developers need to reason about unit tests throughout software development and evolution, in order to diagnose test failures, maintain the tests, and to understand code written by other developers. Unreadable tests are more difficult to maintain and lose some of their value to developers. To overcome this problem, we propose a domain-specific model of unit test readability based on human judgements, and use this model to augment automated unit test generation. The resulting approach can automatically generate test suites with both high coverage and also improved readability. In human studies users prefer our improved tests and are able to answer maintenance questions about them 14% more quickly at the same level of accuracy. Ermira Daka, José Campos 0001, Gordon Fraser 0001, Jonathan Dorn, Westley Weimer |
ESEC/SIGSOFT FSE | 5 |
| 2015 | Generating Readable Unit Tests for Guava
Ermira Daka, José Campos 0001, Jonathan Dorn, Gordon Fraser 0001, Westley Weimer |
SSBSE | 5 |
| 2015 | Towards Automatic Band-Limited Procedural ShadersabstractProcedural shaders are a vital part of modern rendering systems. Despite their prevalence, however, procedural shaders remain sensitive to aliasing any time they are sampled at a rate below the Nyquist limit. Antialiasing is typically achieved through numerical techniques like supersampling or precomputing integrals stored in mipmaps. This paper explores the problem of analytically computing a band-limited version of a procedural shader as a continuous function of the sampling rate. There is currently no known way of analytically computing these integrals in general. We explore the conditions under which exact solutions are possible and develop several approximation strategies for when they are not. Compared to supersampling methods, our approach produces shaders that are less expensive to evaluate and closer to ground truth in many cases. Compared to mipmapping or precomputation, our approach produces shaders that support an arbitrary bandwidth parameter and require less storage. We evaluate our method on a range of spatially-varying shader functions, automatically producing antialiased versions that have comparable error to 4×4 multisampling but can be over an order of magnitude faster. While not complete, our approach is a promising first step toward this challenging goal and indicates a number of interesting directions for future work. Jonathan Dorn, Connelly Barnes, Jason Lawrence, Westley Weimer |
Comput. Graph. Forum | 4 |
| 2015 | The ManyBugs and IntroClass Benchmarks for Automated Repair of C ProgramsabstractThe field of automated software repair lacks a set of common benchmark problems. Although benchmark sets are used widely throughout computer science, existing benchmarks are not easily adapted to the problem of automatic defect repair, which has several special requirements. Most important of these is the need for benchmark programs with reproducible, important defects and a deterministic method for assessing if those defects have been repaired. This article details the need for a new set of benchmarks, outlines requirements, and then presents two datasets, ManyBugs and IntroClass, consisting between them of 1,183 defects in 15 C programs. Each dataset is designed to support the comparative evaluation of automatic repair algorithms asking a variety of experimental questions. The datasets have empirically defined guarantees of reproducibility and benchmark quality, and each study object is categorized to facilitate qualitative evaluation and comparisons by category of bug or program. The article presents baseline experimental results on both datasets for three existing repair methods, GenProg, AE, and TrpAutoRepair, to reduce the burden on researchers who adopt these datasets for their own comparative evaluations. Claire Le Goues, Neal J. Holtschulte, Edward K. Smith, Yuriy Brun, Premkumar T. Devanbu, Stephanie Forrest, Westley Weimer |
IEEE Trans. Software Eng. | 7 |
| 2014 | Post-compiler software optimization for reducing energyabstractModern compilers typically optimize for executable size and speed, rarely exploring non-functional properties such as power efficiency. These properties are often hardware-specific, time-intensive to optimize, and may not be amenable to standard dataflow optimizations. We present a general post-compilation approach called Genetic Optimization Algorithm (GOA), which targets measurable non-functional aspects of software execution in programs that compile to x86 assembly. GOA combines insights from profile-guided optimization, superoptimization, evolutionary computation and mutational robustness. GOA searches for program variants that retain required functional behavior while improving non-functional behavior, using characteristic workloads and predictive modeling to guide the search. The resulting optimizations are validated using physical performance measurements and a larger held-out test suite. Our experimental results on PARSEC benchmark programs show average energy reductions of 20%, both for a large AMD system and a small Intel system, while maintaining program functionality on target workloads. Eric M. Schulte, Jonathan Dorn, Stephen Harding, Stephanie Forrest, Westley Weimer |
ASPLOS | 5 |
| 2014 | Using Genetic Improvement and Code Transplants to Specialise a C++ Program to a Problem Class
Justyna Petke, Mark Harman, William B. Langdon, Westley Weimer |
EuroGP | 4 |
| 2014 | Using dynamic analysis to generate disjunctive invariantsabstractProgram invariants are important for defect detection, program verification, and program repair. However, existing techniques have limited support for important classes of invariants such as disjunctions, which express the semantics of conditional statements. We propose a method for generating disjunctive invariants over numerical domains, which are inexpressible using classical convex polyhedra. Using dynamic analysis and reformulating the problem in non-standard ``max-plus'' and ``min-plus'' algebras, our method constructs hulls over program trace points. Critically, we introduce and infer a weak class of such invariants that balances expressive power against the computational cost of generating nonconvex shapes in high dimensions. ThanhVu Nguyen, Deepak Kapur, Westley Weimer, Stephanie Forrest |
ICSE | 3 |
| 2014 | genBRDF: discovering new analytic BRDFs with genetic programmingabstractWe present a framework for learning new analytic BRDF models through Genetic Programming that we call genBRDF. This approach to reflectance modeling can be seen as an extension of traditional methods that rely either on a phenomenological or empirical process. Our technique augments the human effort involved in deriving mathematical expressions that accurately characterize complex high-dimensional reflectance functions through a large-scale optimization. We present a number of analysis tools and data visualization techniques that are crucial to sifting through the large result sets produced by genBRDF in order to identify fruitful expressions. Additionally, we highlight several new models found by genBRDF that have not previously appeared in the BRDF literature. These new BRDF models are compact and more accurate than current state-of-the-art alternatives. Adam Brady, Jason Lawrence, Pieter Peers, Westley Weimer |
ACM Trans. Graph. | 4 |
| 2014 | DIG: A Dynamic Invariant Generator for Polynomial and Array InvariantsabstractThis article describes and evaluates DIG, a dynamic invariant generator that infers invariants from observed program traces, focusing on numerical and array variables. For numerical invariants, DIG supports both nonlinear equalities and inequalities of arbitrary degree defined over numerical program variables. For array invariants, DIG generates nested relations among multidimensional array variables. These properties are nontrivial and challenging for current static and dynamic invariant analysis methods. The key difference between DIG and existing dynamic methods is its generative technique, which infers invariants directly from traces, instead of using traces to filter out predefined templates. To generate accurate invariants, DIG employs ideas and tools from the mathematical and formal methods domains, including equation solving, polyhedra construction, and theorem proving; for example, DIG represents and reasons about polynomial invariants using geometric shapes. Experimental results on 27 mathematical algorithms and an implementation of AES encryption provide evidence that DIG is effective at generating invariants for these programs. ThanhVu Nguyen, Deepak Kapur, Westley Weimer, Stephanie Forrest |
ACM Trans. Softw. Eng. Methodol. | 3 |
| 2013 | Automated repair of binary and assembly programs for cooperating embedded devicesabstractWe present a method for automatically repairing arbitrary software defects in embedded systems, which have limited memory, disk and CPU capacities, but exist in great numbers. We extend evolutionary computation (EC) algorithms that search for valid repairs at the source code level to assembly and ELF format binaries, compensating for limited system resources with several algorithmic innovations. Our method does not require access to the source code or build toolchain of the software under repair, does not require program instrumentation, specialized execution environments, or virtual machines, or prior knowledge of the bug type. Eric M. Schulte, Jonathan DiLorenzo, Westley Weimer, Stephanie Forrest |
ASPLOS | 3 |
| 2013 | Leveraging Light-Weight Analyses to Aid Software MaintenanceabstractWe will evaluate our techniques and tools on large, real-world systems, comprising tens of millions of lines of code and thousands of defects. The proposed work will attempt to reduce the cost of three specific maintenance tasks: triaging automatically-generated defect reports, automatically synthesizing defect repairs, and automatically identifying out-of-date or incomplete system documentation. We hope to address bottlenecks in each of these three areas and show concrete time and effort savings for each process. The rest of this section describes each maintenance process and our proposed improvements in each case. Zachary P. Fry, Westley Weimer |
ICST | 2 |
| 2013 | Leveraging program equivalence for adaptive program repair: Models and first resultsabstractSoftware bugs remain a compelling problem. Automated program repair is a promising approach for reducing cost, and many methods have recently demonstrated positive results. However, success on any particular bug is variable, as is the cost to find a repair. This paper focuses on generate-and-validate repair methods that enumerate candidate repairs and use test cases to define correct behavior. We formalize repair cost in terms of test executions, which dominate most test-based repair algorithms. Insights from this model lead to a novel deterministic repair algorithm that computes a patch quotient space with respect to an approximate semantic equivalence relation. This allows syntactic and dataflow analysis techniques to dramatically reduce the repair search space. Generate-and-validate program repair is shown to be a dual of mutation testing, suggesting several possible cross-fertilizations. Evaluating on 105 real-world bugs in programs totaling 5MLOC and involving 10,000 tests, our new algorithm requires an order-of-magnitude fewer test evaluations than the previous state-of-the-art and is over three times more efficient monetarily. Westley Weimer, Zachary P. Fry, Stephanie Forrest |
ASE | 1 |
| 2013 | Advances in Automated Program Repair and a Call to Arms
Westley Weimer |
SSBSE | 1 |
| 2013 | Current challenges in automatic software repair
Claire Le Goues, Stephanie Forrest, Westley Weimer |
Softw. Qual. J. | 3 |
| 2012 | Representations and operators for improving evolutionary software repairabstractEvolutionary computation is a promising technique for automating time-consuming and expensive software maintenance tasks, including bug repair. The success of this approach, however, depends at least partially on the choice of representation, fitness function, and operators. Previous work on evolutionary software repair has employed different approaches, but they have not yet been evaluated in depth. This paper investigates representation and operator choices for source-level evolutionary program repair in the GenProg framework [17], focusing on: (1) representation of individual variants, (2) crossover design, (3) mutation operators, and (4) search space definition. We evaluate empirically on a dataset comprising 8 C programs totaling over 5.1 million lines of code and containing 105 reproducible, human-confirmed defects. Our results provide concrete suggestions for operator and representation design choices for evolutionary program repair. When augmented to incorporate these suggestions, GenProg repairs 5 additional bugs (60 vs. 55 out of 105), with a decrease in repair time of 17-43% for the more difficult repair searches. Claire Le Goues, Westley Weimer, Stephanie Forrest |
GECCO | 2 |
| 2012 | Synthesizing API usage examplesabstractKey program interfaces are sometimes documented with usage examples: concrete code snippets that characterize common use cases for a particular data type. While such documentation is known to be of great utility, it is burdensome to create and can be incomplete, out of date, or not representative of actual practice. We present an automatic technique for mining and synthesizing succinct and representative human-readable documentation of program interfaces. Our algorithm is based on a combination of path sensitive dataflow analysis, clustering, and pattern abstraction. It produces output in the form of well-typed program snippets which document initialization, method calls, assignments, looping constructs, and exception handling. In a human study involving over 150 participants, 82% of our generated examples were found to be at least as good at human-written instances and 94% were strictly preferred to state of the art code search. Raymond P. L. Buse, Westley Weimer |
ICSE | 2 |
| 2012 | A systematic study of automated program repair: Fixing 55 out of 105 bugs for $8 eachabstractThere are more bugs in real-world programs than human programmers can realistically address. This paper evaluates two research questions: “What fraction of bugs can be repaired automatically?” and “How much does it cost to repair a bug automatically?” In previous work, we presented GenProg, which uses genetic programming to repair defects in off-the-shelf C programs. To answer these questions, we: (1) propose novel algorithmic improvements to GenProg that allow it to scale to large programs and find repairs 68% more often, (2) exploit GenProg's inherent parallelism using cloud computing resources to provide grounded, human-competitive cost measurements, and (3) generate a large, indicative benchmark set to use for systematic evaluations. We evaluate GenProg on 105 defects from 8 open-source programs totaling 5.1 million lines of code and involving 10,193 test cases. GenProg automatically repairs 55 of those 105 defects. To our knowledge, this evaluation is the largest available of its kind, and is often two orders of magnitude larger than previous work in terms of code or test suite size or defect count. Public cloud computing prices allow our 105 runs to be reproduced for $403; a successful repair completes in 96 minutes and costs $7.32, on average. Claire Le Goues, Michael Dewey-Vogt, Stephanie Forrest, Westley Weimer |
ICSE | 4 |
| 2012 | Using dynamic analysis to discover polynomial and array invariantsabstractDynamic invariant analysis identifies likely properties over variables from observed program traces. These properties can aid programmers in refactoring, documenting, and debugging tasks by making dynamic patterns visible statically. Two useful forms of invariants involve relations among polynomials over program variables and relations among array variables. Current dynamic analysis methods support such invariants in only very limited forms. We combine mathematical techniques that have not previously been applied to this problem, namely equation solving, polyhedra construction, and SMT solving, to bring new capabilities to dynamic invariant detection. Using these methods, we show how to find equalities and inequalities among nonlinear polynomials over program variables, and linear relations among array variables of multiple dimensions. Preliminary experiments on 24 mathematical algorithms and an implementation of AES encryption provide evidence that the approach is effective at finding these invariants. ThanhVu Nguyen, Deepak Kapur, Westley Weimer, Stephanie Forrest |
ICSE | 3 |
| 2012 | A human study of patch maintainabilityabstractIdentifying and fixing defects is a crucial and expensive part of the software lifecycle. Measuring the quality of bug-fixing patches is a difficult task that affects both functional correctness and the future maintainability of the code base. Recent research interest in automatic patch generation makes a systematic understanding of patch maintainability and understandability even more critical. Zachary P. Fry, Bryan Landau, Westley Weimer |
ISSTA | 3 |
| 2012 | StrSolve: solving string constraints lazily
Pieter Hooimeijer, Westley Weimer |
Autom. Softw. Eng. | 2 |
| 2012 | GenProg: A Generic Method for Automatic Software RepairabstractThis paper describes GenProg, an automated method for repairing defects in off-the-shelf, legacy programs without formal specifications, program annotations, or special coding practices. GenProg uses an extended form of genetic programming to evolve a program variant that retains required functionality but is not susceptible to a given defect, using existing test suites to encode both the defect and required functionality. Structural differencing algorithms and delta debugging reduce the difference between this variant and the original program to a minimal repair. We describe the algorithm and report experimental results of its success on 16 programs totaling 1.25 M lines of C code and 120K lines of module code, spanning eight classes of defects, in 357 seconds, on average. We analyze the generated repairs qualitatively and quantitatively to demonstrate that the process efficiently produces evolved programs that repair the defect, are not fragile input memorizations, and do not lead to serious degradation in functionality. Claire Le Goues, ThanhVu Nguyen, Stephanie Forrest, Westley Weimer |
IEEE Trans. Software Eng. | 4 |
| 2012 | Measuring Code Quality to Improve Specification MiningabstractFormal specifications can help with program testing, optimization, refactoring, documentation, and, most importantly, debugging and repair. However, they are difficult to write manually, and automatic mining techniques suffer from 90-99 percent false positive rates. To address this problem, we propose to augment a temporal-property miner by incorporating code quality metrics. We measure code quality by extracting additional information from the software engineering process and using information from code that is more likely to be correct, as well as code that is less likely to be correct. When used as a preprocessing step for an existing specification miner, our technique identifies which input is most indicative of correct program behavior, which allows off-the-shelf techniques to learn the same number of specifications using only 45 percent of their original input. As a novel inference technique, our approach has few false positives in practice (63 percent when balancing precision and recall, 3 percent when focused on precision), while still finding useful specifications (e.g., those that find many bugs) on over 1.5 million lines of code. Claire Le Goues, Westley Weimer |
IEEE Trans. Software Eng. | 2 |
| 2011 | Benefits and barriers of user evaluation in software engineering researchabstractIn this paper, we identify trends about, benefits from, and barriers to performing user evaluations in software engineering research. From a corpus of over 3,000 papers spanning ten years, we report on various subtypes of user evaluations (e.g., coding tasks vs. questionnaires) and relate user evaluations to paper topics (e.g., debugging vs. technology transfer). We identify the external measures of impact, such as best paper awards and citation counts, that are correlated with the presence of user evaluations. We complement this with a survey of over 100 researchers from over 40 different universities and labs in which we identify a set of perceived barriers to performing user evaluations. Raymond P. L. Buse, Caitlin Sadowski, Westley Weimer |
OOPSLA | 3 |
| 2011 | Automating regression testing using web-based application similarities
Kinga Dobolyi, Elizabeth Soechting, Westley Weimer |
Int. J. Softw. Tools Technol. Transf. | 3 |
| 2011 | Genetic programming for shader simplificationabstractWe present a framework based on Genetic Programming (GP) for automatically simplifying procedural shaders. Our approach computes a series of increasingly simplified shaders that expose the inherent trade-off between speed and accuracy. Compared to existing automatic methods for pixel shader simplification [Olano et al. 2003; Pellacini 2005], our approach considers a wider space of code transformations and produces faster and more faithful results. We further demonstrate how our cost function can be rapidly evaluated using graphics hardware, which allows tens of thousands of shader variants to be considered during the optimization process. Our approach is also applicable to multi-pass shaders and perceptual-based error metrics. Pitchaya Sitthi-amorn, Nicholas Modly, Westley Weimer, Jason Lawrence |
ACM Trans. Graph. | 3 |
| 2010 | Designing better fitness functions for automated program repairabstractEvolutionary methods have been used to repair programs automatically, with promising results. However, the fitness function used to achieve these results was based on a few simple test cases and is likely too simplistic for larger programs and more complex bugs. We focus here on two aspects of fitness evaluation: efficiency and precision. Efficiency is an issue because many programs have hundreds of test cases, and it is costly to run each test on every individual in the population. Moreover, the precision of fitness functions based on test cases is limited by the fact that a program either passes a test case, or does not, which leads to a fitness function that can take on only a few distinct values. This paper investigates two approaches to enhancing fitness functions for program repair, incorporating (1) test suite selection to improve efficiency and (2) formal specifications to improve precision. We evaluate test suite selection on 10 programs, improving running time for automated repair by 81%. We evaluate program invariants using the Fitness Distance Correlation (FDC) metric, demonstrating significant improvements and smoother evolution of repairs Ethan Fast, Claire Le Goues, Stephanie Forrest, Westley Weimer |
GECCO | 4 |
| 2010 | A human study of fault localization accuracyabstractLocalizing and repairing defects are critical software engineering activities. Not all programs and not all bugs are equally easy to debug, however. We present formal models, backed by a human study involving 65 participants (from both academia and industry) and 1830 total judgments, relating various software- and defect-related features to human accuracy at locating errors. Our study involves example code from Java textbooks, helping us to control for both readability and complexity. We find that certain types of defects are much harder for humans to locate accurately. For example, humans are over five times more accurate at locating “extra statements” than “missing statements” based on experimental observation. We also find that, independent of the type of defect involved, certain code contexts are harder to debug than others. For example, humans are over three times more accurate at finding defects in code that provides an array abstraction than in code that provides a tree abstraction. We identify and analyze code features that are predictive of human fault localization accuracy. Finally, we present a formal model of debugging accuracy based on those source code features that have a statistically significant correlation with human performance. Zachary P. Fry, Westley Weimer |
ICSM | 2 |
| 2010 | Modeling consumer-perceived web application fault severities for testingabstractDespite the growing usage of web applications, extreme resource constraints during their development frequently leave them inadequately tested. Because testing may be perceived as having a low return on investment for web applications, we believe that providing a consumer-perceived fault severity model could allow developers to prioritize faults according to their likelihood of impacting consumer retention, encouraging web application developers to test more effectively. In a study involving 386 humans and 800 web application faults, we observe that an arbitrary human judgment of fault severity is unreliable. We thus present two models of fault severity that outperform individual humans in terms of correctly predicting the average consumer-perceived severity of web application faults. Our first model uses human annotations of fault surface features, and is 87 % accurate at identifying low-priority, non-severe faults. We also present a fully automated conservative model that correctly identifies 55 % of non-severe faults without missing any severe faults. Both models outperform humans at flagging severe faults, and can substitute or reinforce humans by prioritizing faults encountered in web application development and testing. Kinga Dobolyi, Westley Weimer |
ISSTA | 2 |
| 2010 | Automatically documenting program changesabstractSource code modifications are often documented with log messages. Such messages are a key component of software maintenance: they can help developers validate changes, locate and triage defects, and understand modifications. However, this documentation can be burdensome to create and can be incomplete or inaccurate. Raymond P. L. Buse, Westley Weimer |
ASE | 2 |
| 2010 | Solving string constraints lazilyabstractDecision procedures have long been a fixture in program analysis, and reasoning about string constraints is a key element in many program analyses and testing frameworks. Recent work on string analysis has focused on providing decision procedures that model string operations. Separating string analysis from its client applications has important and familiar benefits: it enables the independent improvement of string analysis tools and it saves client effort. Pieter Hooimeijer, Westley Weimer |
ASE | 2 |
| 2010 | Automated program repair through the evolution of assembly codeabstractA method is described for automatically repairing legacy software at the assembly code level using evolutionary computation. The technique is demonstrated on Java byte code and x86 assembly programs, showing how to find program variations that correct defects while retaining desired behavior. Test cases are used to demonstrate the defect and define required functionality. The paper explores advantages of assembly-level repair over earlier work at the source code level - the ability to repair programs written in many different languages; and the ability to repair bugs that were previously intractable. The paper reports experimental results showing reasonable performance of assembly language repair even on non-trivial programs Eric M. Schulte, Stephanie Forrest, Westley Weimer |
ASE | 3 |
| 2010 | Learning a Metric for Code ReadabilityabstractIn this paper, we explore the concept of code readability and investigate its relation to software quality. With data collected from 120 human annotators, we derive associations between a simple set of local code features and human notions of readability. Using those features, we construct an automated readability measure and show that it can be 80 percent effective and better than a human, on average, at predicting readability judgments. Furthermore, we show that this metric correlates strongly with three measures of software quality: code changes, automated defect reports, and defect log messages. We measure these correlations on over 2.2 million lines of code, as well as longitudinally, over many releases of selected projects. Finally, we discuss the implications of this study on programming language design and engineering practice. For example, our data suggest that comments, in and of themselves, are less important than simple blank lines to local judgments of readability. Raymond P. L. Buse, Westley Weimer |
IEEE Trans. Software Eng. | 2 |
| 2009 | Exploiting refactoring in formal verificationabstractIn previous work, we introduced Echo, a new approach to the formal verification of the functional correctness of software. Part of what makes Echo practical is a technique called verification refactoring. The program to be verified is mechanically refactored specifically to facilitate verification. After refactoring, the program is documented with low-level annotations, and a specification is extracted mechanically. Proofs that the semantics of the refactored program are equivalent to those of the original program, that the code conforms to the annotations, and that the extracted specification implies the program's original specification constitute the verification argument. In this paper, we discuss verification refactoring and illustrate it with a case study of the verification of an optimized implementation of the advanced encryption standard (AES) against its official specification. We compare the practicality of verification using refactoring with traditional correctness proofs and refinement, and we assess its efficacy using seeded defects. Xiang Yin 0001, John C. Knight, Westley Weimer |
DSN | 3 |
| 2009 | A genetic programming approach to automated software repairabstractGenetic programming is combined with program analysis methods to repair bugs in off-the-shelf legacy C programs. Fitness is defined using negative test cases that exercise the bug to be repaired and positive test cases that encode program requirements. Once a successful repair is discovered, structural differencing algorithms and delta debugging methods are used to minimize its size. Several modifications to the GP technique contribute to its success: (1) genetic operations are localized to the nodes along the execution path of the negative test case; (2) high-level statements are represented as single nodes in the program tree; (3) genetic operators use existing code in other parts of the program, so new code does not need to be invented. The paper describes the method, reviews earlier experiments that repaired 11 bugs in over 60,000 lines of code, reports results on new bug repairs, and describes experiments that analyze the performance and efficacy of the evolutionary components of the algorithm. Stephanie Forrest, ThanhVu Nguyen, Westley Weimer, Claire Le Goues |
GECCO | 3 |
| 2009 | The road not taken: Estimating path execution frequency staticallyabstractA variety of compilers, static analyses, and testing frameworks rely heavily on path frequency information. Uses for such information range from optimizing transformations to bug finding. Path frequencies are typically obtained through profiling, but that approach is severely restricted: it requires running programs in an indicative environment, and on indicative test inputs. We present a descriptive statistical model of path frequency based on features that can be readily obtained from a program's source code. Our model is over 90% accurate with respect to several benchmarks, and is sufficient for selecting the 5% of paths that account for over half of a program's total runtime. We demonstrate our technique's robustness by measuring its performance as a static branch predictor, finding it to be more accurate than previous approaches on average. Finally, our qualitative analysis of the model provides insight into which source-level features indicate ldquohot pathsrdquo. Raymond P. L. Buse, Westley Weimer |
ICSE | 2 |
| 2009 | Automatically finding patches using genetic programmingabstractAutomatic program repair has been a longstanding goal in software engineering, yet debugging remains a largely manual process. We introduce a fully automated method for locating and repairing bugs in software. The approach works on off-the-shelf legacy applications and does not require formal specifications, program annotations or special coding practices. Once a program fault is discovered, an extended form of genetic programming is used to evolve program variants until one is found that both retains required functionality and also avoids the defect in question. Standard test cases are used to exercise the fault and to encode program requirements. After a successful repair has been discovered, it is minimized using structural differencing algorithms and delta debugging. We describe the proposed method and report experimental results demonstrating that it can successfully repair ten different C programs totaling 63,000 lines in under 200 seconds, on average. Westley Weimer, ThanhVu Nguyen, Claire Le Goues, Stephanie Forrest |
ICSE | 1 |
| 2009 | Harnessing Web-Based Application Similarities to Aid in Regression TestingabstractWeb-based applications are growing in complexity and criticality, increasing the need for their precise validation. Regression testing is an established approach for providing information about the quality of an application in the face of recurring updates that dominate the web. We present techniques to address a key challenge of the automated regression testing of web-based applications. Innocuous program evolutions often appear to fail tests and must be manually inspected. We rely on inherent similarities between independent web-based applications to provide fully automated solutions for reducing the number of false positives associated with regression testing such applications, simultaneously focusing on returning all true positives. Our approach predicts which test cases merit human inspection by applying a model derived from regression testing other programs. We are 2.5 to 50 times as accurate as current industrial practice, but require no user annotations. Kinga Dobolyi, Westley Weimer |
ISSRE | 2 |
| 2009 | A decision procedure for subset constraints over regular languagesabstractReasoning about string variables, in particular program inputs, is an important aspect of many program analyses and testing frameworks. Program inputs invariably arrive as strings, and are often manipulated using high-level string operations such as equality checks, regular expression matching, and string concatenation. It is difficult to reason about these operations because they are not well-integrated into current constraint solvers. Pieter Hooimeijer, Westley Weimer |
PLDI | 2 |
| 2009 | Macrodebugging: global views of distributed program executionabstractCreating and debugging programs for wireless embedded networks (WENs) is notoriously difficult. Macroprogramming is an emerging technology that aims to address this problem by providing high-level programming abstractions. We present MDB, the first system to support the debugging of macroprograms. MDB allows the user to set break-points and step through a macroprogram using a source-level debugging interface similar to GDB, a process we call macrodebugging. A key challenge of MDB is to step through a macroprogram in sequential order even though it executes on the network in a distributed, asynchronous manner. Besides allowing the user to view distributed state, MDB also provides the ability to search for bugs over the entire history of distributed states. Finally, MDB allows the user to make hypothetical changes to a macroprogram and to see the effect on distributed state without the need to redeploy, execute, and test the new code. We show that macrodebugging is both easy and efficient: MDB consumes few system resources and requires few user commands to find the cause of bugs. We also provide a lightweight version of MDB called MDB Lite that can be used during the deployment phase to reduce resource consumption while still eliminating the possibility of heisenbugs: changes in the manifestation of bugs caused by enabling or disabling the debugger. Tamim I. Sookoor, Timothy W. Hnat, Pieter Hooimeijer, Westley Weimer, Kamin Whitehouse |
SenSys | 4 |
| 2009 | Specification Mining with Few False Positives
Claire Le Goues, Westley Weimer |
TACAS | 2 |
| 2008 | Automated duplicate detection for bug tracking systemsabstractBug tracking systems are important tools that guide the maintenance activities of software developers. The utility of these systems is hampered by an excessive number of duplicate bug reports-in some projects as many as a quarter of all reports are duplicates. Developers must manually identify duplicate bug reports, but this identification process is time-consuming and exacerbates the already high cost of software maintenance. We propose a system that automatically classifies duplicate bug reports as they arrive to save developer time. This system uses surface features, textual semantics, and graph clustering to predict duplicate status. Using a dataset of 29,000 bug reports from the Mozilla project, we perform experiments that include a simulation of a real-time bug reporting environment. Our system is able to reduce development cost by filtering out 8% of duplicate bug reports while allowing at least one report for each real defect to reach developers. Nicholas Jalbert, Westley Weimer |
DSN | 2 |
| 2008 | Changing Java's Semantics for Handling Null Pointer ExceptionsabstractWe envision a world where no exceptions are raised; instead, language semantics are changed so that operations are total functions. Either an operation executes normally or tailored recovery code is applied where exceptions would have been raised. As an initial step and evaluation of this idea, we propose to transform programs so that null pointer dereferences are handled automatically without a large runtime overhead. We increase robustness by replacing code that raises null pointer exceptions with error-handling code, allowing the program to continue execution. Our technique first finds potential null pointer dereferences and then automatically transforms programs to insert null checks and error-handling code. These transformations are guided by composable, context-sensitive recovery policies. Error-handling code may, for example, create default objects of the appropriate types, or restore data structure invariants. If no null pointers would be dereferenced, the transformed program behaves just as the original.We applied our transformation in experiments involving multiple benchmarks, the Java Standard Library, and externally reported null pointer exceptions. Our technique was able to handle the reported exceptions and allow the programs to continue to do useful work, with an average execution time overhead of less than 1% and an average bytecode space overhead of 22%. Kinga Dobolyi, Westley Weimer |
ISSRE | 2 |
| 2008 | A metric for software readabilityabstractIn this paper, we explore the concept of code readability and investigate its relation to software quality. With data collected from human annotators, we derive associations between a simple set of local code features and human notions of readability. Using those features, we construct an automated readability measure and show that it can be 80% effective, and better than a human on average, at predicting readability judgments. Furthermore, we show that this metric correlates strongly with two traditional measures of software quality, code changes and defect reports. Finally, we discuss the implications of this study on programming language design and engineering practice. For example, our data suggests that comments, in of themselves, are less important than simple blank lines to local judgments of readability. Raymond P. L. Buse, Westley Weimer |
ISSTA | 2 |
| 2008 | Automatic documentation inference for exceptionsabstractException handling is a powerful and widely-used program-ming language abstraction for constructing robust software systems. Unfortunately, it introduces an inter-procedural flow of control that can be difficult to reason about. Fail-ure to do so correctly can lead to security vulnerabilities, breaches of API encapsulation, and any number of safety policy violations. We present a fully automated tool that statically infers and characterizes exception-causing conditions in Java pro-grams. Our tool is based on an inter-procedural, context-sensitive analysis. The output of this tool is well-suited for use as human-readable documentation of exceptional condi-tions. We evaluate the output of our tool by comparing it to over 900 instances of existing exception documentation in almost two million lines of code. We find that the output of our tool is at least as good as existing documentation 85% of the time and is better 25 % of the time. Raymond P. L. Buse, Westley Weimer |
ISSTA | 2 |
| 2008 | Formal Verification by Reverse Synthesis
Xiang Yin 0001, John C. Knight, Elisabeth A. Nguyen, Westley Weimer |
SAFECOMP | 4 |
| 2008 | MacroLab: a vector-based macroprogramming framework for cyber-physical systemsabstractWe present a macroprogramming framework called MacroLab that offers a vector programming abstraction similar to Matlab for Cyber-Physical Systems (CPSs). The user writes a single program for the entire network using Matlab-like operations such as addition, find, and max. The framework executes these operations across the network in a distributed fashion, a centralized fashion, or something between the two - whichever is most efficient for the target deployment. We call this approach deployment-specific code decomposition (DSCD). MacroLab programs can be executed on mote-class hardware such as the Telos [24] motes. Our results indicate that MacroLab introduces almost no additional overhead in terms of message cost, power consumption, memory footprint, or CPU cycles over TinyOS Timothy W. Hnat, Tamim I. Sookoor, Pieter Hooimeijer, Westley Weimer, Kamin Whitehouse |
SenSys | 4 |
| 2008 | Exceptional situations and program reliabilityabstractIt is difficult to write programs that behave correctly in the presence of run-time errors. Proper behavior in the face of exceptional situations is important to the reliability of long-running programs. Existing programming language features often provide poor support for executing clean-up code and for restoring invariants. We present a data-flow analysis for finding a certain class of exception-handling defects: those related to a failure to release resources or to clean up properly along all paths. Many real-world programs violate such resource usage rules because of incorrect exception handling. Our flow-sensitive analysis keeps track of outstanding obligations along program paths and does a precise modeling of control flow in the presence of exceptions. Using it, we have found over 1,300 exception handling defects in over 5 million lines of Java code. Based on those defects we propose a programming language feature, the compensation stack, that keeps track of obligations at run time and ensures that they are discharged. We present a type system for compensation stacks that tracks collections of obligations. Finally, we present case studies to demonstrate that this feature is natural, efficient, and can improve reliability. Westley Weimer, George C. Necula |
ACM Trans. Program. Lang. Syst. | 1 |
| 2008 | Privately Finding SpecificationsabstractBuggy software is a reality and automated techniques for discovering bugs are highly desirable. A specification describes the correct behavior of a program. For example, a file must eventually be closed once it has been opened. Specifications are learned by finding patterns in normal program execution traces versus erroneous ones. With more traces, more specifications can be learned more accurately. By combining traces from multiple parties that possess distinct programs but use a common library, it is possible to obtain sufficiently many traces. However, obtaining traces from competing parties is problematic: By revealing traces, it may be possible to learn that one party writes buggier code than another. We present an algorithm by which mutually distrusting parties can work together to learn program specifications while preserving their privacy. We use a perturbation algorithm to obfuscate individual trace values while still allowing statistical trends to be mined from the data. Despite the noise introduced to safeguard privacy, empirical evidence suggests that our algorithm learns specifications that find 85 percent of the bugs that a no-privacy approach would find. Westley Weimer, Nina Mishra |
IEEE Trans. Software Eng. | 1 |
| 2007 | Modeling bug report qualityabstractSoftware developers spend a significant portion of their resources handling user-submitted bug reports. For software that is widely deployed, the number of bug reports typically outstrips the resources available to triage them. As a result, some reports may be dealt with too slowly or not at all. Pieter Hooimeijer, Westley Weimer |
ASE | 2 |
| 2006 | Patches as better bug reportsabstractTools and analyses that find bugs in software are becoming increasingly prevalent. However, even after the potential false alarms raised by such tools are dealt with, many real reported errors may go unfixed. In such cases the programmers have judged the benefit of fixing the bug to be less than the time cost of understanding and fixing it.The true utility of a bug-finding tool lies not in the number of bugs it finds but in the number of bugs it causes to be fixed.Analyses that find safety-policy violations typically give error reports as annotated backtraces or counterexamples. We propose that bug reports additionally contain a specially-constructed patch describing an example way in which the program could be modified to avoid the reported policy violation. Programmers viewing the analysis output can use such patches as guides, starting points, or as an additional way of understanding what went wrong.We present an algorithm for automatically constructing such patches given model-checking and policy information typically already produced by most such analyses. We are not aware of any previous automatic techniques for generating patches in response to safety policy violations. Our patches can suggest additional code not present in the original program, and can thus help to explain bugs related to missing program elements. In addition, our patches do not introduce any new violations of the given safety policy.To evaluate our method we performed a software engineering experiment, applying our algorithm to over 70 bug reports produced by two off-the-shelf bug-finding tools running on large Java programs. Bug reports also accompanied by patches were three times as likely to be addressed as standard bug reports.This work represents an early step toward developing new ways to report bugs and to make it easier for programmers to fix them. Even a minor increase in our ability to fix bugs would be a great increase for the quality of software. Westley Weimer |
GPCE | 1 |
| 2005 | Mining Temporal Specifications for Error Detection
Westley Weimer, George C. Necula |
TACAS | 1 |
| 2005 | CCured: type-safe retrofitting of legacy softwareabstractThis article describes CCured, a program transformation system that adds type safety guarantees to existing C programs. CCured attempts to verify statically that memory errors cannot occur, and it inserts run-time checks where static verification is insufficient.CCured extends C's type system by separating pointer types according to their usage, and it uses a surprisingly simple type inference algorithm that is able to infer the appropriate pointer kinds for existing C programs. CCured uses physical subtyping to recognize and verify a large number of type casts at compile time. Additional type casts are verified using run-time type information. CCured uses two instrumentation schemes, one that is optimized for performance and one in which metadata is stored in a separate data structure whose shape mirrors that of the original user data. This latter scheme allows instrumented programs to invoke external functions directly on the program's data without the use of a wrapper function.We have used CCured on real-world security-critical network daemons to produce instrumented versions without memory-safety vulnerabilities, and we have found several bugs in these programs. The instrumented code is efficient enough to be used in day-to-day operations. George C. Necula, Jeremy Condit, Matthew Harren, Scott McPeak, Westley Weimer |
ACM Trans. Program. Lang. Syst. | 5 |
| 2004 | Finding and preventing run-time error handling mistakesabstractIt is difficult to write programs that behave correctly in the presence of run-time errors. Existing programming language features often provide poor support for executing clean-up code and for restoring invariants in such exceptional situations. We present a dataflow analysis for finding a certain class of error-handling mistakes: those that arise from a failure to release resources or to clean up properly along all paths. Many real-world programs violate such resource safety policies because of incorrect error handling. Our flow-sensitive analysis keeps track of outstanding obligations along program paths and does a precise modeling of control flow in the presence of exceptions. Using it, we have found over 800 error handling mistakes almost 4 million lines of Java code. The analysis is unsound and produces false positives, but a few simple filtering rules suffice to remove them in practice. The remaining mistakes were manually verified. These mistakes cause sockets, files and database handles to be leaked along some paths. We present a characterization of the most common causes of those errors and discuss the limitations of exception handling, finalizers and destructors in addressing them. Based on those errors, we propose a programming language feature that keeps track of obligations at run time and ensures that they are discharged. Finally, we present case studies to demonstrate that this feature is natural, efficient, and can improve reliability; for example, retrofitting a 34kLOC program with it resulted in a 0.5% code size decrease, a surprising 17% speed increase (from correctly deallocating resources in the presence of exceptions), and more consistent behavior. Westley Weimer, George C. Necula |
OOPSLA | 1 |
| 2003 | CCured in the real worldabstractCCured is a program transformation system that adds memory safety guarantees to C programs by verifying statically that memory errors cannot occur and by inserting run-time checks where static verification is insufficient.This paper addresses major usability issues in a previous version of CCured, in which many type casts required the use of pointers whose representation was expensive and incompatible with precompiled libraries. We have extended the CCured type inference algorithm to recognize and verify statically a large number of type casts; this goal is achieved by using physical subtyping and pointers with run-time type information to allow parametric and subtype polymorphism. In addition, we present a new instrumentation scheme that splits CCured's metadata into a separate data structure whose shape mirrors that of the original user data. This scheme allows instrumented programs to invoke external functions directly on the program's data without the use of a wrapper function.With these extensions we were able to use CCured on real-world security-critical network daemons and to produce instrumented versions without memory-safety vulnerabilities. Jeremy Condit, Matthew Harren, Scott McPeak, George C. Necula, Westley Weimer |
PLDI | 5 |
| 2002 | Temporal-Safety Proofs for Systems Code
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George C. Necula, Grégoire Sutre, Westley Weimer |
CAV | 6 |
| 2002 | CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs
George C. Necula, Scott McPeak, Shree Prakash Rahul, Westley Weimer |
CC | 4 |
| 2002 | CCured: type-safe retrofitting of legacy codeabstractIn this paper we propose a scheme that combines type inference and run-time checking to make existing C programs type safe. We describe the CCured type system, which extends that of C by separating pointer types according to their usage. This type system allows both pointers whose usage can be verified statically to be type safe, and pointers whose safety must be checked at run time. We prove a type soundness result and then we present a surprisingly simple type inference algorithm that is able to infer the appropriate pointer kinds for existing C programs.Our experience with the CCured system shows that the inference is very effective for many C programs, as it is able to infer that most or all of the pointers are statically verifiable to be type safe. The remaining pointers are instrumented with efficient run-time checks to ensure that they are used safely. The resulting performance loss due to run-time checks is 0-150%, which is several times better than comparable approaches that use only dynamic checking. Using CCured we have discovered programming bugs in established C programs such as several SPECINT95 benchmarks. George C. Necula, Scott McPeak, Westley Weimer |
POPL | 3 |
| 2002 | Speeding Up Dataflow Analysis Using Flow-Insensitive Pointer Analysis
Stephen Adams 0001, Thomas Ball 0001, Manuvir Das, Sorin Lerner, Sriram K. Rajamani, Mark Seigle, Westley Weimer |
SAS | 7 |
| 2000 | OceanStore: An Architecture for Global-Scale Persistent StorageabstractOceanStore is a utility infrastructure designed to span the globe and provide continuous access to persistent information. Since this infrastructure is comprised of untrusted servers, data is protected through redundancy and cryptographic techniques. To improve performance, data is allowed to be cached anywhere, anytime. Additionally, monitoring of usage patterns allows adaptation to regional outages and denial of service attacks; monitoring also enhances performance through pro-active movement of data. A prototype implementation is currently under development. John Kubiatowicz, David Bindel, Yan Chen 0004, Steven E. Czerwinski, Patrick R. Eaton, Dennis Geels, Ramakrishna Gummadi, Sean C. Rhea, Hakim Weatherspoon, Westley Weimer, Chris Wells, Ben Y. Zhao |
ASPLOS | 10 |