Research

Members
Research
Meetings
Publications
Contact Info

Our research is in the area of Formal Software Verification. We use formal logics to specify software systems and to prove the correctness of such systems, or to show that a system does not satisfy its specification. In the latter case, the software system has to be corrected and the correction has to be proved correct. Part of our work is also in formulating proof rules for reasoning about systems so that the intuitive explanations of their designers can be captured naturally in the formal reasoning.
 
Self-Stabilization

Distributed and parallel algorithms are usually complicated. Many of them are used in safety critical applications, e.g., in avionics, transportation, and e-commerce. Self-stabilization ensures that distributed and parallel algorithms are resilient to transient failures: A self-stabilizing algorithm eventually always exhibits correct behavior after the last transient error has occurred. We investigate correctness of self-stabilizing algorithms.
 
Evolving Systems

Recently we have also started to investigate correctness of evolving systems. That is, if one version of a system is replaced by another version of that system and the specification is changed, can parts of an earlier correctness proof be re-used?
 
Register Constructions

Except for self-stabilization and evolving systems, we also focus on implementation of different register constructions. The algorithms, although short in description, are complicated. We work on correctness proofs of those algorithm. We also plan to mechanize those proofs using the PVS theorem prover.
 
Boyer-Moore's String Preprocessing Algorithm

The Boyer-Moore's pattern matching algorithm utilizes two preprocessing algorithms: one based on single characters only and the other based on a string. The string-preprocessing algorithm is complicated. A number of researchers have found several errors in that preprocessing algorithm. We have identified another minor error in recently published versions of the string-preprocessing algorithm and corrected it. We have given a correctness proof of the corrected version and we have mechanically verified the hand-written correctness proof using the PVS theorem prover. The PVS 2.3 proof can be found here.
 

Home | Members | Research | Meetings | Publications | Contact Info

For problems or questions regarding this web contact besta@cs.wayne.edu.
Last updated: 09/05/04.