arXiv subjects

Xiong Xu

Publications and source records attributed to Xiong Xu.

15 recordsLinked to original sources

arXiv2026

Magnetic proximity-induced non-relativistic valley polarization

The magnetic proximity effect in van der Waals heterostructures exerts a significant impact on the properties of adjacent materials. Here, we propose van der Waals heterostructures composed of monolayers ferromagnets (FM) and altermagnets (AM), in which the magnetic proximity effect from the FM induces pronounced non-relativistic valley polarization in the AM, and this phenomenon is demonstrated to be universal. Furthermore, by tuning the magnetization of the FM and the N\'eel vector direction of the AM, four independent valley-polarized states can be realized in the FM/AM heterostructures, exhibiting strong magnetic-valley coupling. These findings suggest that FM/AM heterostructures hold potential application value in the field of valleytronics-based information storage.

cond-mat.mtrl-sci↗

arXiv2026

Fully compensated and uncompensated ferrimagnetic ferrovalley semiconductors

Altermagnets (AMs) and fully compensated ferrimagnets (FC-FIMs) are emerging classes of magnetic materials that combine the advantages of antiferromagnets and ferromagnets. Here, we elucidate the mechanism behind the uniaxial strain-driven transformation from AM to FC-FIM and find that the accompanying non-relativistic valley polarization is positively correlated with the net magnetic moment between magnetic atoms in opposite spin sublattices. We then propose an uncompensated ferrimagnetic monolayer VCrSeTeO to achieve large intrinsic valley polarization. Spin-orbit coupling (SOC) is shown to further increase the valley polarization to over 400 meV under uniaxial strains and the reason is explained in terms of SOC perturbation theorem. Furthermore, we reveal a distinctive anomalous valley Hall effect in which the valley Hall voltage is reversed within the same valley in ferrimagnet VCrSeTeO. This work proposes a strategy for realizing giant valley polarization and provides theoretical guidance for the application of ferrimagnetic ferrovalley semiconductors derived from altermagnets in valleytronics.

cond-mat.mtrl-sci↗

arXiv2026

Realizing giant valley polarization effect based on monolayer altermagnets

Stable and remarkable valley polarization effect is the key to utilizing valley degree of freedom in valleytronic devices. According to first-principles calculations and symmetry analysis, we reveal that valley polarization effect in monolayer V2Se2O altermagnet is correlated with the net magnetic moment between magnetic V atoms under uniaxial strain, thereby proposing two strategies for achieving giant valley polarization effect. Firstly, substituting one V atom in V2Se2O with Cr to construct a ferrimagnetic monolayer VCrSe2O enhances the net magnetic moment between magnetic atoms, thereby realizing a giant valley polarization effect. Applying uniaxial strain along either the a-axis or b-axis significantly increases the value of valley polarization, which exhibits a nearly linear relationship with the net magnetic moments between the magnetic atoms. Secondly, constructing a van der Waals heterostructure composed of V2Se2O and α-SnO monolayers breaks mirror symmetry, thereby inducing a net magnetic moment, which in turn causes a remarkable valley polarization effect. Compressing the interlayer distance of the heterostructure can increase the net magnetic moment between V atoms, then enhancing the value of valley polarization to nearly 400 meV. This work reveals that valley polarization in monolayer altermagnet is correlated with the net magnetic moment between magnetic atoms. Finally, we propose two strategies to achieve giant valley polarization based on monolayer altermagnets, providing theoretical guidance for the potential applications of ferrimagnetic monolayers and altermagnet-based heterostructures in valleytronics.

cond-mat.mtrl-sci↗

arXiv2026

Integrating Symbolic Execution with LLMs for Automated Generation of Program Specifications

Automatically generating formal specifications including loop invariants, preconditions, and postconditions for legacy code is critical for program understanding, reuse and verification. However, the inherent complexity of control and data structures in programs makes this task particularly challenging. This paper presents a novel framework that integrates symbolic execution with large language models (LLMs) to automatically synthesize formally verified program specifications. Our method first employs symbolic execution to derive precise strongest postconditions for loop-free code segments. These symbolic execution results, along with automatically generated invariant templates, then guide the LLM to propose and iteratively refine loop invariants until a correct specification is obtained. The template-guided generation process robustly combines symbolic inference with LLM reasoning, significantly reducing hallucinations and syntactic errors by structurally constraining the LLM's output space. Furthermore, our approach can produce strong specifications without relying on externally provided verification goals, enabled by the rich semantic context supplied by symbolic execution, overcoming a key limitation of prior goal-dependent tools. Extensive evaluation shows that our tool SESpec outperforms the existing state-of-the-art tools across numerical and data-structure benchmarks, demonstrating both high precision and broad applicability.

