Publications (49)
Automated Recurrence Analysis for Almost-Linear Expected-Runtime Bounds
Krishnendu Chatterjee, Hongfei Fu, Aniket Murhekar
We consider the problem of developing automated techniques for solving recurrence relations to aid the expected-runtime analysis of programs. Several classical textbook algorithms…
A variable time-step, second-order, and MBP-preserving linear stabilized scheme for the time-fractional Allen-Cahn equation
Bingyin Zhang, Ao Zhang, Hongfei Fu
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 equatio…
Quantitative Analysis of Assertion Violations in Probabilistic Programs
Jinyi Wang, Yican Sun, Hongfei Fu +2
In this work, we consider the fundamental problem of deriving quantitative bounds on the probability that a given assertion is violated in a probabilistic program. We provide autom…
A fast fractional block-centered finite difference method for two-sided space-fractional diffusion equations on general nonuniform grids
Meijie Kong, Hongfei Fu
In this paper, a two-sided variable-coefficient space-fractional diffusion equation with fractional Neumann boundary condition is considered. To conquer the weak singularity caused…
An efficient two-grid fourth-order compact difference scheme with variable-step BDF2 method for the semilinear parabolic equation
Bingyin Zhang, Hongfei Fu
Due to the lack of corresponding analysis on appropriate mapping operator between two grids, high-order two-grid difference algorithms are rarely studied. In this paper, we firstly…
A linear, mass-conserving, multi-time-step compact block-centered finite difference method for incompressible miscible displacement problem in porous media
Xiaoying Wang, Hongxing Rui, Hongfei Fu
In this paper, a two-dimensional incompressible miscible displacement model is considered, and a novel decoupled and linearized high-order finite difference scheme is developed, by…
A linear, decoupled and positivity-preserving time-staggered block-centered finite difference method for the multi-species Keller-Segel chemotaxis system
Ao Zhang, Bingyin Zhang, Hongfei Fu
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…
Maximal Cost-Bounded Reachability Probability on Continuous-Time Markov Decision Processes
Hongfei Fu
In this paper, we consider multi-dimensional maximal cost-bounded reachability probability over continuous-time Markov decision processes (CTMDPs). Our major contributions are as f…
Probabilistic Verification of Neural Networks via Efficient Probabilistic Hull Generation
Jingyang Li, Xin Chen, Hongfei Fu +1
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 proba…
POD/DEIM Reduced-Order Modeling of Time-Fractional Partial Differential Equations with Applications in Parameter Identification
Hongfei Fu, Hong Wang, Zhu Wang
In this paper, a reduced-order model (ROM) based on the proper orthogonal decomposition and the discrete empirical interpolation method is proposed for efficiently simulating time-…
Structural Abstraction and Refinement for Probabilistic Programs
Guanyan Li, Juanen Li, Zhilei Han +3
In this paper, we present structural abstraction refinement, a novel framework for verifying the threshold problem of probabilistic programs. Our approach represents the structure…
Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving
Peixin Wang, Tengshun Yang, Hongfei Fu +2
In Bayesian probabilistic programming, a central problem is to estimate the normalised posterior distribution (NPD) of a probabilistic program with conditioning via score (a.k.a. o…
Inductive Reachability Witnesses
Ali Asadi, Krishnendu Chatterjee, Hongfei Fu +2
In this work, we consider the fundamental problem of reachability analysis over imperative programs with real variables. The reachability property requires that a program can reach…
Fully decoupled, linear and structure-preserving block-centered finite difference methods for the Keller-Segel chemotaxis system on staggered non-uniform grids
Jie Xu, Hongfei Fu
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 staggere…
Sharp Two-Round Adaptivity and Round Hierarchies for Semantic Regular Expressions
Runzhou Li, Hongfei Fu, Qingkai Shi +1
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 fix…
EconCSLib: A Lean Library for Computational Economics and AI-Assisted Research
Xiaohui Bei, Jiajun Ma, Zhan Jing +2
Mathematical formalization uses interactive theorem provers to turn informal mathematical statements into machine-checkable artifacts. The success of mathlib, a large collaborative…
Affine Disjunctive Invariant Generation with Farkas' Lemma
Jingyu Ke, Hongfei Fu, Hongming Liu +3
In the verification of loop programs, disjunctive invariants are essential to capture complex loop dynamics such as phase and mode changes. In this work, we develop a novel approac…
Computational Approaches for Stochastic Shortest Path on Succinct MDPs
Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady +1
We consider the stochastic shortest path (SSP) problem for succinct Markov decision processes (MDPs), where the MDP consists of a set of variables, and a set of nondeterministic ru…
Polynomial Invariant Generation for Floating-Point Programs
Xuran Cai, Liqian Chen, Hongfei Fu
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-…
Synthesizing Best Abstract Transformers via Parallel Bit-Vector Optimization
Weiqi Wang, Peisen Yao, Hanrui Zuo +3
Abstract interpretation provides a principled foundation for constructing sound static analyses through systematic abstraction. A central challenge is synthesizing the best abstrac…
High-order nonuniform time-stepping and MBP-preserving linear schemes for the time-fractional Allen-Cahn equation
Bingyin Zhang, Hongfei Fu
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…
Modular Verification for Almost-Sure Termination of Probabilistic Programs
Mingzhang Huang, Hongfei Fu, Krishnendu Chatterjee +1
In this work, we consider the almost-sure termination problem for probabilistic programs that asks whether a given probabilistic program terminates with probability 1. Scalable app…
Cost Analysis of Nondeterministic Probabilistic Programs
Peixin Wang, Hongfei Fu, Amir Kafshdar Goharshady +3
We consider the problem of expected cost analysis over nondeterministic probabilistic programs, which aims at automated methods for analyzing the resource-usage of such programs. P…
Energy dissipation law and maximum bound principle-preserving linear BDF2 schemes with variable steps for the Allen-Cahn equation
Bingyin Zhang, Hongfei Fu, Rihui Lan +1
In this paper, we propose and analyze a linear, structure-preserving scalar auxiliary variable (SAV) method for solving the Allen--Cahn equation based on the second-order backward…
Numerical analysis and efficient implementation of fast collocation methods for fractional Laplacian model on nonuniform grids
Meijie Kong, Hongfei Fu
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…
Equational Bit-Vector Solving via Strong Gröbner Bases
Jiaxin Song, Hongfei Fu, Charles Zhang
Bit-vectors, which are integers in a finite number of bits, are ubiquitous in software and hardware systems. In this work, we consider the satisfiability modulo theories (SMT) of b…
New Approaches for Almost-Sure Termination of Probabilistic Programs
Mingzhang Huang, Hongfei Fu, Krishnendu Chatterjee
We study the almost-sure termination problem for probabilistic programs. First, we show that supermartingales with lower bounds on conditional absolute difference provide a sound a…
Dynamic-stabilization-based linear schemes for the Allen-Cahn equation with degenerate mobility: MBP and energy stability
Hongfei Fu, Dianming Hou, Zhonghua Qiao +1
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 nu…
Non-polynomial Worst-Case Analysis of Recursive Programs
Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady
We study the problem of developing efficient approaches for proving worst-case bounds of non-deterministic recursive programs. Ranking functions are sound and complete for proving…
Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time
Peixin Wang, Hongfei Fu, Krishnendu Chatterjee +2
The notion of program sensitivity (aka Lipschitz continuity) specifies that changes in the program input result in proportional changes to the program output. For probabilistic pro…
Approximating Acceptance Probabilities of CTMC-Paths on Multi-Clock Deterministic Timed Automata
Hongfei Fu
We consider the problem of approximating the probability mass of the set of timed paths under a continuous-time Markov chain (CTMC) that are accepted by a deterministic timed autom…
High order numerical methods based on quadratic spline collocation method and averaged L1 scheme for the variable-order time fractional mobile/immobile diffusion equation
Xiao Ye, Jun Liu, Bingyin Zhang +2
In this paper, we consider the variable-order time fractional mobile/immobile diffusion (TF-MID) equation in two-dimensional spatial domain, where the fractional order sati…
A decoupled linear, mass-conservative block-centered finite difference method for the Keller-Segel chemotaxis system
Jie Xu, Hongfei Fu
As a class of nonlinear partial differential equations, the Keller-Segel system is widely used to model chemotaxis in biology. In this paper, we present the construction and analys…
Probabilistic Floating-Point Round-Off Analysis via Concentration Inequalities
Yichen Tao, Hongfei Fu, Jiawei Chen +1
Floating-point round-off errors are ubiquitous in numerically intensive programs arising in fields such as scientific computing and optimization. As floating-point errors potential…
Termination Analysis of Probabilistic Programs through Positivstellensatz's
Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady
We consider nondeterministic probabilistic programs with the most basic liveness property of termination. We present efficient methods for termination analysis of nondeterministic…
Polynomial Invariant Generation for Non-deterministic Recursive Programs
Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady +1
We consider the classical problem of invariant generation for programs with polynomial assignments and focus on synthesizing invariants that are a conjunction of strict polynomial…
Termination of Nondeterministic Recursive Probabilistic Programs
Krishnendu Chatterjee, Hongfei Fu
We study the termination problem for nondeterministic recursive probabilistic programs. First, we show that a ranking-supermartingales-based approach is both sound and complete for…
Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs
Krishnendu Chatterjee, Hongfei Fu, Petr Novotny +1
In this paper, we consider termination of probabilistic programs with real-valued variables. The questions concerned are: 1. qualitative ones that ask (i) whether the program termi…
Fractional-step High-order and Bound-preserving Method for Convection Diffusion Equations
Baolin Kuang, Hongfei Fu, Shusen Xie
In this paper, we derive two bound-preserving and mass-conserving schemes based on the fractional-step method and high-order compact (HOC) finite difference method for nonlinear co…
Array-Carrying Symbolic Execution for Function Contract Generation
Weijie Lu, Jingyu Ke, Hongfei Fu +4
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 funda…
Error estimates of linear decoupled structure-preserving incremental viscosity splitting methods for the Cahn--Hilliard--Navier--Stokes system
Baolin Kuang, Hongfei Fu, Xiaoli Li
We propose first- and second-order time discretization schemes for the coupled Cahn--Hilliard--Navier--Stokes model, leveraging the incremental viscosity splitting (IVS) method. Th…
Piecewise Analysis of Probabilistic Programs via -Induction
Tengshun Yang, Shenghua Feng, Hongfei Fu +3
In probabilistic program analysis, quantitative analysis aims at deriving tight numerical bounds for probabilistic properties such as expectation and assertion probability. Most pr…
Unconditional optimal-order error estimates of linear relaxation compact difference scheme for the coupled nonlinear Schrödinger system
Ying Gao, Hongfei Fu, Xiaoying Wang
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 th…
Automated Tail Bound Analysis for Probabilistic Recurrence Relations
Yican Sun, Hongfei Fu, Krishnendu Chatterjee +1
Probabilistic recurrence relations (PRRs) are a standard formalism for describing the runtime of a randomized algorithm. Given a PRR and a time limit , we consider the classica…
Guided Diffusion Model for Adversarial Purification
Jinyi Wang, Zhaoyang Lyu, Dahua Lin +2
With wider application of deep neural networks (DNNs) in various algorithms and frameworks, security threats have become one of the concerns. Adversarial attacks disturb DNN-based…
Maximum-Norm Error Estimates of Fourth-Order Compact and ADI Compact Finite Difference Methods for Nonlinear Coupled Bacterial Systems
Jie Xu, Shusen Xie, Hongfei Fu
In this paper, by introducing two temporal-derivative-dependent auxiliary variables, a linearized and decoupled fourth-order compact finite difference method is developed and analy…
Strang splitting structure-preserving high-order compact difference schemes for nonlinear convection diffusion equations
Baolin Kuang, Shusen Xie, Hongfei Fu
In this paper, we present a class of high-order and efficient compact difference schemes for nonlinear convection diffusion equations, which can preserve both bounds and mass. For…
Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties
Hongfei Fu, Yi Li, Jianlin Li +1
Probabilistic timed automata (PTAs) are timed automata (TAs) extended with discrete probability distributions.They serve as a mathematical model for a wide range of applications th…
Concentration-Bound Analysis for Probabilistic Programs and Probabilistic Recurrence Relations
Jinyi Wang, Yican Sun, Hongfei Fu +3
Analyzing probabilistic programs and randomized algorithms are classical problems in computer science. The first basic problem in the analysis of stochastic processes is to conside…