publications
preprint
2024
- arXiv (FORGE)Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFastWen Fan, Marilyn Rego, Xin Hu, Sanya Dod, Zhaorui Ni, Danning Xie, Jenna DiVincenzo, and Lin TanarXiv preprint arXiv:2411.02318, Dec 2024
Static verification is a powerful method for enhancing software quality, but it demands significant human labor and resources. This is particularly true of static verifiers that reason about heap manipulating programs using an ownership logic. LLMs have shown promise in a number of software engineering activities, including code generation, test generation, proof generation for theorem provers, and specification generation for static verifiers. However, prior work has not explored how well LLMs can perform specification generation for specifications based in an ownership logic, such as separation logic. To address this gap, this paper explores OpenAI’s GPT-4o model’s effectiveness in generating specifications on C programs that are verifiable with VeriFast, a separation logic based static verifier. Our experiment employs three different types of user inputs as well as basic and Chain-of-Thought (CoT) prompting to assess GPT’s capabilities. Our results indicate that the specifications generated by GPT-4o preserve functional behavior, but struggle to be verifiable. When the specifications are verifiable they contain redundancies. Future directions are discussed to improve the performance.
conference and journal
2025
- TOPLASGradual C0: Symbolic Execution for Gradual VerificationJenna DiVincenzo, Ian McCormack, Conrad Zimmerman, Hemant Gouni, Jacob Gorenburg, Jan-Paul Ramos-Dávila, Mona Zhang, Joshua Sunshine, Éric Tanter, and Jonathan AldrichACM Trans. Program. Lang. Syst., Jan 2025
Current static verification techniques such as separation logic 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 more specifications are written and more static guarantees are made. 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 7.1 and 40.2% compared to the fully dynamic approach used in prior work (for context, the worst cases for the approach by Wise et al. [2020] range from 0.1 to 4.5 seconds depending on the benchmark). Further, the worst-case scenarios for performance are predictable and avoidable. This work paves the way towards evaluating gradual verification at scale.
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
2025
- TPSAGradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual VerificationConrad Zimmerman, and Jenna DiVincenzoIn 1st Workshop on the Theory and Practice of Static Analysis, 2025
Previously, gradual verification has been developed using overapproximating logics such as Hoare logic. We show that the static verification component of gradual verification is also connected to underapproximating logics like incorrectness logic. To do this, we use a novel definition of gradual verification and a novel gradualization of exact logic (Maksimovic et al. 2023) which we call gradual exact logic. Further, we show that Hoare logic, incorrectness logic, and gradual verification can be defined in terms of gradual exact logic. We hope that this connection can be used to develop tools and techniques that apply to both gradual verification and bug-finding. For example, we envision that techniques defined in terms of exact logic can be directly applied to verification, bug-finding, and gradual verification, using the principles of gradual typing (Garcia et al. 2016).
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