cs.SE↗

arXiv2026

MAFNet:Multi-frequency Adaptive Fusion Network for Real-time Stereo Matching

Existing stereo matching networks typically rely on either cost-volume construction based on 3D convolutions or deformation methods based on iterative optimization. The former incurs significant computational overhead during cost aggregation, whereas the latter often lacks the ability to model non-local contextual information. These methods exhibit poor compatibility on resource-constrained mobile devices, limiting their deployment in real-time applications. To address this, we propose a Multi-frequency Adaptive Fusion Network (MAFNet), which can produce high-quality disparity maps using only efficient 2D convolutions. Specifically, we design an adaptive frequency-domain filtering attention module that decomposes the full cost volume into high-frequency and low-frequency volumes, performing frequency-aware feature aggregation separately. Subsequently, we introduce a Linformer-based low-rank attention mechanism to adaptively fuse high- and low-frequency information, yielding more robust disparity estimation. Extensive experiments demonstrate that the proposed MAFNet significantly outperforms existing real-time methods on public datasets such as Scene Flow and KITTI 2015, showing a favorable balance between accuracy and real-time performance.

cs.CV↗

arXiv2025

DTVM: Revolutionizing Smart Contract Execution with Determinism and Compatibility

We introduce the DeTerministic Virtual Machine (DTVM) Stack, a next-generation smart contract execution framework designed to address critical performance, determinism, and ecosystem compatibility challenges in blockchain networks. Building upon WebAssembly (Wasm) while maintaining full Ethereum Virtual Machine (EVM) ABI compatibility, DTVM introduces a Deterministic Middle Intermediate Representation (dMIR) and a hybrid lazy-JIT compilation engine to balance compilation speed and execution efficiency. DTVM further accommodates diverse instruction set architectures (e.g., EVM, RISC-V) through modular adaptation layers. This enables seamless integration with DTVM's hybrid lazy-JIT compilation engine, which dynamically optimizes performance while preserving deterministic execution guarantees across heterogeneous environments. The key contributions including: 1). The framework achieves up to 2$\times$ acceleration over evmone in dominant Ethereum contract (e.g. ERC20/721/1155) execution and reduces fibonacci computation latency by 11.8$\sim$40.5% compared to Wasm based VMs. 2). A novel trampoline hot-switch mechanism enables sub-millisecond (0.95ms) post-deployment invocation times, outperforming up to about 23$\times$ in compilation and invocation efficiency. 3). It supports multi-language development (Solidity, C++, Rust, Java, Go, and AssemblyScript) through unified bytecode conversion while maintaining EVM ABI compatibility for seamless invocation. It reduces machine code object sizes by 30.0$\sim$72.6%, coupled with a minimized Trusted Computing Base. 4). It offers SmartCogent, an AI-driven full-stack development experience, leveraging fine-tuned LLMs and retrieval-augmented generation to automate tasks across the smart contract lifecycle: development, debugging, security auditing, and deployment. DTVM Stack has been open-sourced (https://github.com/DTVMStack).

cs.DC↗

arXiv2025

HpC: A Calculus for Hybrid and Mobile Systems -- Full Version

Networked cybernetic and physical systems of the Internet of Things (IoT) immerse civilian and industrial infrastructures into an interconnected and dynamic web of hybrid and mobile devices. The key feature of such systems is the hybrid and tight coupling of mobile and pervasive discrete communications in a continuously evolving environment (discrete computations with predominant continuous dynamics). In the aim of ensuring the correctness and reliability of such heterogeneous infrastructures, we introduce the hybrid π-calculus (HpC), to formally capture both mobility, pervasiveness and hybridisation in infrastructures where the network topology and its communicating entities evolve continuously in the physical world. The π-calculus proposed by Robin Milner et al. is a process calculus that can model mobile communications and computations in a very elegant manner. The HpC we propose is a conservative extension of the classical π-calculus, i.e., the extension is ``minimal'', and yet describes mobility, time and physics of systems, while allowing to lift all theoretical results (e.g. bisimulation) to the context of that extension. We showcase the HpC by considering a realistic handover protocol among mobile devices.

cs.PL↗

arXiv2024

Piezovalley effect and magnetovalley coupling in altermagnetic semiconductors

