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

There hasn't been a lot of work with theorem provers on shared-memory protocols.
One example is Seungjoon Park's work at Stanford. See

for some pointers to his work.

Jason Yang used higher order logic to specify memory orderings in

Google also tells me that J Moore published a paper entitled

   "An ACL2 proof of Write-Invalidate Cache Coherence"

in LNCS 1427 (Proceedings of CAV'98).

However, most people who verify such things use Murphi, or other explicit-state model checkers. For example, a student of mine, Sudhindra Pandav, recently came
up with counterexample-based techniques (using UCLID) and applied them
to FLASH and German.


On Sep 16, 2005, at 6:22 AM, yongjian Li wrote:

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).

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