16 citations · 26 across the 15 of their papers we have counts for
4 papers · 1 filter
Mars 2.0: A Toolchain for Modeling, Analysis, Verification and Code Generation of Cyber-Physical Systems
Bohua Zhan, Xiong Xu, Qiang Gao +4
We introduce Mars 2.0 for modeling, analysis, verification and code generation of Cyber-Physical Systems. Mars 2.0 integrates Mars 1.0 with several important extensions and improve…
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…
Formally Verified C Code Generation from Hybrid Communicating Sequential Processes
Shuling Wang, Zekun Ji, Bohua Zhan +3
Hybrid Communicating Sequential Processes (HCSP) is a formal model for hybrid systems, including primitives for evolution along an ordinary differential equation (ODE), communicati…
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…