arXiv subjects

Hongfei Fu

Publications and source records attributed to Hongfei Fu.

At least 19 recordsLinked to original sources

arXiv2026

Efficient second-order physics-preserving schemes for incompressible flows with variable density and viscosity

This paper proposes a novel second-order prediction--filter--projection framework for incompressible flows with variable density and viscosity. In this framework, a constrained $L^2$-projection is enforced to unconditionally preserve the prescribed density bounds and discrete mass conservation, while a generalized-Laplacian reformulation combined with the D-CSAV approach is used to discretize the variable-viscosity momentum equation. In particular, a density-weighted second-order time filter is proposed, which eliminates the additional uniform-in-time bound restriction imposed on the time difference quotient of the discrete density in existing stability analyses. The resulting scheme is shown to satisfy an unconditional modified-energy dissipation law, without the viscosity-related restrictions imposed in earlier work. Then, an additional scalar auxiliary variable and its compatible temporal discretization are introduced to construct a variable-step prediction--filter--projection scheme. This scheme is also bound-preserving and mass-conserving, and satisfies an unconditional modified-energy dissipation law. Moreover, the modified energy is much closer to the ``original'' kinetic energy, differing from it only through the auxiliary-variable corrections. Based on the variable-step scheme, a reliable energy-based adaptive time-stepping strategy is developed. Finally, numerical experiments demonstrate the accuracy, physics-preserving properties, and efficiency of the proposed schemes.

math.NA↗

arXiv2026

Bound-preserving and mass-conserving projection BCFD methods for incompressible miscible displacement in porous media

In this paper, we propose and analyze two novel structure-preserving projection schemes for the incompressible miscible displacement problem in porous media. These schemes are specifically designed to preserve two essential physical properties--concentration bounds and the mass balance identity, and are accompanied by a rigorous error analysis for the projection approach. Both schemes are second-order accurate in space but differ in temporal accuracy: one is first-order and the other is second-order. Methodologically, both schemes comprise a prediction step for the concentration variable, based on a second-order modified upwind discretization together with an implicit-explicit finite difference approximation, followed by a projection (or correction) step that enforces the desired physical constraints, namely bounds and mass conservation. For the first-order temporal scheme, the velocity and pressure are solved at the first step on staggered spatial grids with explicit treatment of concentration. In contrast, for the second-order scheme, to ensure well-posedness and to suppress non-physical oscillations in the simulation, the velocity and pressure are solved at the final step with the concentration treated implicitly. A rigorous numerical theoretical framework is established for the first-order scheme, encompassing optimal-order error estimates, stability, and proofs of the existence and uniqueness of the numerical solutions. The numerical analysis framework is further extended to the more involved second-order scheme, and the corresponding theoretical results are briefly outlined. Finally, numerical examples, including some 'real' simulations, are presented to verify the theoretical findings and demonstrate the strong performance of the proposed schemes. In particular, the occurrence of viscous fingering is successfully captured and confirmed by the numerical results.

math.NA↗

arXiv2026

Staged Multi-step UTXO Workflows via Recursive Invariants

Stateless UTXO-style execution validates transactions from local and referenced data, supporting parallel validation and predictable serialized-size/weight accounting, but multi-step workflows must explicitly thread state through outputs. However, a prepared next-step transaction may become stale when another valid spend confirms first, shifting consistency maintenance, off-chain tracking, and transaction rebuilding to the protocol boundary and potentially increasing coordination cost and latency. Explicitly addressing this gap, recursive invariants (RIs) provide a transaction-level logic and toolchain in which workflow rules are predicates over a transaction's inputs and indexed successor positions referenced by the RI. Realizing such a successor causes the accepted transaction to re-check its predecessor's RI one step later, carrying the workflow rule forward without application-level shared mutable state or executable logic attached to outputs; repeated one-step checks thereby preserve validation-time locality and make validation work explicitly accountable. Many successor clauses are not decidable when the current transaction is validated, so our small statically typed DSL uses Kleene-style three-valued semantics over true, false, and unknown to defer future-dependent obligations until they become checkable. Alongside the DSL, we formalize UTXO validation and ledger extension in our model, identify the validation-time-evaluable one-step fragment, prove the deduction system sound for the three-valued semantics, and give corresponding transaction-validation and ledger-extension algorithms. Notably, a prototype RI interpreter and benchmarking toolchain evaluate six practice-motivated workflows; the reported traces show approximately linear cumulative validation-cost proxy growth while illustrating staged constraints without committing each step to a preconstructed successor transaction.

