Finding polynomial loop invariants for probabilistic programs

Yijun Feng, Lijun Zhang, David N. Jansen +2

A Theorem Prover for Quantum Hoare Logic and Its Applications

Tao Liu, Yangjia Li, Shuling Wang +2

Inner-Approximating Reachable Sets for Polynomial Systems with Time-Varying Uncertainties

Bai Xue, Martin Fränzle, Naijun Zhan

Synthesizing SystemC Code from Delay Hybrid CSP

Gaogao Yan, Li Jiao, Shuling Wang +1

Approximate Bisimulation and Discretization of Hybrid CSP

Gaogao Yan, Li Jiao, Yangjia Li +2

Computing Semi-algebraic Invariants for Polynomial Dynamical Systems

Jiang Liu, Naijun Zhan, Hengjun Zhao

Reach-Avoid Differential Games Based on Invariant Generation

Bai Xue, Qiuye Wang, Naijun Zhan +2

The paper investigates infinite‑horizon reach‑avoid differential games, deriving the set of initial states from which a player can continuously enforce safety using Hamilton‑Jacobi…

Compositional Hoare-style Reasoning about Hybrid CSP in the Duration Calculus

Dimitar Guelev, Shuling Wang, Naijun Zhan

Interpolation synthesis for quadratic polynomial inequalities and combination with EUF

Ting Gan, Liyun Dai, Bican Xia +3

Robust Non-termination Analysis of Numerical Software

Bai Xue, Naijun Zhan, Yangjia Li +1

Generating Non-Linear Interpolants by Semidefinite Programming

Liyun Dai, Bican Xia, Naijun Zhan