Abstract Mutexes are fundamental synchronization primitives in concurrent programming, but their improper use can lead to deadlocks. Conventional assume-based modeling abstracts mutex semantics via assumptions, simplifying safety verification but hindering deadlock verification. Although prior efforts have aimed to address this limitation, we show that state-of-the-art methods remain inaccurate. In this paper, we propose a novel modeling approach that captures mutex semantics using ordering constraints, enabling accurate deadlock verification within partial-order-based concurrent verification frameworks. We formally prove the correctness of our method and implement it in a prototype tool, Deagle-DL . We evaluate Deagle-DL against a state-of-the-art bounded model checker ESBMC that employs the conventional modeling approach, and a state-of-the-art static analysis tool for deadlock detection. Our experiments show that Deagle-DL significantly outperforms both tools in terms of precision, while maintaining substantial efficiency.

Abstract SMT solving with ordering consistency theory achieves state-of-the-art efficiency in bounded model checking of concurrent programs. At its core is a dedicated theory solver that derives the write-serialization (WS) and from-read (FR) orders on the fly, thereby allowing their explicit encodings to be omitted. Additionally, the solver is equipped with preventive propagation , which proactively eliminates theory-level conflicts. This work presents a refined ordering consistency theory that overcomes two existing limitations. First, we address the weak SC problem , where the solver may fail to reconstruct a total WS order and thus admit executions weaker than Sequential Consistency. We identify the core reason as insufficient constraints on WS totality. As a solution, we restore the WS encodings to ensure its totality, while preserving WS derivation to curb the resulting growth in the search space. Second, the existing framework for preventive propagation does not support WS variables or atomicity constraints. We extend it to incorporate these elements, yielding a more general and principled propagation mechanism. Experiments show that our approach soundly prevents weak-SC behaviors, enables effective propagation, and maintains competitive overall performance.

High-precision control of constrained robot manipulators under uncertainties remains a fundamental challenge. While conventional nonlinear model predictive control (NMPC) often struggles with real-time requirements due to its heavy computational burden, linear MPC (LMPC) typically relies on terminal invariant sets that are often computationally intractable for complex nonlinear systems. To address these limitations, this paper proposes a computationally efficient data-driven linear model predictive control (DLMPC) framework that achieves control accuracy comparable to NMPC while ensuring real-time performance. A variable-length sliding-window dynamic mode decomposition with control (DMDc) method is developed to identify a time-varying local affine model from recent input–output data, enabling accurate linearization under uncertainties. Based on this model, a novel time-varying terminal constraint is designed to substitute the conventional terminal set, thereby obviating the need for uncertainty upper bounds that are difficult to obtain in practice. The recursive feasibility and stability of the proposed framework are established using Lyapunov stability theory. Finally, experimental results on a Franka Emika Panda robot demonstrate the effectiveness and superior performance of the proposed method.

In recent years, reinforcement learning has been widely applied in the field of games. However, most studies focus on assisting agents to achieve victory, with less attention paid to whether the agents exhibit human-like characteristics. In order to build human-like agents with high performance, we propose a method for learning the strategies of human players in modern three-dimensional video games. Our method utilizes a hierarchical framework, learning basic behaviors and intentions of human players at the lower level through imitation learning, and generalized policies at the high level through reinforcement learning. Compared with other existing methods, our method demonstrates significant advantages in learning human-like strategies in complex environments.

Despite the rapid development of neural vocoders in recent years, they usually suffer from some intrinsic challenges like opaque modeling, and parameter-performance trade-off. In this study, we propose an innovative time-frequency (T-F) domain-based neural vocoder to resolve the above-mentioned challenges. To be specific, we bridge the connection between the classical signal range-null decomposition (RND) theory and vocoder task, and the reconstruction of target spectrogram can be decomposed into the superimposition between the range-space and null-space, where the former is enabled by a linear domain shift from the original mel-scale domain to the target linear-scale domain, and the latter is instantiated via a learnable network for further spectral detail generation. Accordingly, we propose a novel dual-path framework, where the spectrum is hierarchically encoded/decoded, and the cross- and narrow-band modules are elaborately devised for efficient sub-band and sequential modeling. Comprehensive experiments are conducted on the LJSpeech and LibriTTS benchmarks. Quantitative and qualitative results show that while enjoying lightweight network parameters, the proposed approach yields state-of-the-art performance among existing advanced methods. Our code and the pretrained model weights are available at https://github.com/Andong-Li-speech/RNDVoC.

