Re: [isabelle] who knows theorem-proving about cache protocols



| who know who has theorem-proving tehniques for proving invariants for cache
| protocol, especially for parameter protocols such as FLASH and German?

I've done a formalization in HOL Light of the finite-state abstraction
method given by Chou, Mannava and Park at FMCAD 2004:

 http://www.cs.utexas.edu/users/hunt/FMCAD/2004/accepted/3.html

However, I've never written it up at all, let alone published it.

John.





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