2 citations · 4 across the 8 of their papers we have counts for
9 papers
How Powerful are LLMs in Generating Formal Program Specifications?
Fanpeng Yang, Xing Li, Shuling Wang +7
Formal verification provides strong guarantees of software correctness, but its adoption is limited by the high cost of writing precise formal specifications. While recent large la…
Exact Moment Estimation of Stochastic Differential Dynamics
Shenghua Feng, Jie An, Naijun Zhan +1
Moment estimation for stochastic differential equations (SDEs) is fundamental to the formal reasoning and verification of stochastic dynamical systems, yet remains challenging and…
Switching Controller Synthesis for Hybrid Systems Against STL Formulas
Han Su, Shenghua Feng, Sinong Zhan +1
Switching controllers play a pivotal role in directing hybrid systems (HSs) towards the desired objective, embodying a ``correct-by-construction'' approach to HS design. Identifyin…
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…
On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains
Hao Wu, Shenghua Feng, Ting Gan +3
Barrier certificates, serving as differential invariants that witness system safety, play a crucial role in the verification of cyber-physical systems (CPS). Prevailing computation…
Reset Controller Synthesis by Reach-avoid Analysis for Delay Hybrid Systems
Han Su, Jiyu Zhu, Shenghua Feng +5
A reset controller plays a crucial role in designing hybrid systems. It restricts the initial set and redefines the reset map associated with discrete transitions, in order to guar…
Lower Bounds for Possibly Divergent Probabilistic Programs
Shenghua Feng, Mingshuai Chen, Han Su +3
We present a new proof rule for verifying lower bounds on quantities of probabilistic programs. Our proof rule is not confined to almost-surely terminating programs -- as is the ca…
Unbounded-Time Safety Verification of Stochastic Differential Dynamics
Shenghua Feng, Mingshuai Chen, Bai Xue +2
In this paper, we propose a method for bounding the probability that a stochastic differential equation (SDE) system violates a safety specification over the infinite time horizon.…
Over- and Under-Approximating Reachable Sets for Perturbed Delay Differential Equations
Bai Xue, Qiuye Wang, Shenghua Feng +1
This note explores reach set computations for perturbed delay differential equations (DDEs). The perturbed DDEs of interest in this note is a class of DDEs whose dynamics are subje…