

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, selfstabilization, distributed algorithms design and analysis, program semantics, and
object/componentoriented technologies.
More information about my research can be found below on this page or
at the following links:

A Formal Proof of a SelfStabilizing Algorithm
(20022005)
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
selfstabilizing version of that algorithm ensures that the protocol
tolerates transient failures.
In this project, we have developed a formal correctness proof of a selfstabilizing ℓ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 LinearTime 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:
 Besta, M. and F. Stomp:
An Assertional Correctness Proof of a SelfStabilizing ℓExclusion Algorithm (Extended Abstract).
In Proceedings of the 11^{th} IEEE International Conference on Engineering of Complex Computer Systems
(ICECCS '06), pp. 199208, Stanford, CA, August 2006. 
 Besta, M: Selfstabilizing ℓexclusion: A correctness proof.
Dissertation, Wayne State University, Detroit, MI, 2005. 
 Besta, M:
Selfstabilizing ℓexclusion: A correctness proof.
Dissertation prospectus, Wayne State University, Detroit,
MI, 2002. 
 Abraham, U., S. Dolev, T. Herman, and I. Koll:
Selfstabilizing ℓexclusion. In Theoretical Computer
Science 266(12), 653692, 2001.


A Proof of BoyerMoore's String Preprocessing Algorithm
(20002002)
The BoyerMoore's pattern matching algorithm utilizes two
preprocessing algorithms: one based on single characters only
and the other based on a string. Correctness of the
singlecharacter preprocessing algorithm has been established
and mechanically verified by Boyer and Moore in 1981. The
stringpreprocessing 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
stringpreprocessing 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 handwritten correctness proof using the PVS
theorem prover. The PVS proof can be found
here.
Related Publications:
 Besta, M. and F. Stomp:
A complete mechanization of a
correctness proof of a stringpreprocessing algorithm. In
Formal
Methods in System Design 27(12), pp. 527,
2005. 
 Stomp, F.:
Correctness of substringpreprocessing in BoyerMoore's
pattern matching algorithm. In Theoretical
Computer Science 290(1), 5978, 2003. 
 Besta, M. and F. Stomp:
Mechanization of a proof of a stringpreprocessing in
BoyerMoore's pattern matching algorithm. In
Proceedings of the 8^{th}
International Conference on Engineering of Complex Computer
Systems (ICECCS '02), pp. 6877, IEEE CS, December 2002,
Greenbelt, MD.


