Die Entwicklung moderner, die aktuelle Forschung widerspiegelnder Werkzeuge zur automatischen Verifikation ist damit eine zentrale Aufgabe in unserer Gruppe. Herauszustellen sind dabei die folgenden Entwicklungen:
- In Zusammenarbeit mit dem DFKI Saarbrücken wurde das INKA-System, ein Beweiswerkzeug, das einen vor allem auf Induktion gestützten Kalkül und zahlreiche leistungsfähige Heuristiken beinhaltet, entwickelt. Als eines der Hauptbestandteile ist es in das VSE-System (Verification Support Environment) integriert worden und steht damit für einen industriellen Einsatz zur Verfügung.
- Gegenwärtig entwickeln wir das Verifikationswerkzeug VeriFun, welches sich aufgrund einer leistungsfähigen Automatisierungskomponente einerseits und der Möglichkeit zur Interaktion und damit zur gezielten Steuerung des Beweisprozesses andererseits auszeichnet.Besondere Schwerpunkte bei der Entwicklung lagen auf der Gestaltung einer klar strukturierten, auch didaktisch geeigneten Oberfläche, auf einer einfach portierbaren Implementierung (in Java) und einem leicht verständlichen und variablen Konzept und Kalkül, ohne dabei auf heute bereits erreichbare Leistungsfähigkeit zu verzichten. Das VeriFun- System wird sowohl in der Lehre als auch in den Forschungsprojekten eingesetzt.
- Im Projekt Lernender Beweiser werden Verfahren des Maschinellen Lernens in Beweissysteme eingebunden. Das System Plagiator dient hierzu als Testplattform. Aufgrund seiner Lernkomponente ist es in der Lage, für ein neues Beweisziel einen geeigneten, bereits berechneten Beweis zu finden und zu übertragen, bzw. – wenn dies nicht gelingt – den Benutzer beim interaktiven Nachweis der Aussage zu unterstützen und den Beweis für nachfolgende Aufgaben in einer Bibliothek abzuspeichern.
