 
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.
SelfStabilization
Distributed and parallel algorithms are usually complicated. Many of
them are used in safety critical applications, e.g., in avionics,
transportation, and ecommerce. Selfstabilization ensures
that distributed and parallel algorithms are resilient to transient
failures: A selfstabilizing algorithm eventually always exhibits
correct behavior after the last transient error has occurred. We
investigate correctness of selfstabilizing 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 reused?

Register Constructions
Except for selfstabilization 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.

BoyerMoore's String Preprocessing
Algorithm
The BoyerMoore's pattern matching algorithm utilizes two
preprocessing algorithms: one based on single characters only and
the other based on a string. The stringpreprocessing 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 stringpreprocessing algorithm and corrected it. We have given a
correctness proof of the corrected version and we have mechanically verified the handwritten
correctness proof using the PVS theorem prover. The PVS 2.3 proof can be
found
here.


