Die Entwicklung beweisbar korrekter Software ist eines der wichtigsten Ziele des Software-Engineering. Für einen Korrektheitsnachweis sind einerseits die Anforderungen, gemäß deren sich die Software verhalten soll, formal zu spezifizieren und andererseits das Verhalten der Software in einem adäquaten semantischen Modell zu erfassen. Die Vorlesung legt die mathematischen Grundlagen für die Spezifikation und die Semantik von sequentiellen Programmen, stellt Beweismethoden und ihre Umsetzung in einem Theorembeweiser vor und gibt eine Einführung in die methodische Entwicklung korrekter sequentieller Programme.
