[isabelle] on formalization of predicate abstraction



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

regards!



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