Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
This thesis takes up the challenge of formal specification and verification of concurrent programs with shared memory. To this end, we use the logic Rely-Guarantee Interval Temporal Logic (RGITL) that has been natively implemented in the interactive theorem prover KIV. The logic incorporates several techniques that make the verification of such concurrent programs more tractable. In particular, temporal logic makes it possible to intuitively specify both safety and liveness requirements for these programs. Moreover, compositional reasoning breaks down the verification of a property of a concurrent program into smaller proof obligations that must be shown for the constituent subprograms. We mechanically derive various rely-guarantee rules for the compositional verification of partial/total correctness and absence of deadlock of concurrent programs in RGITL. Moreover, we evaluate the practical use of the logic in the domain of highly concurrent data structure implementations: We derive novel compositional proof methods for the central safety/liveness conditions of linearizability and lock-freedom. Finally, we show the application of our methods to verify a number of intricate data structure implementations correct.