Although neural network-based speech enhancement models perform much better than their traditional counterparts, their substantial computational demands make it challenging for real-time applications on edge devices. Moreover, compact models often exhibit weak generalization in complex and out-of-domain scenarios. In this paper, we propose an efficient model based on our previous work Split-and-Merge Recurrent-based UNet (SMRU). The proposed model achieves a significant reduction in computational load through the incorporation of Skip-RNN layers and an attention-based sub-band compression module. Moreover, the employment of a two-stage uncertainty-driven loss function for aleatoric uncertainty capture leads to enhanced generalization and denoising performance without increasing the computational complexity during inference. Experimental results demonstrate that our model not only surpasses the original SMRU but also outperforms recently proposed lightweight models with similar computational cost (approximately 200M MACs). Furthermore, our model exhibits strong generalization in cross-corpus test sets, making it a promising solution for real-time speech enhancement applications.

The proliferation of deep neural networks has spawned the rapid development of acoustic echo cancellation and noise suppression, and plenty of prior arts have been proposed, which yield promising performance. Nevertheless, they rarely consider the deployment generality in different processing scenarios, such as edge devices, and cloud processing. To this end, this paper proposes a general model, termed SMRU, to cover different application scenarios. The novelty lies in two-fold. First, a multi-scale band split layer and band merge layer are proposed to effectively fuse local frequency bands for lower complexity modeling. Besides, by simulating the multi-resolution feature modeling characteristic of the classical UNet structure, a novel recurrent-dominated UNet is devised. It consists of multiple variable frame rate blocks, each of which involves the causal time down-/upsampling layer with varying compression ratios and the dualpath structure for inter- and intra-band modeling. The model is configured from $50 \mathrm{M} / \mathrm{s}$ to $6.8 \mathrm{G} / \mathrm{s}$ in terms of MACs, and the experimental results show that the proposed approach yields competitive or even better performance over existing baselines, and has the full potential to adapt to more general scenarios with varying complexity requirements.

Automatically verifying multi-threaded programs is difficult because of the vast number of thread interleavings, a problem aggravated by weak memory consistency. Partial orders can help with verification because they can represent many thread interleavings concisely. However, there is no dedicated decision procedure for solving partial-order constraints. In this article, we propose a novel ordering consistency theory for concurrent program verification that is applicable not only under sequential consistency, but also under the TSO and PSO weak memory models. We further develop an efficient theory solver, which checks consistency incrementally, generates minimal conflict clauses, and includes a custom propagation procedure. We have implemented our approach in a tool, called Zord , and have conducted extensive experiments on the SV-COMP 2020 ConcurrencySafety benchmarks. Our experimental results show a significant improvement over the state-of-the-art.

Abstract is an SMT-based multi-threaded program verification tool. It is built on top of (front-end) and (back-end). The basic idea of is to integrate into the SMT solver an ordering consistency theory that handles ordering relations over the shared variable accesses in the program. The front-end encodes the input program into an extended propositional formula that contains ordering constraints. The back-end is reinforced with a solver for the ordering consistency theory. This paper presents the basic idea, architecture, installation, and usage of .

The happens-before orders have been widely adopted to model thread interleaving behaviors of concurrent programs. A dedicated ordering theory solver, usually composed of theory propagation, consistency checking, and conflict clause generation, plays a central role in concurrent program verification. We propose a novel preventive reasoning approach that automatically preserves the ordering consistency and makes consistency checking and conflict clause generation omissible. We implement our approach in a prototype tool and conduct experiments on credible benchmarks; results reveal a significant improvement over existing state-of-the-art concurrent program verifiers.

Analyzing multi-threaded programs is hard due to the number of thread interleavings. Partial orders can be used for modeling and analyzing multi-threaded programs. However, there is no dedicated decision procedure for solving partial-order constraints. In this paper, we propose a novel ordering consistency theory for multi-threaded program verification under sequential consistency, and we elaborate its theory solver, which realizes incremental consistency checking, minimal conflict clause generation, and specialized theory propagation to improve the efficiency of SMT solving. We conducted extensive experiments on credible benchmarks; the results show significant promotion of our approach.