|
| |
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.
|
|
|
