Abstractions for Fault-Tolerant Distributed System
Verification

• ABSTRACT:
  
  Four kinds of abstraction for the design and analysis of fault--tolerant distributed systems are discussed.  These abstractions concern system messages, faults, fault--masking voting, and communication.  The abstractions are formalized in higher--order logic, and are intended to facilitate specifying and verifying such systems in higher--order theorem--provers.

• BIBTEX:
  

  @InProceedings{spider_abstractions,
    author =    {Lee Pike and Jeffrey Maddalon and Paul Miner and Alfons Geser},
    title =     {Abstractions for Fault-Tolerant Distributed System Verification},
    booktitle = {Theorem Proving in Higher Order Logics ({TPHOL}s)},
    year =      {2004},
    pages =     {257--270},
    editor =    {Konrad Slind and Annette Bunker and Ganesh Gopalakrishnan},
    volume =    {3223},
    series =    {Lecture Notes in Computer Science},
    publisher = {Springer},
    note =      {Available at \url{https://leepike.github.io/pub_pages/abstractions.html}}}

• PAPER DOWNLOAD: pdf 

• SLIDES DOWNLOAD: pdf

• PVS FILES DOWNLOAD: PVS dump file