Die Active Group und "Agentic Engineering"

23.06.2026 von Michael Sperber

In den letzten Monaten haben wir - wie alle in der Branche - viele Gespräche dazu geführt, wie die Zukunft der Softwareentwicklung aussehen wird. Es geht natürlich um „Agentic Engineering“ (AE), also der Benutzung von LLM-basierenden Agenten, um direkt aus Anforderungen den Code für Softwaresysteme zu generieren. Neben der allgemeinen Frage haben wir uns überlegt, was diese Entwicklung für uns bei der Active Group bedeutet und wie wir mit den veränderten Rahmenbedingungen umgehen.

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.