3 citations · 7 across the 10 of their papers we have counts for
4 papers · 1 filter
Extending PPTL for Verifying Heap Evolution Properties
Xu Lu, Zhenhua Duan, Cong Tian
In this paper, we integrate separation logic with Propositional Projection Temporal Logic (PPTL) to obtain a two-dimensional logic, namely PPTL$^{\tiny\mbox{SL}}$. The spatial dime…
An Improved Decision Procedure for Linear Time Mu-Calculus
Yao Liu, Zhenhua Duan, Cong Tian
An improved Present Future form (PF form) for linear time -calculus (TL) is presented in this paper. In particular, the future part of the new version turns into the conjunct…
Detecting Spurious Counterexamples Efficiently in Abstract Model Checking
Cong Tian, Zhenhua Duan
Abstraction is one of the most important strategies for dealing with the state space explosion problem in model checking. In the abstract model, the state space is largely reduced,…
Making Abstraction Refinement Efficient in Model Checking
Cong Tian, Zhenhua Duan
Abstraction is one of the most important strategies for dealing with the state space explosion problem in model checking. In the abstract model, although the state space is largely…