Tag Archives: Computational Logic

informatik-bilderleiste-02

Österreichs LogikerInnen vernetzen sich

Vor kurzem fand im Universitätszentrum Obergurgl der Universität Innsbruck der Helmut Veith Memorial Workshop (HVW) statt. Vom 31. Jänner bis 02. Februar 2017 trafen sich Österreichs LogikerInnen um im Namen von Helmut Veith, dem vor einem Jahr verstorbenen führenden Logiker und Computerwissenschaftler, die Vernetzung voranzutreiben.

Teamfoto des HVW 2017 in Obergurgl © Georg Moser
Teamfoto des HVW 2017 in Obergurgl © Georg Moser

Veith ist es gelungen Österreich zum weltweiten Zentrum der Verifikation zu machen. Die Verifikation bezeichnet die automatisierte Korrektheitsanalyse von Software, welche zusehends an Bedeutung gewinnt, da die IT geradezu alle Lebensbereiche durchdringt. Methode dieser Forschung ist die Logik, die “lingua franca” der Computerwissenschaft.

Renommierte Gastredner sprachen in ihren Beiträgen über grundlegenen Überlegungen zur Logik sowie über die Entwicklung industriell verwertbarer Verifikationswerkzeuge. Moshe Vardi, Professor an der Rice University in Texas, ist Editor der “Communication of the ACM”, der weltweiten Vereinigung von IT Fachkräften und darüberhinaus für seine klarsichtigen Beiträge zur Auswirkung der Automatisierung auf unseren Arbeitsmarkt bekanne. Erich Grädel, Professor der RWTH Aachen, ist Spezialist der endlichen Modelltheorie, Herausgeber u.a. des Journals “Mathematical Logic Quarterly” und veröffentliche mehrere Bücher zur Logik, Spiel- und Entscheidungstheorie.

Der erfolgreiche Workshop wurde von assoz. Prof. Dr. Georg Moser, Computation with Bounded Ressources, Computational Logic, geleitet. Der nächste HVM-Workshop wird 2018 in Salzburg stattfinden.

Links:

http://cbr.uibk.ac.at/events/hvw/
http://cbr.uibk.ac.at

(Gabriele Strasser, Georg Moser)
informatik-bilderleiste-02

Softwaresicherheit gewährleisten – Zertifizierung Redux

Kürzlich wurde das von Dr. Christian Sternagel eingereichte Projekt “Zertifizierung Redux” vom Fonds zur Förderung der wissenschaftlichen Forschung (FWF) bewilligt. Im Rahmen dieses Projektes werden Programme entwickelt, die Softwaresicherheit überprüfen.

Damit Programme fehlerfrei funktionieren, sind sogenannte Zertifizierer zur Überprüfung notwendig. So ein Zertifizierungsprogramm ist das in der Forschungsgruppe Computational Logic entwickelte Programm CeTA. Das Projekt von Christian Sternagel hat zum Ziel, CeTA um neue Techniken zu erweitern.

Das Projekt Zertifizierung Redux wird mit 334.000 Euro gefördert und hat eine Laufzeit von 3 Jahren. Zum Abstract

Die Forschungsgruppe Computational Logic (CL) am Institut für Informatik ist sehr erfolgreich im Bereich Termersetzung und Zertifizierung. Der Informatiker René Thiemann erhielt 2014 den START-Preis des FWF für seine Forschung “Zertifizierte Terminierung und Komplexität von Programmen”. Im Rahmen des “Vienna Summer of Logic” holten sich die LogikerInnen der Universität Innsbruck drei der begehrten Kurz-Gödel-Medaillen ab.

Weiterführende Links:

Webseite Christian Sternagel: http://cl-informatik.uibk.ac.at/users/griff/

Forschungsgruppe Computational Logic (CL): http://cl-informatik.uibk.ac.at/

Presseberichte:
http://www.uibk.ac.at/public-relations/presse/archiv/2014/542/

http://www.uibk.ac.at/ipoint/blog/1225856.html

(Gabriele Strasser)

Abstract Projekt Zertifizierung Redux

Abstract Projekt Zertifizierung Redux

Termersetzung ist ein einfaches aber dennoch ausdrucksstarkes Berechenbarkeitsmodel, welches zu großen Teilen der deklarativen Pogrammierung sowie dem computerunterstützen Beweisen zu Grunde liegt. Außerdem gibt es Methoden welche die Verifikation von Computerprogrammen auf das Nachweisen bestimmter Eigenschaften von entsprechenden Termersetzungssystemen reduzieren.

