4 papers
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…
Compression of enumerations and gain
George Barmpalias, Xiaoyan Zhang, Bohua Zhan
We study the compressibility of enumerations in the context of Kolmogorov complexity, focusing on strong and weak forms of compression and their gain: the amount of auxiliary infor…
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…
HpC: A Calculus for Hybrid and Mobile Systems -- Full Version
Xiong Xu, Jean-Pierre Talpin, Shuling Wang +4
Networked cybernetic and physical systems of the Internet of Things (IoT) immerse civilian and industrial infrastructures into an interconnected and dynamic web of hybrid and mobil…