27 citations · 62 across the 16 of their papers we have counts for
23 papers
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…
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-…
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…
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…
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 classical…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…