An official website of the United States government
This paper presents a program analysis method that generates program summaries involving polynomial arithmetic. Our approach builds on prior techniques that use solvable polynomial maps for summarizing loops. These techniques are able to generateallpolynomial invariants for a restricted class of programs, but cannot be applied to programs outside of this class—for instance, programs with nested loops, conditional branching, unstructured control flow, etc. There currently lacks approaches to apply these prior methods to the case of general programs. This paper bridges that gap. Instead of restricting the kinds of programs we can handle, our methodabstractsevery loop into a model that can be solved with prior techniques, bringing to bear prior work on solvable polynomial maps to general programs. While no method can generate all polynomial invariants for arbitrary programs, our method establishes its merit through amonotonictyresult. We have implemented our techniques, and tested them on a suite of benchmarks from the literature. Our experiments indicate our techniques show promise on challenging verification tasks requiring non-linear reasoning.
more »
« less
This content will become publicly available on August 1, 2026
Designing 3D Anisotropic Frame Fields with Odeco Tensors
This paper introduces a method to synthesize a 3D tensor field within a constrained geometric domain represented as a tetrahedral mesh. Whereas previous techniques optimize forisotropicfields, we focus onanisotropictensor fields that are smooth and aligned with the domain boundary or user guidance. The key ingredient of our method is a novel computational design framework, built on top of thesymmetric orthogonally decomposable(odeco) tensor representation, to optimize the stretching ratios and orientations for each tensor in the domain. In contrast to past techniques designed only forisotropictensors, we demonstrate the efficacy of our approach in generating smooth volumetric tensor fields with highanisotropyand shape conformity, especially for the domain with complex shapes. We apply these anisotropic tensor fields to various applications, such as anisotropic meshing, structural mechanics, and fabrication.
more »
« less
- PAR ID:
- 10631404
- Publisher / Repository:
- ACM
- Date Published:
- Journal Name:
- ACM Transactions on Graphics
- Volume:
- 44
- Issue:
- 4
- ISSN:
- 0730-0301
- Page Range / eLocation ID:
- 1 to 14
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Hockett, Kevin Loren (Ed.)ABSTRACT Rhizopus microsporusis a necrotrophic post-harvest pathogen that causes significant economic losses in the agricultural sector. To explore alternatives to conventional management strategies for the mitigation of post-harvest infections, we investigated the potential of two previously identified endophyticBacillus velezensisstrains as biological control agents. Throughin vitroandin vivoexperiments, we examined the mechanisms of biocontrol displayed by twoB. velezensisstrains (KV10 and KV15) against threeR. microsporusstrains (W2-50, W2-51, and W2-58).In vitroassays assessed co-cultivability and the inhibitory effects ofB. velezensisagainstR. microsporus. The results demonstrated strain-specific antifungal activity with a reduction in fungal growth across treatments. Further analysis revealed that volatile organic compounds produced byB. velezensiscontributed to its antifungal properties. To evaluate the biocontrol efficacyin vivo, tomato fruits were inoculated withR. microsporusand subsequently treated withB. velezensis. The results support the strain-specific reduction in tomato spoilage, yielding various spoilage rates observed across treatments. Our findings highlight the potential ofB. velezensisas a promising biocontrol agent for the management ofR. microsporuspost-harvest infections in tomatoes. Further research is warranted to optimize the applicationof B. velezensisas a sustainable and environmentally friendly approach for controlling post-harvest diseases in tomatoes.IMPORTANCEOur study shows the significance of improving sustainable agriculture by offering an alternative to the use of chemical fungicides in post-harvest applications. Opportunistic fungal pathogens likeRhizopus microsporuscan have detrimental effects on post-harvest commodities like tomatoes. Post-harvest fungal infections are mainly controlled by chemical fungicides that pose health risks to humans and the environment. Utilizing biocontrol agents provides an environmentally safe alternative. Understanding the mechanisms of biocontrol employed by beneficial bacteria likeBacillus velezensison fungal pathogens gives insight into safer, more environmentally friendly alternatives to protect food crops. Our results suggest that targeted microbial solutions can mitigate post-harvest losses.more » « less
-
This paper is about semantic regular expressions (SemREs). This is a concept that was recently proposed by Smore (Chen et al. 2023) in which classical regular expressions are extended with a primitive to query external oracles such as databases and large language models (LLMs). SemREs can be used to identify lines of text containing references to semantic concepts such as cities, celebrities, political entities, etc. The focus in their paper was on automatically synthesizing semantic regular expressions from positive and negative examples. In this paper, we study themembership testing problem. First, we present a two-pass NFA-based algorithm to determine whether a stringwmatches a SemRErinO(|r|2|w|2+ |r| |w|3) time, assuming the oracle responds to each query in unit time. In common situations, where oracle queries are not nested, we show that this procedure runs inO(|r|2|w|2) time. Experiments with a prototype implementation of this algorithm validate our theoretical analysis, and show that the procedure massively outperforms a dynamic programming-based baseline, and incurs a ≈ 2 × overhead over the time needed for interaction with the oracle. Second, we establish connections between SemRE membership testing and the triangle finding problem from graph theory, which suggest that developing algorithms which are simultaneously practical and asymptotically faster might be challenging. Furthermore, algorithms for classical regular expressions primarily aim to optimize their time and memory consumption. In contrast, an important consideration in our setting is to minimize the cost of invoking the oracle. We demonstrate an Ω(|w|2) lower bound on the number of oracle queries necessary to make this determination.more » « less
-
We propose a new synthesis algorithm that canefficientlysearch programs withlocalvariables (e.g., those introduced by lambdas). Prior bottom-up synthesis algorithms are not able to evaluate programs withfree local variables, and therefore cannot effectively reduce the search space of such programs (e.g., using standard observational equivalence reduction techniques), making synthesis slow. Our algorithm can reduce the space of programs with local variables. The key idea, dubbedlifted interpretation, is to lift up the program interpretation process, from evaluating one program at a time to simultaneously evaluating all programs from a grammar. Lifted interpretation provides a mechanism to systematically enumerate all binding contexts for local variables, thereby enabling us to evaluate and reduce the space of programs with local variables. Our ideas are instantiated in the domain of web automation. The resulting tool,Arborist, can automate a significantly broader range of challenging tasks more efficiently than state-of-the-art techniques includingWebRobotand Helena.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
