Previous Research
Updated 05/25/08
Photo Album
Contact Me


This page gives an overview of the research projects I have been involved while in the graduate school. The projects are sorted according to the institution where the projects took place. For details about my current projects, please visit my current research web page. If you need more information about my previous research projects, feel free to contact me via e-mail.
Wayne State University, Detroit, Michigan

Since Fall 2000 I worked on my Ph.D. degree in Computer Science under the supervision of Dr. Frank Stomp. My research focused on Formal Methods and verification of algorithms and their correctness proofs. I was involved in several projects:

bulletA Proof of an Atomic Register Construction (2002-2005)
An implementation of an atomic bit register was published recently. The algorithm, although short in description, is complicated. This project was aimed at investigation of correctness of that algorithm. We developed a correctness proof of the algorithm and worked on mechanization of the proof using the PVS theorem prover.
bulletA Formal Proof of a Self-Stabilizing ℓ-Exclusion Algorithm (2001-2004)
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 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.: Self-Stabilizing ℓ-Exclusion: A Correctness Proof. Dissertation, Wayne State University, Detroit, MI, June 2005.
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 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.

bulletBoyer-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.
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.
bulletStomp, F.: Correctness of substring-preprocessing in Boyer-Moore's pattern matching algorithm. In Theoretical Computer Science 290(1), 59-78, 2003.
Charles University, Prague, Czech Republic

In Fall 1997 I started working on my Ph.D. degree under the supervision of Dr. Frantisek Plasil. During my stay at the Department of Software Engineering I worked on

bulletBehavior Protocols (1998-2000)
Nowadays most of software products are built from software components. A component is described by a set of interfaces providing services to clients and a set of interfaces requesting services from other components. Larger components are assembled from smaller components. Architectures of assembled components are described by means of an architecture description language. It is desirable to describe not only component architecture, but also component collaboration, i.e., component behavior. We conducted research to enhance an architecture description language with a description of component behavior. You can read more about behavior protocols here.

Related Publications:
bulletPlasil, F., S. Visnovsky, and M. Besta: Bounding component behavior via protocols. In Proceeding of Technology of Object-Oriented Languages and Systems (TOOLS 30), pp. 387-398, IEEE CS, August 1999, Santa Barbara, CA.
bulletPlasil, F. and S. Visnovsky: Behavior protocols for software components. In IEEE Transactions on Software Engineering 28(11), 1056-1076, 2002.
Palacky University, Olomouc, Czech Republic

I received my Bachelor and Master's degrees in Computer Science from Palacky University in Olomouc. During my studies in the Department of Computer Science, I worked under the supervision of Dr. Vladimir Sklenar and was involved in three research projects. Their brief descriptions is below:

bulletAbstract Data Views (1994-1996)
My Master thesis research was on a new programming concept called Abstract Data Views (ADV). This is a design and implementation mechanism providing clean separation of the user interface from the application at both the design and implementation level. This concept can be used not only for graphical presentation of the application state, but also as a means of communication among (distributed) components.

Related Publications:
bulletBesta, M.: Abstract Data Views. Master's thesis, Palacky University, Olomouc, Czech Republic, May 1996.

bulletALVIS - Algorithm Visualization (1993-1995)
In order students better understand design principles of new algorithms it is convenient to employ a demonstration tool. In the course of this project we implemented a sophisticated tool that allowed one to design a visual demonstration of an arbitrary algorithm. We implemented language interpreters of several programming languages and many data and program view components to allow for visualization and interaction between a user and the tool.

Related Publications:
bulletSklenar, V., M. Kudelka, and V. Snasel: A Software Tool for Visualization of Algorithms. In Proceedings of Computer Based Learning in Science (CBLIS '95), Opava, Czech Republic, July 1995. (ISBN 80-901974-0-X)

bulletNormal Forms of Context-Free Grammars (1992-1993)
In this project we implemented a tool for transformation of context-free grammars into Chomsky and Greibach Normal Forms. The tool offers a user interface to allow for demonstration of transformation steps that have to be taken during execution of the transformation algorithms. You can download the project archive here (in Czech).

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