Jump to Content
Milos Besta

Milos Besta

Authored Publications
Google Publications
Other Publications
Sort By
  • Title
  • Title, descending
  • Year
  • Year, descending
    An Assertional Correctness Proof of a Self-Stabilizing l-Exclusion Algorithm
    Frank Stomp
    11th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'06), IEEE CS (2006), pp. 199-208
    Preview abstract A formal correctness proof of a self-stabilizing l-exclusion algorithm (SLEX) is described. The analyzed algorithm is an improvement of the SLEX due to Abraham, Dolev, Herman, and Koll, since our version satisfies a stronger liveness property. The proof is formulated in Linear-Time Temporal Logic and utilizes a history variable to model access to regular registers. The proof consists of a safety part and a liveness part. Our analysis provides some new insight in the correctness of the algorithm: (1) Our proof is constructive. That is, we explicitly formulate auxiliary quantities required to establish some of the properties. This contrasts with the operational arguments of Abraham et al., where many quantities are not explicitly formulated and the validity of the above mentioned properties is established by disproving their non-existence. (2) We characterize processes (and their minimum number) identified by some process as attempting to enter the critical section. (3) A novel proof rule for reasoning about programs in the presence of disabled processes is presented to structure the liveness proof. View details
    A Complete Mechanization of Correctness of a String-Preprocessing Algorithm
    Frank Stomp
    Formal Methods in System Design, vol. 27 (2005), pp. 5-17
    Mechanization of a Proof of String-Preprocessing in Boyer-Moore's Pattern Matching Algorithm
    Frank Stomp
    8th International Conference on Engineering of Complex Computer Systems (ICECCS '02), IEEE CS (2002), pp. 68-77