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

Certification Redux – FWF Project approved

Christian Sternagel’s project proposal, extending current certification techniques for term rewriting, was approved by the Austrian Science Fund (FWF) in its 51st board meeting. The project has a duration of 3 years and the grant amount is EUR 334K.

In the recent past, certification is very successful in the area of automated termination and confluence proving as well as completion (where certification means the automatic and reliable verification of proofs that were generated by untrusted tools).

The aim of this project is to extend the existing IsaFoR/CeTA project as follows: formalize the recently introduced weighted path order and extend it to rewriting modulo associativity and commutativity (AC-rewriting); support certification of conditional confluence proofs; and formalize the theory of AC-rewriting, AC-unification, and normalized completion. This will bring CeTA up to speed with the most recent tool developments of termination tools (ttt2), confluence tools (csi), and completion tools (mkbtt).

Links:

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

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

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

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

(Christian Sternagel)

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 project “From Confluence to Unique Normal Forms: Certification and Complexity” approved

Aart Middeldorp’s project proposal on confluence and the related unique normal form property of rewrite systems was approved by the Austrian Science Fund (FWF) in its 51st board meeting. The project has a duration of 3 years and the grant amount is EUR 437K.

In the preceding years many powerful confluence methods have been developed and implemented in confluence tools that participate in the recently established confluence competition. Important first steps towards certification have been made, but much remains to be done. The aim of this project is to fill two important gaps concerning certification, investigate methods for the unique normal form property, study various complexity issues related to confluence and unique normal forms, and further develop the confluence tool CSI and the certification tool CeTA for confluence.

(Aart Middeldorp, 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


Foto: 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