アイテム詳細

要旨

Program verification increases the degree of confidence that a program will
perform correctly. Manual verification is an error-prone and tedious task. Its
automation is highly desirable. The verification methodology reduces the
reasoning about temporal properties of program computations to testing the
validity of implication between auxiliary
first-order assertions. The synthesis of such auxiliary assertions is the main
challenge for automated tools. There already exist successful tools for the
verification of safety properties. These properties require that some �bad�
states never appear during program computations. The tools construct
invariants, which are auxiliary assertions for safety. Invariants are computed
symbolically by applying techniques of abstract interpretation. Liveness
properties require that some �good� states will eventually appear in every
computation. The synthesis of auxiliary assertions for the verification of
liveness properties is the next challenge for automated verification tools.
This dissertation argues that transition invariants can provide a new basis for
the development of automated methods for the verification of liveness
properties. We support this thesis as follows. We introduce a new notion of
auxiliary assertions called transition invariant. We apply this notion to
propose a proof rule for the verification of liveness properties. We provide a
viable approach for the automated synthesis of transition invariants by
abstract interpretation, which automates the proof rule. For this purpose, we
introduce a transition predicate abstraction. This abstraction does not have an
inherent limitation to preserve only safety properties.
Most liveness properties of concurrent programs only hold under certain
assumptions on non-deterministic choices made during program executions. These
assumptions are known as fairness requirements. A direct treatment of fairness
requirements in a proof rule is desirable. We specialize our proof rule for the
direct accounting of two common ways of specifying fairness. Fairness
requirements can be imposed either on program transitions or on sets of
programs states. We treat both cases via abstract-transition programs and
labeled transition invariants respectively.
We have developed a basis for the construction of automated tools that can not
only prove that a program never does anything bad, but can also prove that the
program eventually does something good. Such proofs increase our confidence
that the program will perform correctly.