An official website of the United States government
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
This content will become publicly available on June 17, 2026
HotStuff-1: Linear Consensus with One-Phase Speculation
This paper introduces HotStuff-1, a BFT consensus protocol that improves the latency of HotStuff-1 by two network hops while maintaining linear communication complexity against faults. Furthermore, HotStuff-1 incorporates an incentive-compatible leader rotation design that motivates leaders to propose transactions promptly. HotStuff-1 achieves a reduction of two network hops byspeculativelysending clients early finality confirmations, after one phase of the protocol. Introducing speculation into streamlined protocols is challenging because, unlike stable-leader protocols, these protocols cannot stop the consensus and recover from failures. Thus, we identifyprefix speculation dilemmain the context of streamlined protocols; HotStuff-1 is the first streamlined protocol to resolve it. HotStuff-1 embodies an additional mechanism,slotting, that thwarts delays caused by (1) rationally-incentivized leaders and (2) malicious leaders inclined to sabotage others' progress. The slotting mechanism allows leaders to dynamically drive as many decisions as allowed by network transmission delays before view timers expire, thus mitigating both threats.
more »
« less
- Award ID(s):
- 2245373
- PAR ID:
- 10611624
- Publisher / Repository:
- ACM
- Date Published:
- Journal Name:
- Proceedings of the ACM on Management of Data
- Volume:
- 3
- Issue:
- 3
- ISSN:
- 2836-6573
- Page Range / eLocation ID:
- 1 to 29
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Böhme, Rainer; Kiffer, Lucianna (Ed.)We consider the problem of secret leader election with accountability. Secret leader election protocols counter adaptive adversaries by keeping the identities of elected leaders secret until they choose to reveal themselves, but in existing protocols this means it is impossible to determine who was elected leader if they fail to act. This opens the door to undetectable withholding attacks, where leaders fail to act in order to slow the protocol or bias future elections in their favor. We formally define accountability (in weak and strong variants) for secret leader election protocols. We present three paradigms for adding accountability, using delay-based cryptography, enforced key revelation, or threshold committees, all of which ensure that after some time delay the result of the election becomes public. The paradigm can be chosen to balance trust assumptions, protocol efficiency, and the length of the delay before leaders are revealed. Along the way, we introduce several new cryptographic tools including re-randomizable timed commitments and timed VRFs.more » « less
-
ABSTRACT ObjectiveInflammation may be an integral physiological mechanism through which discrimination impacts cardiovascular health and contributes to racial health disparities. Limited research has examined psychosocial factors that protect against the negative effects of discrimination on inflammation. Perceived control is a promising possible protective factor, given that it has been shown to moderate the relationship between other psychosocial stressors and physiological outcomes. This study thus tested whether systemic inflammation mediated the link between discrimination and cardiovascular health and whether perceived control moderated this relationship. MethodsData for this project included 347 non-Hispanic/Latinx Black adults (mean [standard deviation] age = 51.64 [11.24] years; 33% female) taken from the Midlife in the United States study. Perceived control and daily discrimination were assessed via self-report, and inflammation was measured via circulating levels of C-reactive protein (CRP), interleukin-6 (IL-6), fibrinogen, and tumor necrosis factor α. Cardiovascular health was measured by morbidity of cardiovascular conditions: heart disease, hypertension, and/or stroke. ResultsCRP (indirect effect:b =0.004, 95% confidence interval [CI] = 0.001–0.007) and fibrinogen (indirect effect:b =0.002, 95% CI = 0.0003–0.005) mediated the link between discrimination and cardiovascular conditions. Perceived control moderated the relationship between discrimination and CRP (F(1, 293) = 4.58, ΔR2= 0.013,b= −0.02, SE = 0.01,p= .033). CRP mediated the link between discrimination and cardiovascular conditions only for those who reported low levels of perceived control (Index = −0.003, 95% CI = −0.007 to −0.0001). ConclusionFindings provide empirical evidence of inflammation as a mechanism linking discrimination to cardiovascular conditions among Black Americans. Additionally, perceived control may be protective. Findings could suggest beliefs about control as a potential intervention target to help reduce the negative effects of discrimination on cardiovascular health among Black Americans.more » « less
-
Blockchains operating at the global scale demand high-performance byzantine fault-tolerant (BFT) consensus protocols. Most classic PBFT-like protocols suffer from an issue known as the leader bottleneck, which severely limits their throughput and resource utilization. Recently, Directed Acyclic Graph, or DAG-based protocols, have emerged as a promising approach for eliminating the leader bottleneck and achieving better performance. They attain higher throughput by separating data dissemination and block ordering. However, their safety and liveness logic is also significantly more elaborate. So far, most DAG-based protocols have only enjoyed on-paper security proofs, and it is not clear how to construct formal proofs of these protocols efficiently. We introduce LiDO-DAG, a concurrent object model that abstracts the common logic of these protocols. LiDO-DAG is constructed by combining a DAG abstraction and LiDO, a recently proposed abstraction for leader-based consensus. To demonstrate that our framework enables rapid validation of new DAG-based protocol designs, we implemented LiDO-DAG in Coq and applied it to three recent DAG-based protocols, including Narwhal, Bullshark, and Sailfish. Our framework readily yields mechanized safety and liveness proofs for all three protocols, which are also the first mechanized liveness proofs of any DAG-based protocol. Our framework has also revealed an optimization for Sailfish that improves its worst-case latency.more » « less
-
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
