17 citations · 27 across the 9 of their papers we have counts for
9 papers
Distinguishable-particle Glassy Crystal: the simplest molecular model of glass
Leo S. I. Lam, Gautham Gopinath, Zichen Zhao +7
The nature of glassy dynamics and the glass transition are long-standing problems under active debate. In the presence of a structural disorder widely believed to be an essential c…
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…
Machine-checked executable semantics of Stateflow
Shicheng Yi, Shuling Wang, Bohua Zhan +1
Simulink is a widely used model-based development environment for embedded systems. Stateflow is a component of Simulink for modeling event-driven control via hierarchical state ma…
Compositional Hoare-style Reasoning about Hybrid CSP in the Duration Calculus
Dimitar Guelev, Shuling Wang, Naijun Zhan
Deductive methods for the verification of hybrid systems vary on the format of statements in correctness proofs. Building on the example of Hoare triple-based reasoning, we have in…
Approximate Bisimulation and Discretization of Hybrid CSP
Gaogao Yan, Li Jiao, Yangjia Li +2
Hybrid Communicating Sequential Processes (HCSP) is a powerful formal modeling language for hybrid systems, which is an extension of CSP by introducing differential equations for m…
A Theorem Prover for Quantum Hoare Logic and Its Applications
Tao Liu, Yangjia Li, Shuling Wang +2
Quantum Hoare Logic (QHL) was introduced in Ying's work to specify and reason about quantum programs. In this paper, we implement a theorem prover for QHL based on Isabelle/HOL. By…