publications
preprint
2024
- arXivGradual C0: Symbolic Execution for Gradual VerificationJenna DiVincenzo, Ian McCormack, Hemant Gouni, Jacob Gorenburg, Jan-Paul Ramos-Dávila, Mona Zhang, Conrad Zimmerman, Joshua Sunshine, Éric Tanter, and Jonathan AldricharXiv preprint arXiv:2210.02428, Jan 2024
Current static verification techniques support a wide range of programs. However, such techniques only support complete and detailed specifications, which places an undue burden on users. To solve this problem, prior work proposed gradual verification, which handles complete, partial, or missing specifications by soundly combining static and dynamic checking. Gradual verification has also been extended to programs that manipulate recursive, mutable data structures on the heap. Unfortunately, this extension does not reward users with decreased dynamic checking as specifications are refined. In fact, all properties are checked dynamically regardless of any static guarantees. Additionally, no full-fledged implementation of gradual verification exists so far, which prevents studying its performance and applicability in practice. We present Gradual C0, the first practicable gradual verifier for recursive heap data structures, which targets C0, a safe subset of C designed for education. Static verifiers supporting separation logic or implicit dynamic frames use symbolic execution for reasoning; so Gradual C0, which extends one such verifier, adopts symbolic execution at its core instead of the weakest liberal precondition approach used in prior work. Our approach addresses technical challenges related to symbolic execution with imprecise specifications, heap ownership, and branching in both program statements and specification formulas. We also deal with challenges related to minimizing insertion of dynamic checks and extensibility to other programming languages beyond C0. Finally, we provide the first empirical performance evaluation of a gradual verifier, and found that on average, Gradual C0 decreases run-time overhead between 11-34% compared to the fully-dynamic approach used in prior work. Further, the worst-case scenarios for performance are predictable and avoidable.
conference and journal
2024
- POPLSound Gradual Verification with Symbolic ExecutionConrad Zimmerman, Jenna DiVincenzo, and Jonathan AldrichProc. ACM Program. Lang., Jan 2024
Gradual verification, which supports explicitly partial specifications and verifies them with a combination of static and dynamic checks, makes verification more incremental and provides earlier feedback to developers. While an abstract, weakest precondition-based approach to gradual verification was previously proven sound, the approach did not provide sufficient guidance for implementation and optimization of the required run-time checks. More recently, gradual verification was implemented using symbolic execution techniques, but the soundness of the approach (as with related static checkers based on implicit dynamic frames) was an open question. This paper puts practical gradual verification on a sound footing with a formalization of symbolic execution, optimized run-time check generation, and run time execution. We prove our approach is sound; our proof also covers a core subset of the Viper tool, for which we are aware of no previous soundness result. Our formalization enabled us to find a soundness bug in an implemented gradual verification tool and describe the fix necessary to make it sound.
2023
2021
- ECOOPGradual Program Analysis for Null PointersSam Estep, Jenna L Wise, Jonathan Aldrich, Éric Tanter, Johannes Bader, and Joshua SunshineIn 35th European Conference on Object-Oriented Programming (ECOOP 2021), Dec 2021
Static analysis tools typically address the problem of excessive false positives by requiring programmers to explicitly annotate their code. However, when faced with incomplete annotations, many analysis tools are either too conservative, yielding false positives, or too optimistic, resulting in unsound analysis results. In order to flexibly and soundly deal with partially-annotated programs, we propose to build upon and adapt the gradual typing approach to abstract-interpretation-based program analyses. Specifically, we focus on null-pointer analysis and demonstrate that a gradual null-pointer analysis hits a sweet spot, by gracefully applying static analysis where possible and relying on dynamic checks where necessary for soundness. In addition to formalizing a gradual null-pointer analysis for a core imperative language, we build a prototype using the Infer static analysis framework, and present preliminary evidence that the gradual null-pointer analysis reduces false positives compared to two existing null-pointer checkers for Infer. Further, we discuss ways in which the gradualization approach used to derive the gradual analysis from its static counterpart can be extended to support more domains. This work thus provides a basis for future analysis tools that can smoothly navigate the tradeoff between human effort and run-time overhead to reduce the number of reported false positives.
- TOCHIPLIERS: a process that integrates user-centered methods into programming language designMichael Coblenz, Gauri Kambhatla, Paulette Koronkevich, Jenna L Wise, Celeste Barnaby, Joshua Sunshine, Jonathan Aldrich, and Brad A MyersACM Transactions on Computer-Human Interaction (TOCHI), Dec 2021
Programming language design requires making many usability-related design decisions. However, existing HCI methods can be impractical to apply to programming languages: languages have high iteration costs, programmers require significant learning time, and user performance has high variance. To address these problems, we adapted both formative and summative HCI methods to make them more suitable for programming language design. We integrated these methods into a new process, PLIERS, for designing programming languages in a user-centered way. We assessed PLIERS by using it to design two new programming languages. Glacier extends Java to enable programmers to express immutability properties effectively and easily. Obsidian is a language for blockchains that includes verification of critical safety properties. Empirical studies showed that the PLIERS process resulted in languages that could be used effectively by many programmers and revealed additional opportunities for language improvement.
2020
- OOPSLAGradual Verification of Recursive Heap Data StructuresJenna Wise, Johannes Bader, Cameron Wong, Jonathan Aldrich, Éric Tanter, and Joshua SunshineProceedings of the ACM on Programming Languages, Dec 2020
Current static verification techniques do not provide good support for incrementality, making it difficult for developers to focus on specifying and verifying the properties and components that are most important. Dynamic verification approaches support incrementality, but cannot provide static guarantees. To bridge this gap, prior work proposed gradual verification, which supports incrementality by allowing every assertion to be complete, partial, or omitted, and provides sound verification that smoothly scales from dynamic to static checking. The prior approach to gradual verification, however, was limited to programs without recursive data structures. This paper extends gradual verification to programs that manipulate recursive, mutable data structures on the heap. We address several technical challenges, such as semantically connecting iso- and equi-recursive interpretations of abstract predicates, and supporting gradual verification of heap ownership. This work thus lays the foundation for future tools that work on realistic programs and support verification within an engineering process in which cost-benefit trade-offs can be made.
- TOGPenrose: from mathematical notation to beautiful diagramsKatherine Ye, Wode Ni, Max Krieger, Dor Ma’ayan, Jenna Wise, Jonathan Aldrich, Joshua Sunshine, and Keenan CraneACM Transactions on Graphics (TOG), Dec 2020
We introduce a system called Penrose for creating mathematical diagrams. Its basic functionality is to translate abstract statements written in familiar math-like notation into one or more possible visual representations. Rather than rely on a fixed library of visualization tools, the visual representation is user-defined in a constraint-based specification language; diagrams are then generated automatically via constrained numerical optimization. The system is user-extensible to many domains of mathematics, and is fast enough for iterative design exploration. In contrast to tools that specify diagrams via direct manipulation or low-level graphics programming, Penrose enables rapid creation and exploration of diagrams that faithfully preserve the underlying mathematical meaning. We demonstrate the effectiveness and generality of the system by showing how it can be used to illustrate a diverse set of concepts from mathematics and computer graphics.
2018
- HPECPerformance of Graph Analytics Applications on Many-Core ProcessorsJenna Wise, Emily Lederman, Manoj Kumar, and Pratap PattnaikIn 2018 IEEE High Performance extreme Computing Conference (HPEC), Dec 2018
Attaining good performance on graph analytics applications on modern day many-core processors is challenging, because these processors have complex pipelines to manage out of order execution of hundreds of instructions in flight. These pipelines have been optimized for high performance computing (HPC) applications, not for graph analytics. It is preferable to leave the task of attaining good performance to the system developers, and to separate the performance concern from the application programmer’s concerns. In this paper, we show that the linear algebra formulation of graph-analytics effectively handles the aforementioned separation of concerns. This formulation is a better fit for many-core processors as the many-core processors are optimized for HPC applications which have a substantial linear algebra component. We show that on POWER8, a many-core processor, an eightfold performance advantage can be attained on the Graph500 benchmark by adopting the linear algebra formulation. We also present the CPI stack analysis of three graph analytics kernels, and show that the linear algebra implementations of these kernels make efficient use of the POWER8 core. Inhibitors to still better performance are discussed.
2016
- IEEETracking Developers’ eyes in the IDEBonita Sharif, Timothy Shaffer, Jenna Wise, and Jonathan I MaleticIEEE Software, Dec 2016
With recorded eye gaze sessions, researchers will be able to determine all the locations that developers examine in software development artifacts. This will pave the way to further improve IDEs to support developers in various software engineering tasks. Toward that goal, researchers developed iTrace, software that interfaces with an eye tracker and IDE to capture eye gaze on software artifacts and map them to their semantic meaning.
2015
- ESEC/FSEiTrace: Enabling Eye Tracking on Software Artifacts Within the IDE to Support Software Engineering TasksTimothy R Shaffer, Jenna L Wise, Braden M Walters, Sebastian C Müller, Michael Falcone, and Bonita SharifIn Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, Dec 2015
The paper presents iTrace, an Eclipse plugin that implicitly records developers’ eye movements while they work on change tasks. iTrace is the first eye tracking environment that makes it possible for researchers to conduct eye tracking studies on large software systems. An overview of the design and architecture is presented along with features and usage scenarios. iTrace is designed to support a variety of eye trackers. The design is flexible enough to record eye movements on various types of software artifacts (Java code, text/html/xml documents, diagrams), as well as IDE user interface elements. The plugin has been successfully used for software traceability tasks and program comprehension tasks. iTrace is also applicable to other tasks such as code summarization and code recommendations based on developer eye movements. A short video demonstration is available at https://youtu.be/3OUnLCX4dXo.
workshop
2024
- PriSCGradual Verification for Smart ContractsHaojia Sun, Kunal Singh, Jan-Paul Ramos-Dávila, Jonathan Aldrich, and Jenna DiVincenzoIn 8th Workshop on the Principles of Secure Compilation, 2024
Blockchains facilitate secure resource transactions through smart contracts, yet these digital agreements are prone to vulnerabilities, particularly when interacting with external contracts, leading to substantial monetary losses. Traditional verification techniques fall short in providing comprehensive security assurances, especially against re-entrancy attacks, due to the unavailable implementations of external contracts. This paper introduces an incremental approach: gradual verification. We combine static and dynamic verification techniques to enhance security, guarantee soundness and flexibility, and optimize resource usage in smart contract interactions. By implementing a prototype for gradually verifying Algorand smart contracts via the pyTEAL language, we demonstrate the effectiveness of our approach, contributing to the safe and efficient execution of smart contracts.
2020
- WGTGradual Verification of Recursive Heap Data StructuresJenna Wise, Johannes Bader, Jonathan Aldrich, Éric Tanter, and Joshua SunshineIn First ACM SIGPLAN Workshop on Gradual Typing, 2020
Static verification tools for recursive heap data structures impose significant annotation burden on developers. This is true even when verifying a simple function that inserts an element at the end of a linked list. Gradual verification was introduced to allow developers to deal with this burden incrementally, if at all. It draws from research on gradual typing to produce a verification system that supports imprecise specifications along a continuum. However, current gradual verification technology can only support a simple first-order specification logic. This paper outlines work in progress on an extension to gradual verification that supports implicit dynamic frames and recursive abstract predicates using examples. This paper also highlights challenges and proposes solutions to verifying such examples.
2016
- SEmotionTowards an Emotionally Aware Development Environment: Invited TalkJenna Wise, Brent Prox, Benjamin Clark, and Bonita SharifIn Proceedings of the 1st International Workshop on Emotion Awareness in Software Engineering, 2016
The paper takes a position on enhancing existing development environments to support awareness of developer affect. To realize this, the environment needs to implicitly interface with biometric devices such as an eye tracker. Such development environments can help the developer detect when they need to take a break or when they need help. Besides helping the developer, researchers can also make use of such environments to study developer behavior in a realistic setting thereby improving tool support for emotional awareness as well as other software tasks.
miscellaneous
2016
- SIAMRedistricting Youngstown Police BeatsSebastian Haigler, Ashley Orr, Eric Shehadi, Jenna Wise, and Kristi YazvacSIAM Undergraduate Research Online, 2016