Petrinetze sind ein weit verbreitetes Werkzeug zur Modellierung und Verifikation sequentieller und verteilter Systeme. Als graphisches Modell überzeugen sie durch Anschaulichkeit und Verständlichkeit und kommen daher auch in vielen Bereichen außerhalb der Informatik zum Einsatz. Der Fokus dieser Lehrveranstaltung liegt auf dem Einsatz von Petrinetzen als Tool für die Verifikation. Nach einer Einführung in Petrinetze als Modellierungswerkzeug, werden wir uns mit verschiedenen Analysemethoden auf Petrinetzen beschäftigen. Dazu betrachten wir verschiedene für die Verifikation wichtige Fragestellungen, wie Terminierung und Lebendigkeit, und diskutieren Techniken mit denen diese Eigenschaften auf Petrinetz-Modellen analysiert werden können.