[isabelle] on formalization of predicate abstraction in Isabelle

Dear experts:
  Do you know who have done formalization in Isabelle or other theorem prover
 for predicate abstraction in advanced model checking theory, and
 prove that the abstarcted system 
can simulates the original system?

Thanks in advance


Associate Professor 
State Key Laboratory of Computer Science, 
Institute of Software, 
Chinese Academy of Sciences 
P.O. Box 8718 
Beijing 100190 

Tel. (86) (10) 62661645 
E-mail: lyj238 at ios.ac.cn 

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.