cs.CR↗

arXiv2026

Sharp Two-Round Adaptivity and Round Hierarchies for Semantic Regular Expressions

Semantic regular expressions (SemREs) attach external Boolean predicates to matched spans, making both the number and the sequentiality of oracle calls central resources. For a fixed expression and word, we represent membership by a polynomial-size monotone span circuit and identify optimal semantic evaluation with Boolean decision-tree evaluation. We determine the extremal power of adaptivity asymptotically sharply. For every $E\ge2$, there is a unary, star-free, semantic-depth-one instance of syntax size $Θ(E)$ with $E$ essential oracle keys and only unit-length semantic spans whose one-round cost is $E$, whereas its exact two-round and unrestricted deterministic costs are \[ \log_2 E+\tfrac12\log_2\log_2 E+O(1). \] Consequently, the largest nonadaptive-to-adaptive ratio is $(1+o(1))E/\log_2E$, including the optimal leading constant. A second restricted family exhibits a complete round hierarchy: its optimal $R$-round cost is $Θ(R E^{1/R})$. Thus the maximal gap already appears in two rounds, while other instances interpolate smoothly across all round budgets. Both constructions admit one-predicate realizations over the fixed alphabet $\{0,1,\#\}$ with logarithmic-length semantic spans and $O(E\log^2 E)$ total representation size. Under pointwise error $δ<1/2$ and worst-case expected cost, randomized nonadaptive complexity is exactly $(1-2δ)E$ for every instance with $E$ essential keys. Finally, for a fixed word $w$ and $h$ predicate names, the exact randomized minimax value is $(1-2δ)h sd(w)$, where $sd(w)$ counts distinct substring values; a span bound $s$ replaces $sd(w)$ by $sd_s(w)$. These results separate semantic information acquisition, parallel latency, and local symbolic matching cost.

cs.FL↗

arXiv2026

A linear, decoupled and positivity-preserving time-staggered block-centered finite difference method for the multi-species Keller-Segel chemotaxis system

In this paper, we present a linearly implicit, second-order block-centered finite difference (BCFD) prediction-then-projection scheme for the multi-species Keller-Segel chemotaxis system on non-uniform spatio-temporal grids. The proposed scheme integrates a standard Crank-Nicolson time-marching algorithm with an $L^2$ projection step to enforce positivity and mass conservation. The use of variable time stepsize and time-staggered discretization fully decouples the solutions of the multi-species cell density variables and the chemoattractant concentration variable while facilitating linearization, thereby greatly enhancing computational efficiency. Notably, the variable time-stepping algorithm and non-uniform grid BCFD discretization jointly enable adaptive resolution and local refinement near blow-up, thereby improving efficiency and accuracy without compromising the desired physical property-preserving in the simulation. Furthermore, using the mathematical induction method and the energy analysis approach, the unique solvability of the proposed scheme is rigorously proved, and we show that cell densities achieve second-order convergence in both time and space in the discrete $L^2$ norm, while the chemoattractant concentration achieves second-order convergence in the discrete $H^1$ norm. Representative numerical experiments are presented to validate the theoretical findings and demonstrate the reliability of the proposed scheme in simulating the blow-up phenomenon.

math.NA↗

arXiv2026

EconCSLib: A Lean Library for Computational Economics and AI-Assisted Research

Mathematical formalization uses interactive theorem provers to turn informal mathematical statements into machine-checkable artifacts. The success of mathlib, a large collaborative library for Lean, illustrates the potential of this approach. Recent progress in AI-assisted programming and theorem proving is also making large-scale formalization more practical. This paper presents EconCSLib, an early Lean 4 library for computational economics, as both infrastructure and a case study for AI-assisted formalization. The library aims to provide reusable definitions and theorems for game theory, mechanism design, social choice, and related areas. Beyond verified proofs of existing results, the library also aims to host machine-checked open problems and formalization of modern research papers. We discuss the design principles behind the library, the lessons learned from its development, and future directions for AI-assisted formalization in computational economics.

cs.GT↗

arXiv2026

Synthesizing Best Abstract Transformers via Parallel Bit-Vector Optimization

Abstract interpretation provides a principled foundation for constructing sound static analyses through systematic abstraction. A central challenge is synthesizing the best abstract transformers that achieve optimal precision within a given abstract domain. This paper addresses this problem for low-level code modeled with fixed-size bit-vectors. Recent approaches formulate the synthesis task as a multi-objective Optimization Modulo Theories (OMT) problem, but suffer from limited scalability. We introduce Spear, a parallel synthesis framework that exploits a key structural insight: while the bits within each objective must be processed sequentially, the objectives themselves are independent. Spear leverages the independence of inter-objective bits to better parallelize the synthesis. Experimental results on benchmarks across two binary analysis domains show that Spear consistently outperforms state-of-the-art OMT solvers, solving more instances and achieving significantly improved runtimes. To our knowledge, this is the first approach to apply parallelism to accelerate the synthesis of optimal abstract transformers.

cs.PL↗

arXiv2026

A variable time-step, second-order, and MBP-preserving linear stabilized scheme for the time-fractional Allen-Cahn equation

In this paper, we present a second-order linear scheme based on the variable-step Alikhanov formula and central difference discretization for the time-fractional Allen-Cahn equation. The nonlinear potential is treated explicitly via a second-order extrapolation with preprocessing, which enables the discrete maximum-bound principle (MBP) to be preserved through an appropriate stabilization technique. Moreover, by developing a discrete fractional Grönwall inequality together with the uniform boundedness of numerical solutions guaranteed by the MBP, we establish an $α$-robust and optimal second-order maximum-norm error estimate under initial weak singularity assumption. In addition, energy stability is proved in the sense that the discrete original energy is uniformly bounded by the initial energy plus a high-order spatiotemporal correction term. Finally, extensive numerical experiments are presented to demonstrate the effectiveness of the proposed scheme.

math.NA↗

arXiv2026

Fully decoupled, linear and structure-preserving block-centered finite difference methods for the Keller-Segel chemotaxis system on staggered non-uniform grids

In this paper, we propose two fully decoupled, linear and structure-preserving block-centered finite difference schemes for the classical Keller-Segel chemotaxis system on staggered non-uniform spatial grids. Both novel schemes are second-order accurate in space; one is first-order accurate in time, while the other achieves second-order temporal accuracy. Moreover, we show that the schemes preserve several inherent physical laws at the discrete level: (i) the positivity of both the cell density and the chemoattractant concentration; (ii) the conservation of total cell mass; and (iii) a discrete energy dissipation property for the first-order scheme. In particular, the temporally first-order scheme unconditionally preserves positivity, mass conservation, and energy dissipation, whereas the second-order scheme ensures positivity under a sufficient (but not necessary) time-step condition. The proposed methods yield more accurate and efficient simulations of chemotactic dynamics, especially in the presence of rapid blow-up phenomena, on specified non-uniform spatial grids. Numerical experiments are conducted to validate the theoretical findings and to illustrate the accuracy and reliability of the proposed schemes.

math.NA↗

arXiv2026

Polynomial Invariant Generation for Floating-Point Programs

In numeric-intensive computations, it is well known that the execution of floating-point programs is imprecise as floating-point arithmetic incurs round-off errors. Although round-off errors are small for a single floating-point operation, the aggregation of such errors may be dramatic and cause catastrophic program failures. Therefore, to ensure the correctness of floating-point programs, round-off error needs to be carefully taken into account. In this work, we consider polynomial invariant generation for floating-point programs, aiming at generating tight invariants under the perturbation of round-off errors. Our contribution is a novel framework for applying polynomial constraint solving to address the invariant generation problem, which is also the first polynomial constraint solving based approach that handles floating-point errors to our best knowledge. In our framework, we propose a novel combination of round-off error analysis and polynomial constraint solving, aiming to circumvent the cost of handling a large number of error variables in the floating-point model. Experimental results over a variety of challenging benchmarks show that our framework outperforms SOTA approaches in both time efficiency and the precision of generated invariants.

cs.PL↗

arXiv2026

Probabilistic Floating-Point Round-Off Analysis via Concentration Inequalities

Floating-point round-off errors are ubiquitous in numerically intensive programs arising in fields such as scientific computing and optimization. As floating-point errors potentially lead to unexpected and catastrophic program failures, one must derive guaranteed round-off thresholds to ensure the correctness of these programs. However, deterministic round-off thresholds tend to be too conservative to be usable in practice, since they often involve large round-off errors that occur with small probability. Probabilistic thresholds relax deterministic ones by specifying that the probability of the round-off error exceeding a threshold is below a given confidence. In this work, we propose a novel approach to probabilistic round-off analysis, by applying concentration inequalities over the Taylor expansion from FPTaylor (TOPLAS 2018). A major obstacle in applying concentration inequalities is that the Taylor expansion involves absolute value operators that make the calculation of the expected values of the first order partial differential terms difficult. Our first step to overcome this obstacle is a sound over-approximation that removes the absolute value operators in polynomial expressions. Then, we show how to handle fractional expressions by a transformation into polynomial case. Finally, we show how to improve our approach with range partitioning. Our approach is scalable since the key computational part is the calculation of expected values of polynomial expressions with independent variables, for which the linear and independence properties of expectation boost the computation. Experimental results show that our approach is orders of magnitude more time efficient, while producing thresholds with comparable precision against the state of the art.

cs.LO↗

arXiv2026

Probabilistic Verification of Neural Networks via Efficient Probabilistic Hull Generation

The problem of probabilistic verification of a neural network investigates the probability of satisfying the safe constraints in the output space when the input is given by a probability distribution. It is significant to answer this problem when the input is affected by disturbances often modeled by probabilistic variables. In the paper, we propose a novel neural network probabilistic verification framework which computes a guaranteed range for the safe probability by efficiently finding safe and unsafe probabilistic hulls. Our approach consists of three main innovations: (1) a state space subdivision strategy using regression trees to produce probabilistic hulls, (2) a boundary-aware sampling method which identifies the safety boundary in the input space using samples that are later used for building regression trees, and (3) iterative refinement with probabilistic prioritization for computing a guaranteed range for the safe probability. The accuracy and efficiency of our approach are evaluated on various benchmarks including ACAS Xu and a rocket lander controller. The result shows an obvious advantage over the state of the art.

cs.AI↗

arXiv2026

High-order nonuniform time-stepping and MBP-preserving linear schemes for the time-fractional Allen-Cahn equation

In this paper, we present a class of nonuniform time-stepping, high-order linear stabilized schemes that can preserve both the discrete energy stability and maximum-bound principle (MBP) for the time-fractional Allen-Cahn equation. To this end, we develop a new prediction strategy to obtain a second-order and MBP-preserving predicted solution, which is then used to handle the nonlinear potential explicitly. Additionally, we introduce an essential nonnegative auxiliary functional that enables the design of an appropriate stabilization term to dominate the predicted nonlinear potential, and thus to preserve the discrete MBP. Combining the newly developed prediction strategy and auxiliary functional, we propose two unconditionally energy-stable linear stabilized schemes, L1 and L2-$1_σ$ schemes. We show that the L1 scheme unconditionally preserves the discrete MBP, whereas the L2-$1_σ$ scheme requires a mild time-step restriction. Furthermore, we develop an improved L2-$1_σ$ scheme with enhanced MBP preservation for large time steps, achieved through a novel unbalanced stabilization term that leverages the boundedness and monotonicity of the auxiliary functional. Representative numerical examples validate the accuracy, effectiveness, and physics-preserving of the proposed methods.

math.NA↗

arXiv2026

Array-Carrying Symbolic Execution for Function Contract Generation

Function contract generation is a classical problem in program analysis that targets the automated analysis of functions in a program with multiple procedures. The problem is fundamental in inter-procedural analysis where properties of functions are first obtained via the generation of function contracts and then the generated contracts are used as building blocks to analyze the whole program. Typical objectives in function contract generation include pre-/post-conditions and assigns information (that specifies the modification information over program variables and memory segments during function execution). In programs with array manipulations, a crucial point in function contract generation is the treatment of array segments that imposes challenges in inferring invariants and assigns information over such segments. To address this challenge, we propose a novel symbolic execution framework that carries invariants and assigns information over contiguous segments of arrays. We implement our framework as a prototype within LLVM, and further integrate our prototype with the ACSL assertion format and the Frama-C software verification platform. Experimental evaluation over a variety of benchmarks from the literature and functions from realistic libraries shows that our framework is capable of handling array manipulating functions that indeed involve the carry of array information and are beyond existing approaches.

cs.PL↗

arXiv2026

Piecewise Analysis of Probabilistic Programs via $k$-Induction

In probabilistic program analysis, quantitative analysis aims at deriving tight numerical bounds for probabilistic properties such as expectation and assertion probability. Most previous works consider numerical bounds over the whole program state space monolithically and do not consider piecewise bounds. Not surprisingly, monolithic bounds are either conservative, or not expressive and succinct enough in general. To derive better bounds, we propose a novel approach for synthesizing piecewise bounds over probabilistic programs. First, we show how to extract useful piecewise information from latticed $k$-induction operators, and combine the piecewise information with Optional Stopping Theorem to obtain a general approach to derive piecewise bounds over probabilistic programs. Second, we develop algorithms to synthesize piecewise polynomial bounds, and show that the synthesis can be reduced to bilinear programming in the linear case, and soundly relaxed to semidefinite programming in the polynomial case. Experimental results show that our approach generates tight piecewise bounds for a wide range of benchmarks when compared with the state of the art.

cs.PL↗

arXiv2025

Unconditional optimal-order error estimates of linear relaxation compact difference scheme for the coupled nonlinear Schrödinger system

This paper presents a linear, decoupled, mass- and energy-conserving numerical scheme for the multi-dimensional coupled nonlinear Schrödinger (CNLS) system. The scheme combines the fourth-order compact difference approximation in space with the relaxation technique in a time-staggered mesh framework, solving the primal unknowns and introduced auxiliary relaxation variables sequentially with high efficiency and high-order accuracy. We show the unique solvability and discrete conservation laws of the developed scheme. In particular, for the first time, leveraging an auxiliary error equation system combined with the cut-off technique, optimal-order error estimates in the discrete H1-norm for the primal variables at the time nodes, and in the discrete L2-norm for the auxiliary relaxation variables at the intermediate time nodes, are rigorously proved without any coupling mesh conditions, which contribute to the primary theoretical contribution of this paper for multi-dimensional CNLS system. Numerical experiments demonstrate convincingly the strong performance of the proposed scheme in long-term simulations, maintaining both physical invariants and high-order accuracy.

math.NA↗

arXiv2025

Numerical analysis and efficient implementation of fast collocation methods for fractional Laplacian model on nonuniform grids

We propose a fast collocation method based on Krylov subspace iterative solver on general nonuniform grids for the fractional Laplacian problem, in which the fractional operator is presented in a singular integral formulation. The method is proved to be uniquely solvable on general nonuniform grids for $α\in(0,1)$, provided that the sum-of-exponentials (SOE) approximation is sufficiently accurate. In addition, a modified scheme is developed and proved to be uniquely solvable on uniform grids for $α\in(0,2)$. Efficient implementation of the proposed fast collocation schemes based on fast matrix-vector multiplication is carefully discussed, in terms of computational complexity and memory requirement. To further improve computational efficiency, a banded preconditioner is incorporated into the Krylov subspace iterative solver. A rigorous maximum-norm error analysis for $α\in(0,1)$ is presented on specific graded grids, which shows that the convergence order depends on the grading parameter. Numerical experiments validate the predicted convergence and demonstrate the efficiency of the fast collocation schemes.

math.NA↗

arXiv2025

Dynamic-stabilization-based linear schemes for the Allen-Cahn equation with degenerate mobility: MBP and energy stability

In this paper, we investigate linear first- and second-order numerical schemes for the Allen--Cahn equation with a general (possibly degenerate) mobility. Compared with existing numerical methods, our schemes employ a novel dynamic stabilization approach that guarantees unconditional preservation of the maximum bound principle (MBP) and energy stability. A key advance is that the discrete energy stability remains valid even in the presence of degenerate mobility-a property we refer to as mobility robustness. Rigorous maximum-norm error estimates are also established. In particular, for the second-order scheme, we introduce a new prediction strategy with a cut-off preprocessing procedure on the extrapolation solution, and only one linear system needs to be solved per time level. Representative numerical examples are provided to validate the theoretical findings and performance of the proposed schemes.

math.NA↗