[isabelle] who knows theorem-proving about cache protocols



Hi:
  who know who has theorem-proving tehniques for proving invariants for cache protocol, especially for parameter
protocols such as FLASH and German?
   I look for Isabelle's formalization for such problem, but it seems no result.
   I only look for Nipkow's result of I/O automata for ditributed computation (about 8 years before).

Regards!

 






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