Journal/document/root.tex
changeset 13 735e36c64a71
parent 11 8e02fb168350
child 17 105715a0a807
equal deleted inserted replaced
12:85116bc854c0 13:735e36c64a71
    66 has never been formally verified in a theorem prover. As already
    66 has never been formally verified in a theorem prover. As already
    67 pointed out in the literature, the original informal investigation of
    67 pointed out in the literature, the original informal investigation of
    68 the Property Inheritance Protocol presents a correctness ``proof'' for
    68 the Property Inheritance Protocol presents a correctness ``proof'' for
    69 an \emph{incorrect} algorithm. In this paper we fix the problem of
    69 an \emph{incorrect} algorithm. In this paper we fix the problem of
    70 this proof by making all notions precise and implementing a variant of
    70 this proof by making all notions precise and implementing a variant of
    71 a solution proposed earlier. We also generalise the proof to the
    71 a solution proposed earlier. We also generalise the original informal proof to the
    72 practically relevant case where critical sections can
    72 practically relevant case where critical sections can
    73 overlap. Our formalisation in Isabelle/HOL not just
    73 overlap. Our formalisation in Isabelle/HOL not just
    74 uncovers facts not mentioned in the literature, but also shows how to
    74 uncovers facts not mentioned in the literature, but also shows how to
    75 efficiently implement this protocol. Earlier correct implementations
    75 efficiently implement this protocol. Earlier correct implementations
    76 were criticised as too inefficient. Our formalisation is based on
    76 were criticised as too inefficient. Our formalisation is based on