|
|
| 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:
|
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:
 | Besta, 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. |
| Besta, M: Self-stabilizing ℓ-exclusion: A correctness proof.
Dissertation, Wayne State University, Detroit, MI, 2005. |
| Besta, M:
Self-stabilizing ℓ-exclusion: A correctness proof.
Dissertation prospectus, Wayne State University, Detroit,
MI, 2002. |
| Abraham, 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:
| Besta, 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. |
| Stomp, F.:
Correctness of substring-preprocessing in Boyer-Moore's
pattern matching algorithm. In Theoretical
Computer Science 290(1), 59-78, 2003. |
| Besta, 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.
|
|
|
