17 citations · 81 across the 44 of their papers we have counts for
6 papers · 1 filter
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…
Synthesizing Invariants for Polynomial Programs by Semidefinite Programming
Hao Wu, Qiuye Wang, Bai Xue +3
Constraint-solving-based program invariant synthesis takes a parametric invariant template and encodes the (inductive) invariant conditions into constraints. The problem of charact…
Correct-by-Construction for Hybrid Systems by Synthesizing Reset Controller
Jiang Liu, Han Su, Yunjun Bai +4
Controller synthesis, including reset controller, feedback controller, and switching logic controller, provides an essential mechanism to guarantee the correctness and reliability…
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…
A Generalized Hybrid Hoare Logic
Naijun Zhan, Xiangyu Jin, Bohua Zhan +2
Deductive verification of hybrid systems (HSs) increasingly attracts more attention in recent years because of its power and scalability, where a powerful specification logic for H…
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…