Die beiden wohl wichtigsten Eigenschaften in der Termersetzung sind Konfluenz und Terminierung. Während Terminierung sicherstellt dass es keine Endlosschleifen gibt, garantiert Konfluenz das Berechnungen deterministisch in dem Sinne sind, dass beliebige zwei Berechnungspfade stets wieder vereint werden können. Zusammen implizieren diese beiden Eigenschaften, dass man unabhängig von der gewählten Auswertungsstrategie stets das selbe Resultat für die selbe Eingabe erhält. Terminierende und konfluente Systeme von Ersetzungsregeln sind von besonderem Interesse, da sie Entscheidungsverfahren für ihre jeweilige Gleichungstheorie liefern (wenn man wissen will ob zwei Terme äquivalent sind, muss man diese nur vollständig mit Hilfe der Ersetzungsregeln reduzieren und anschließend auf syntaktische Gleichheit überprüfen). Die sogenannte Vervollständigung, stellt eine Möglichkeit dar um eine gegebene Menge von Gleichungen in eine äquivalente Menge von terminierenden und konfluenten Ersetzungsregeln umzuwandeln.

Seit Kurzem ist die Zertifizierung von automatischen Terminierungs- und Konfluenzbeweisen äußerst erfolgreich. Wobei wir mit Zertifizierung die automatische und zuverlässige Verifikation von Beweisen meinen, welche von einem beliebigen externen Programm generiert wurden (z.B. einem automatischen Terminierungs-, Konfluenz-, oder Vervollständigungsprogramm). Der vorherrschende Ansatz in der Zertifizierung kann in zwei Phasen eingeteilt werden: Zuerst formalisiert man die zu Grunde liegende Theorie und die Techniken welche von dem externen Programm verwendet werden mit Hilfe eines Beweisassistenten (z.B. Isabelle/HOL). Danach stellt man für einen gegeben Beweis, der von solch einem Programm erstellt wurde, sicher, dass alle verwendeten Techniken korrekt angewandt wurden. In der ersten Phase überprüft man also, dass die mathematischen Grundlagen der genutzten Techniken im Allgemeinen korrekt sind und dass keine impliziten Annahmen übersehen wurden. In der zweiten Phase stellt man die korrekte Anwendung dieser Techniken auf ein konkretes Problem sicher.

Einer der verfügbaren Zertifizierer ist unser Programm CeTA, das automatisch aus unserer Isabelle Formalisierung der Ersetzungstheorie (IsaFoR) generiert wird. Unsere Hauptprojektziele umfassen die folgenden Erweiterungen von IsaFoR und CeTA: (1) Eine Formalisierung der kürzlich vorgestellten Weighted Path Order (WPO). Weiters soll diese auf den Fall von Ersetzung modulo Assoziativität und Kommutativität erweitert werden. (2) CeTA-Unterstützung für Konfluenzbweise von konditionalen Ersetzungssystemen. (3) Eine Formalisierung von Ersetzung und Unifikation modulo Assoziativität und Kommutativität, sowie die Unterstützung sogenannter normalisierter Vervollständigungsbweise durch CeTA.

Das Erreichen dieser Ziele wird CeTA auf den neuesten Stand bezüglich der jüngsten Entwicklung von Terminierungs-, Konfluenz-, und Vervollständigungsprogrammen bringen.

informatik-bilderleiste-02

FWF-Projekt “Von Konfluenz zu eindeutigen Normalformen: Zertifizierung und Komplexität” genehmigt

Das FWF-Projekt unter der Leitung von Univ.-Prof. Dr. Aart Middeldorp befasst sich mit Konfluenz und der verwandten Eigenschaft eindeutiger Normalformen in Termersetzungssystemen. In den letzten Jahren wurden viele mächtige Methoden für Konfluenz entwickelt und in Konfluenzbeweisern implementiert, welche an dem kürzlich etablierten Konfluenzwettbewerb teilnehmen. Es wurden auch erste Schritte in Richtung automatischer Zertifizierung unternommen, aber dort bleibt viel zu tun. Das Ziel dieses Nachfolgeprojektes ist es, zwei wichtige Lücken bei der Zertifizierung zu füllen, Methoden für Eindeutigkeit von Normalformen zu untersuchen, und Komplexitätsaspekte von Konfluenz und Eindeutigkeit von Normalformen zu betrachten. Weiterhin werden wir das Konfluenzbeweiser CSI sowie den Zertifizierer CeTA für Konfluenz weiterentwickeln. Im Einzelnen sind die Ziele

1. das „layer-framework“ zu formalisieren, welches wichtige Resultate für die Zerlegung von Konfluenzproblemen in Teilprobleme wie z.B. Modularität und Persistenz erfasst,