Clarifying the physical origin of valley polarization and exploring promising ferrovalley materials are conducive to the application of valley degrees of freedom in the field of information storage. Here, we explore two novel altermagnetic semiconductors (monolayers Nb2Se2O and Nb2SeTeO) with Néel temperature above room temperature based on first-principles calculations. It reveals that uniaxial strain induces valley polarization without spin-orbital coupling (SOC) in altermagnets owing to the piezovalley effect, while uniaxial compressive strain transforms the intrinsic ferrovalley semiconductor into a semimetal, half metal and metal. Moreover, moderate biaxial strain renders Janus monolayer Nb2SeTeO to robust Dirac-like band dispersion. The SOC and intrinsic in-plane magnetocrystalline anisotropy energy induce Dirac-like altermagnets to generate apparent valley polarization through magnetovalley coupling. In terms of SOC perturbation, we elucidate the physical mechanism behind in-plane-magnetization induced valley polarization and demonstrate the magnitude of valley polarization is positively correlated with the square of SOC strength and negatively correlated with the bandgap. The present work reveals the physical origin of valley polarization in altermagnets and expands the application of ferrovalley at room temperature in valleytronics.

cond-mat.mtrl-sci↗

arXiv2024

Mars 2.0: A Toolchain for Modeling, Analysis, Verification and Code Generation of Cyber-Physical Systems

We introduce Mars 2.0 for modeling, analysis, verification and code generation of Cyber-Physical Systems. Mars 2.0 integrates Mars 1.0 with several important extensions and improvements, allowing the design of cyber-physical systems using the combination of AADL and Simulink/Stateflow, which provide a unified graphical framework for modeling the functionality, physicality and architecture of the system to be developed. For a safety-critical system, formal analysis and verification of its combined AADL and Simulink/Stateflow model can be conducted via the following steps. First, the toolchain automatically translates AADL and Simulink/Stateflow models into Hybrid CSP (HCSP), an extension of CSP for formally modeling hybrid systems. Second, the HCSP processes can be simulated using the HCSP simulator, and to complement incomplete simulation, they can be verified using the Hybrid Hoare Logic prover in Isabelle/HOL, as well as the more automated HHLPy prover. Finally, implementations in SystemC or C can be automatically generated from the verified HCSP processes. The transformation from AADL and Simulink/Stateflow to HCSP, and the one from HCSP to SystemC or C, are both guaranteed to be correct with formal proofs. This approach allows model-driven design of safety-critical cyber-physical systems based on graphical and formal models and proven-correct translation procedures. We demonstrate the use of the toolchain on several benchmarks of varying complexity, including several industrial-sized examples.

cs.PL↗

arXiv2024

Formally Verified C Code Generation from Hybrid Communicating Sequential Processes

Hybrid Communicating Sequential Processes (HCSP) is a formal model for hybrid systems, including primitives for evolution along an ordinary differential equation (ODE), communication, and parallel composition. Code generation is needed to convert HCSP models into code that can be executed in practice, and the correctness of this conversion is essential to ensure that the generated code accurately reflects the formal model. In this paper, we propose a code generation algorithm from HCSP to C with POSIX library for concurrency. The main difficulties include how to bridge the gap between the synchronized communication model in HCSP and the use of mutexes for synchronization in C, and how to discretize evolution along ODEs and support interrupt of ODE evolution by communication. To prove the correctness of code generation, we define a formal semantics for POSIX C, and build transition system models for both HCSP and C programs. We then define an approximate bisimulation relation between traces of transition systems, and show that under certain robustness conditions for HCSP, the generated C program is approximately bisimilar to the original model. Finally, we evaluate the code generation algorithm on a detailed model for automatic cruise control, showing its utility on real-world examples.

cs.PL↗

arXiv2023

Session Types With Multiple Senders Single Receiver (report version)

Message passing is a fundamental element in software development, ranging from concurrent and mobile computing to distributed services, but it suffers from communication errors such as deadlocks. Session types are a typing discipline for enforcing safe structured interactions between multiple participants. However, each typed interaction is restricted to having one fixed sender and one fixed receiver. In this paper, we extend session types with existential branching types, to handle a common interaction pattern with multiple senders and a single receiver in a synchronized setting, i.e. a receiver is available to receive messages from multiple senders, and which sender actually participates in the interaction cannot be determined till execution. We build the type system with existential branching types, which retain the important properties induced by standard session types: type safety, progress (i.e. deadlock-freedom), and fidelity. We further provide a novel communication type system to guarantee progress of dynamically interleaved multiparty sessions, by abandoning the strong restrictions of existing type systems. Finally, we encode Rust multi-thread primitives in the extended session types to show its expressivity, which can be considered as an attempt to check the deadlock-freedom of Rust multi-thread programs.

