Re: [isabelle] who knows theorem-proving about cache protocols
There hasn't been a lot of work with theorem provers on shared-memory
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
model checkers. For example, a student of mine, Sudhindra Pandav,
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
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