Verifikation von Algorithmen mit Z3 – Teil 3

15.05.2026 von Markus Schlegel

Im ersten Artikel dieser Reihe hatten wir den SMT-Solver Z3 kennen gelernt und uns allgemeine Gedanken zu Spezifikation und Verifikation gemacht. Im zweiten Artikel haben wir den sogenannten Bresenham-Algorithmus – eine Berechnungsvorschrift zum Zeichnen von geraden Linien – mit Z3 implementiert und dann auch sichergestellt, dass dieser Algorithmus genau das tut, was wir von ihm erwarten. Die Implementierung des Bresenham-Algorithmus in Z3 ist zwar lauffähige Software, allerdings ist Z3 (bzw. SMT-LIB2) keine Allzweckprogrammiersprache, d.h. wir werden kein umfängliches Softwareprojekt komplett in Z3 schreiben können. War also alles letztlich doch für die Katz?

Verifikation von Algorithmen mit Z3 – Teil 2

20.03.2026 von Markus Schlegel

Im ersten Artikel dieser Reihe hatten wir den SMT-Solver Z3 kennen gelernt. Wir hatten in der zugehörigen Sprache SMT-LIB-2 eine Spezifikation für die Rasterisierung von Geraden verfasst und dann einen verbesserten Algorithmus entworfen, der mit dem Simplen in seiner Funktionsweise übereinstimmt. Während die Korrespondenz dieser beiden Algorithmen manchen Lesern vielleicht noch offensichtlich erschien, gehen wir in diesem Artikel einen signifikanten Schritt weiter. Wir implementieren den sog. Bresenham-Algorithmus, bei dem auf den ersten Blick ganz und gar nicht mehr klar ist, warum er überhaupt funktioniert.

Softwarearchitektur-Schulungen 2026

08.03.2026 von Michael Sperber

Dies ist ein Post in eigener Sache. Wir (also die Active Group GmbH, Betreiberin dieses Blogs) bieten zahlreiche iSAQB-akkreditierte Schulungen zur Softwarearchitektur an. Dazu gehören Grundlagenschulungen und die fortgeschrittenen Themen Funktionale Softwarearchitektur, Domänenspezifische Sprachen und Formale Methoden.

Hier ist ein Überblick über unser Angebot im Jahr 2026.

Verifikation von Algorithmen mit Z3 – Teil 1

10.02.2026 von Markus Schlegel

Ein Algorithmus soll effizient Lösungen zu gegebenen Problemen berechnen. In der Praxis besteht das Argument, dass der Algorithmus auch die richtigen Lösungen berechnet, meist aus einer Menge von Testfällen, einer kurzen Rechtfertigung in natürlicher Sprache oder einem Stoßgebet. Selbst eine große Menge von Testfällen – auch wenn diese bspw. mithilfe von QuickCheck erstellt wurden – kann aber keine Aussage über die allgemeine Korrektheit eines Softwarestücks machen. Um wirklich sicher zu gehen, müssen wir die Struktur des Codes betrachten, darüber Aussagen treffen und formal argumentieren, dass diese Aussagen auch allgemeine Geltung haben. Ein Mittel, um das zu tun, lernen wir in dieser dreiteiligen Artikelserie kennen: Wir nutzen den SMT-Solver Z3 als automatisierten Theorembeweiser. Diese Artikel sollen einen ersten Einblick geben in die Inhalte unserer neuen iSAQB-Advanced-Level-Schulung zu Formalen Methoden. In der Schulung kommen neben Z3 weitere Verifikationswerkzeuge wie VeriFast, Forge und Liquid Haskell zur Sprache.

Das Programm für die BOB 2026 am 13.3. steht!

12.12.2025 von Michael Sperber

Das Programm der Hauskonferenz der Active Group, der BOB 2026, steht: Am Freitag, dem 13.3.2026, findet passenderweise die dreizehnte BOB statt – wie im letzten Jahr im Scandic-Hotel Potsdamer Platz.

Wir sind stolz auf das Programm, für dessen Entstehung wir allerdings viele tolle weitere Einreichungen ablehnen mußten.

Den Eröffnungsvortrag der BOB wird Stefan Kaufmann (stk) halten – es geht um Digitale Souveränität.

Es gibt wie gewohnt vier Tracks – zwei Tracks mit insgesamt 16 Vorträgen, zwei Tracks mit insgesamt 8 Tutorials.

Die Anmeldung ist eröffnet – der Early-Bird-Rabatt läuft noch bis 16. Januar 2026.