An official website of the United States government
Functional programs typically interact with stateful libraries that hide state behind typed abstractions. One particularly important class of applications are data structure implementations that rely on such libraries to provide a level of efficiency and scalability that may be otherwise difficult to achieve. However, because the specifications of the methods provided by these libraries are necessarily general and rarely specialized to the needs of any specific client, any required application-level invariants must often be expressed in terms of additional constraints on the (often) opaque state maintained by the library. In this paper, we consider the specification and verification of suchrepresentation invariantsusingsymbolic finite automata(SFA). We show that SFAs can be used to succinctly and precisely capture fine-grained temporal and data-dependent histories of interactions between functional clients and stateful libraries. To facilitate modular and compositional reasoning, we integrate SFAs into a refinement type system to qualify stateful computations resulting from such interactions. The particular instantiation we consider,Hoare Automata Types(HATs), allows us to both specify and automatically type-check the representation invariants of a datatype, even when its implementation depends on stateful library methods that operate over hidden state. We also develop a new bidirectional type checking algorithm that implements an efficient subtyping inclusion check over HATs, enabling their translation into a form amenable for SMT-based automated verification. We present extensive experimental results on an implementation of this algorithm that demonstrates the feasibility of type-checking complex and sophisticated HAT-specified OCaml data structure implementations layered on top of stateful library APIs.
more »
« less
This content will become publicly available on January 7, 2026
Derivative-Guided Symbolic Execution
We consider the formulation of a symbolic execution (SE) procedure for functional programs that interact with effectful, opaque libraries. Our procedure allows specifications of libraries and abstract data type (ADT) methods that are expressed inLinear Temporal Logic over Finite Traces(LTLf), interpreting them assymbolic finite automata(SFAs) to enable intelligent specification-guided path exploration in this setting. We apply our technique to facilitate the falsification of complex data structure safety properties in terms of effectful operations made by ADT methods on underlying opaque representation type(s). Specifications naturally characterize admissible traces of temporally-ordered events that ADT methods (and the library methods they depend upon) are allowed to perform. We show how to use these specifications to construct feasible symbolic input states for the corresponding methods, as well as how to encode safety properties in terms of this formalism. More importantly, we incorporate the notion ofsymbolic derivatives, a mechanism that allows the SE procedure to intelligently underapproximate the set of precondition states it needs to explore, based on the automata structures latent in the provided specifications and the safety property that is to be falsified. Intuitively, derivatives enable symbolic execution to exploit temporal constraints defined by trace-based specifications to quickly prune unproductive paths and discover feasible error states. Experimental results on a wide-range of challenging ADT implementations demonstrate the effectiveness of our approach.
more »
« less
- Award ID(s):
- 2321680
- PAR ID:
- 10632795
- Publisher / Repository:
- Association for Computing Machinery
- Date Published:
- Journal Name:
- Proceedings of the ACM on Programming Languages
- Volume:
- 9
- Issue:
- POPL
- ISSN:
- 2475-1421
- Page Range / eLocation ID:
- 1475 to 1505
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
null (Ed.)Shape expressions (SEs) is a novel specification language that was recently introduced to express behavioral patterns over real-valued signals observed during the execution of cyber-physical systems. An SE is a regular expression composed of arbitrary parameterized shapes, such as lines, exponential curves, and sinusoids as atomic symbols with symbolic constraints on the shape parameters. SEs enable a natural and intuitive specification of complex temporal patterns over possibly noisy data. In this article, we propose a novel method for mining a broad and interesting fragment of SEs from time-series data using a combination of techniques from linear regression, unsupervised clustering, and learning finite automata from positive examples. The learned SE for a given dataset provides an explainable and intuitive model of the observed system behavior. We demonstrate the applicability of our approach on two case studies from different application domains and experimentally evaluate the implemented specification mining procedure.more » « less
-
Lightweight syntactic analysis tools like Semgrep and Comby leverage the tree structure of code, making them more expressive than string and regex search. Unlike traditional language frameworks (e.g., ESLint) that analyze codebases via explicit syntax tree manipulations, these tools use query languages that closely resemble the source language. However, state-of-the-art matching techniques for these tools require queries to be complete and parsable snippets, which makes in-progress query specifications useless. We propose a new search architecture that relies only on tokenizing (not parsing) a query. We introduce a novel language and matching algorithm to support tree-aware wildcards on this architecture by building on tree automata. We also presentstsearch, a syntactic search tool leveraging our approach. In contrast to past work, our approach supports syntactic searcheven for previously unparsable queries.We show empirically that stsea rch can support all tokenizable queries, while still providing results comparable to Semgrep for existing queries. Our work offers evidence that lightweight syntactic code search can accept in-progress specifications, potentially improving support for interactive settings. CCS Concepts: •Software and its engineering→Formal language definitions;Software maintenance tools;•Information systems→Query representation;•Theory of computation→ Tree languages.more » « less
-
ABSTRACT ObjectiveNeighborhood perceptions are associated with physical and mental health outcomes; however, the biological associates of this relationship remain to be fully understood. Here, we evaluate the relationship between neighborhood perceptions and amygdala activity and connectivity with salience network (i.e., insula, anterior cingulate, thalamus) nodes. MethodsForty-eight older adults (mean age = 68 [7] years, 52% female, 47% non-Hispanic Black, 2% Hispanic) without dementia or depression completed the Perceptions of Neighborhood Environment Scale. Lower scores indicated less favorable perceptions of aesthetic quality, walking environment, availability of healthy food, safety, violence (i.e., more perceived violence), social cohesion, and participation in activities with neighbors. Participants separately underwent resting-state functional magnetic resonance imaging. ResultsLess favorable perceived safety (β= −0.33,pFDR= .04) and participation in activities with neighbors (β= −0.35,pFDR= .02) were associated with higher left amygdala activity, independent of covariates including psychosocial factors. Less favorable safety perceptions were also associated with enhanced left amygdala functional connectivity with the bilateral insular cortices and the left anterior insula (β= −0.34,pFDR= .04). Less favorable perceived social cohesion was associated with enhanced left amygdala functional connectivity with the right thalamus (β =−0.42,pFDR= .04), and less favorable perceptions about healthy food availability were associated with enhanced left amygdala functional connectivity with the bilateral anterior insula (right:β= −0.39,pFDR= .04; left:β= −0.42,pFDR= .02) and anterior cingulate gyrus (β= −0.37,pFDR= .04). ConclusionsTaken together, our findings document relationships between select neighborhood perceptions and amygdala activity as well as connectivity with salience network nodes; if confirmed, targeted community-level interventions and existing community strengths may promote brain-behavior relationships.more » « less
-
We present a novel symbolic reasoning engine for SQL which can efficiently generate an inputIfornqueriesP1, ⋯,Pn, such that their outputs onIsatisfy a given property (expressed in SMT). This is useful in different contexts, such as disproving equivalence of two SQL queries and disambiguating a set of queries. Our first idea is to reason about an under-approximation of eachPi— that is, a subset ofPi’s input-output behaviors. While it makes our approach both semantics-aware and lightweight, this idea alone is incomplete (as a fixed under-approximation might miss some behaviors of interest). Therefore, our second idea is to perform search over an expressive family of under-approximations (which collectively cover all program behaviors of interest), thereby making our approach complete. We have implemented these ideas in a tool, Polygon, and evaluated it on over 30,000 benchmarks across two tasks (namely, SQL equivalence refutation and query disambiguation). Our evaluation results show that Polygon significantly outperforms all prior techniques.more » « less