cs.PL↗

arXiv2023

Perceptual MAE for Image Manipulation Localization: A High-level Vision Learner Focusing on Low-level Features

Nowadays, multimedia forensics faces unprecedented challenges due to the rapid advancement of multimedia generation technology thereby making Image Manipulation Localization (IML) crucial in the pursuit of truth. The key to IML lies in revealing the artifacts or inconsistencies between the tampered and authentic areas, which are evident under pixel-level features. Consequently, existing studies treat IML as a low-level vision task, focusing on allocating tampered masks by crafting pixel-level features such as image RGB noises, edge signals, or high-frequency features. However, in practice, tampering commonly occurs at the object level, and different classes of objects have varying likelihoods of becoming targets of tampering. Therefore, object semantics are also vital in identifying the tampered areas in addition to pixel-level features. This necessitates IML models to carry out a semantic understanding of the entire image. In this paper, we reformulate the IML task as a high-level vision task that greatly benefits from low-level features. Based on such an interpretation, we propose a method to enhance the Masked Autoencoder (MAE) by incorporating high-resolution inputs and a perceptual loss supervision module, which is termed Perceptual MAE (PMAE). While MAE has demonstrated an impressive understanding of object semantics, PMAE can also compensate for low-level semantics with our proposed enhancements. Evidenced by extensive experiments, this paradigm effectively unites the low-level and high-level features of the IML task and outperforms state-of-the-art tampering localization methods on all five publicly available datasets.

cs.CV↗

arXiv2021

Rapid and Unconditional Parametric Reset Protocol for Tunable Superconducting Qubits

Qubit initialization is a critical task in quantum computation and communication. Extensive efforts have been made to achieve this with high speed, efficiency and scalability. However, previous approaches have either been measurement-based and required fast feedback, suffered from crosstalk or required sophisticated calibration. Here, we report a fast and high-fidelity reset scheme, avoiding the issues above without any additional chip architecture. By modulating the flux through a transmon qubit, we realize a swap between the qubit and its readout resonator that suppresses the excited state population to 0.08% $\pm$ 0.08% within 34 ns (284 ns if photon depletion of the resonator is required). Furthermore, our approach (i) can achieve effective second excited state depletion, (ii) has negligible effects on neighbouring qubits, and (iii) offers a way to entangle the qubit with an itinerant single photon, useful in quantum communication applications.

quant-ph↗

arXiv2019

The reduction of entropy uncertainty for qutrit system under non-Markov noisy environment

In this paper, we explore the entropy uncertainty for qutrit system under non-Markov noisy environment and discuss the effects of the quantum memory system and the spontaneously generated interference (SGI) on the entropy uncertainty in detail. The results show that, the entropy uncertainty can be reduced by using the methods of quantum memory system and adjusting of SGI. Particularly, the entropy uncertainty can be decreased obviously when both the quantum memory system and the SGI are simultaneously applied.

quant-ph↗

arXiv2019

A Message Passing Approach for Multiple Maneuvering Target Tracking

This paper considers the problem of detecting and tracking multiple maneuvering targets, which suffers from the intractable inference of high-dimensional latent variables that include target kinematic state, target visibility state, motion mode-model association, and data association. A unified message passing algorithm that combines belief propagation (BP) and mean-field (MF) approximation is proposed for simplifying the intractable inference. By assuming conjugate-exponential priors for target kinematic state, target visibility state, and motion mode-model association, the MF approximation decouples the joint inference of target kinematic state, target visibility state, motion mode-model association into individual low-dimensional inference, yielding simple message passing update equations. The BP is exploited to approximate the probabilities of data association events since it is compatible with hard constraints. Finally, the approximate posterior probability distributions are updated iteratively in a closed-loop manner, which is effective for dealing with the coupling issue between the estimations of target kinematic state and target visibility state and decisions on motion mode-model association and data association. The performance of the proposed algorithm is demonstrated by comparing with the well-known multiple maneuvering target tracking algorithms, including interacting multiple model joint probabilistic data association, interacting multiple model hypothesis-oriented multiple hypothesis tracker and multiple model generalized labeled multi-Bernoulli.

eess.SY↗