23 citations · 68 across the 22 of their papers we have counts for
6 papers · 1 filter
Verifying Randomized Consensus Protocols with Common Coins
Song Gao, Bohua Zhan, Zhilin Wu +1
Randomized fault-tolerant consensus protocols with common coins are widely used in cloud computing and blockchain platforms. Due to their fundamental role, it is vital to guarantee…
HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes
Xiangyu Jin, Bohua Zhan, Shuling Wang +1
We present a tool called HHLPar for verifying hybrid systems modelled in Hybrid Communicating Sequential Processes (HCSP). HHLPar is built upon a Hybrid Hoare Logic for HCSP, which…
KBX: Verified Model Synchronization via Formal Bidirectional Transformation
Jianhong Zhao, Yongwang Zhao, Peisen Yao +3
Complex safety-critical systems require multiple models for a comprehensive description, resulting in error-prone development and laborious verification. Bidirectional transformati…
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…
OSVAuto: automatic proofs about functional specifications in OS verification
Yulun Wu, Bican Xia, Jiale Xu +2
We present OSVAuto for automatic proofs about functional specifications that commonly arise when verifying operating system kernels. The algorithm behind OSVAuto is designed to sup…
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…