Updated 05/25/08
Photo Album
Contact Me


I was a Ph.D. student at Wayne State University since Fall 1999 till June 2005. I was a member of the Formal Software Verification Lab at the Department of Computer Science, and I conducted research under the supervision of Frank Stomp. My research focused on Formal Methods and formal verification of algorithms and their correctness proofs. I was also interested in theorem proving, model checking, self-stabilization, distributed algorithms design and analysis, program semantics, and object/component-oriented technologies.

More information about my research can be found below on this page or at the following links:

bulletMy Previous Research
bulletMy Publications
bulletMy Resume
bulletMy Research Links
bulletMy Research Genealogy
A Formal Proof of a Self-Stabilizing Algorithm (2002-2005)

Distributed and parallel algorithms are usually complicated. An ℓ-exclusion algorithm implements a protocol that ensures that not more that ℓ processes are in their critical sections at the same time and every process interested in entering its critical section eventually enters the critical section.  A self-stabilizing version of that algorithm ensures that the protocol tolerates transient failures.

In this project, we have developed a formal correctness proof of a self-stabilizing ℓ-exclusion algorithm (SLEX). The analyzed algorithm is an improvement of 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 consists of a safety part and a liveness part. Our analysis provides some new insight in the correctness of the algorithm: (1) We characterize processes (and their minimum number) identified by some process as attempting to enter their critical sections, and (2) a novel proof rule for reasoning about programs in the presence of disabled processes is presented to structure the liveness proof. Our proof is constructive, in contrast to the operational arguments of Abraham et al.

Related Publications:
bulletBesta, M. and F. Stomp: An Assertional Correctness Proof of a Self-Stabilizing ℓ-Exclusion Algorithm (Extended Abstract). In Proceedings of the 11th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS '06), pp. 199-208, Stanford, CA, August 2006.
bulletBesta, M: Self-stabilizing ℓ-exclusion: A correctness proof. Dissertation, Wayne State University, Detroit, MI, 2005.
bulletBesta, M: Self-stabilizing ℓ-exclusion: A correctness proof. Dissertation prospectus, Wayne State University, Detroit, MI, 2002.
bulletAbraham, U., S. Dolev, T. Herman, and I. Koll: Self-stabilizing ℓ-exclusion. In Theoretical Computer Science 266(1-2), 653-692, 2001.

A Proof of Boyer-Moore's String Preprocessing Algorithm (2000-2002)

The Boyer-Moore's pattern matching algorithm utilizes two preprocessing algorithms: one based on single characters only and the other based on a string. Correctness of the single-character preprocessing algorithm has been established and mechanically verified by Boyer and Moore in 1981. The string-preprocessing algorithm is more complicated. There have been found several errors in that algorithm by different authors. In 1999, a minor error was found in the string-preprocessing algorithm and corrected. To make sure the correction of that error does not introduce any new errors in the algorithm a correctness proof of the corrected algorithm was developed. In this research project we have mechanically verified the hand-written correctness proof using the PVS theorem prover. The PVS proof can be found here.

Related Publications:
bulletBesta, M. and F. Stomp: A complete mechanization of a correctness proof of a string-preprocessing algorithm. In Formal Methods in System Design 27(1-2), pp. 5-27, 2005.
bulletStomp, F.: Correctness of substring-preprocessing in Boyer-Moore's pattern matching algorithm. In Theoretical Computer Science 290(1), 59-78, 2003.
bulletBesta, M. and F. Stomp: Mechanization of a proof of a string-preprocessing in Boyer-Moore's pattern matching algorithm. In Proceedings of the 8th International Conference on Engineering of Complex Computer Systems (ICECCS '02), pp. 68-77, IEEE CS, December 2002, Greenbelt, MD.

Home | Personal | Research | Teaching | Photo Album | Contact Me