2. eine Formalisierung des Beweises für Konfluenz von „development-closed“ links-linearen Ersetzungssystemen auf der Basis von Beweistermen und Residuentheorie zu entwickeln,

3. Techniken im Zusammenhang mit „conditional linearization“ wie den Satz von Chew zu erforschen, um automatisierbare Kriterien für die Eindeutigkeit von Normalformen zu finden,

4. (praktisch) entscheidbare Klassen für Konfluenz und eindeutige Normalformen sowie die Komplexität von Suchproblemen im Zusammenhang konkreter Konfluenzmethoden zu untersuchen,

5. und die so gewonnen Erkenntnisse zu nutzen um die Stärke und Effizienz des Konfluenzbeweisers CSI sowie des automatischen Zertifizierers CeTA für Konfluenz zu verbessern.

(René Thiemann, CL)
ifi

START-Programme Award for Computer Scientist at the University of Innsbruck

René Thiemann, computer scientist at the University of Innsbruck received the START-Programme Award, the most prestigious award for young researchers in Austria. René Thiemann’s project deals with the improvement of programs. His aim is to extend the application of Certifiers in regard to reliability and complexity.

Priv.-Doz. Dr. René Thiemann
Priv.-Doz. Dr. René Thiemann

Computer programs become ubiquitous in our world: they are used to manage our money, to control activities in vehicles, and to interact with medical equipment. Therefore, it is of vital importance that programs behave correctly. Here, termination (all computations produce a result) and complexity (how long does it take to get the result, and how much memory is required) are fundamental properties of programs. Unfortunately, these fundamental properties are undecidable. For example, it is not possible to design an analyzer-program which decides for each other program, whether it terminates or not. Nevertheless, much work has been spent on the development of such analyzers which are often (but not always) able to guarantee the property of concern.
Whereas the answer to an analysis for a given program might be simple (yes, the program is terminating), the underlying argument for this answer, i.e., the proof, is usually not that simple. In fact, most analyzers for complexity and termination are complex programs, which combine several techniques while trying to analyze the behavior of a program. Consequently, these analyzers may contain errors and give wrong answers and proofs.
One solution to this problem is the usage of certifiers, which can check the proofs that are generated by the tools. For reliability, the soundness of the certifiers itself has to be formally proven within a theorem prover. This is a challenging and time-consuming task, but it is also rewarding: With the help of the certifiers, several bugs have been spotted, both in the implementations of the analyzers, as well as in soundness proofs of termination techniques which are utilized by the analyzers. Unfortunately, so far the applicability of the available certifiers in this area is rather limited: they mainly handle termination proofs, but not complexity proofs; and they are limited to term rewriting, a simple programming language which can be seen as the foundation of functional programming languages, but which is more of theoretical interest due to its simplicity.
In this project, we will extend the applicability of certifiers in two important directions: we want to support a large class of complexity proofs, and we want to support termination proofs for two real programming languages, Java and Haskell. To this end, we will develop several interesting formalizations. This includes a large library on linear algebra, which will be required for dealing with complexity proofs. Moreover, we will develop a formalized semantics for Haskell and we will extent the existing formalization on Jinja towards Java. (Jinja is a restricted version of Java where certain language constructs are missing.) Our work will drastically improve the reliability of current termination and complexity tools. Furthermore, it can serve as a starting point for performing other formalizations in the area of program analysis and program transformations.

Priv.-Doz. Dr. René Thiemann

René Thiemann was born in Stadtlohn (Nordrhein-Westfalen) in 1976. After studing and receiving his PhD at the RWTH Aachen he moved to Innsbruck to work at the Institute of Computer Science at the University of Innsbruck in 2007. Im July 2014 he received his Habilitation for his work „A Formalization of Termination Techniques in Isabelle/HOL“.

START-Programme Award from the Austrian Science Foundation

The START Programme is the most prestigious award directed at young researchers in Austria. For the coming six years the awardees can plan their reserach activities in a sound financial environment which enables them to establish their own reserach groups. A total of 8 START-Programme Awards were awarded in Austria this year – three of them go to researchers at the University of Innsbruck – the Mathematician Karin Schnass and the Micro Biologist Sigrid Neuhauser.

Links:

http://cl-informatik.uibk.ac.at/news/june-16-2014-cl-member-rene-thiemann-is-entering/
http://www.uibk.ac.at/public-relations/presse/archiv/2014/542/
http://derstandard.at/2000002048994/Josef-Penninger-gewinnt-den-Wittgenstein-Preis