Programmverifikation

Dieses Buch bietet als erstes Lehrbuch eine systematische
Einf}hrung in die Programmverifikation. Sequentielle,
parallele und verteilte Programme werdenin einheitlicher
Weise behandelt.
In den einzelnen Kapiteln des Buches werden deterministische
und nichtdeterministische Programme, Programme mit
gemeinsamen Variablen und verteilte Programme mit
Kommunikation }berBotschaftenaustausch behandelt. F}r jede
dieser Programmklassen werden eine operationelle Semantik,
Syntax-gerichtete Verifikationsregeln mitsamt
Korrektheitsbeweis und ein gr|~eres Verifikationsbeispiel
vorgestellt. Insbesondere werden Programme zur L|sung der
klassischen Probleme Erzeuger-Verbraucher, wechselweiser
Ausschlu~ und verteilte Terminierung diskutiert und
verifiziert. Eine Besonderheit desBuches ist die
einheitliche Behandlung von Fairne~-Annahmen und die
Benutzung von Programmtransformationen.
Das Buch eignet sich f}r ein- oder zweisemestrige
Vorlesungen }ber Programmverifikation. Die Kapitel sind
einheitlich strukturiert und enthalten eine Reihe von
]bungsaufgaben und bibliographischen Hinweisen. Das Buch
f}hrt auch an aktuelle Themen der Forschung heran.