The 4th Confluence Competition (CoCo 2015) is over. Three confluence tools and one certifier that are developed at CL participated and won several categories (results).
Confluence is one of the central properties of programs since it ensures uniqueness of computation results. Numerous results have been obtained on proving confluence of rewrite systems, lambda calculi, etc. and recently, several automatic tools for (dis)proving confluence have been developed. CoCo aims to foster the development of techniques for (dis)proving confluence automatically by setting up a dedicated competition among confluence tools.
CoCo 2015 was collocated with CADE-25 and ran live during the International Workshop on Confluence (IWC 2015) in Berlin. Previous editions of the competition were held in Nagoya (2012), Eindhoven (2013) and Vienna (2014).
In 2015 there have been four competition categories:
confluence of first-order term rewrite systems (TRS)
confluence of conditional term rewrite systems (CTRS)
certification (CPF)
confluence of higher-order term rewrite systems (HRS)
and tools from Innsbruck participated and won in all of them:
CSI won the TRS category (draw with ACP)
ConCon was the most powerful tool for CTRSs
The certifier CeTA in combination with CSI won the category for certified confluence proofs
CSI^ho was the strongest tool in the higher-order category
All these tools are open source.
- Details
- Category: News Archive
Bertram Felgenhauer successfully defended his thesis on theoretical and automation aspects of confluence of term rewriting systems. He will continue his research on the project “From Confluence to Unique Normal Forms: Certification and Complexity”.
- Details
- Category: News Archive
CL congratulates Sarah Winkler to her internship at Microsoft Research Cambridge and Maria Schett to her internship at the IBM Thomas J. Watson Research Center.
- Details
- Category: News Archive
Akihisa works as a researcher on the project “Certifying Termination and Complexity Proofs of Programs.“
- Details
- Category: News Archive
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).
- Details
- Category: News Archive
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.
- Details
- Category: News Archive
The CL member Michael Färber will be awarded with the Prix de la France 2014 for his master’s thesis on the topic “Complexity of Equivalence Proofs of Simple Deterministic Grammars”.
The award ceremony will take place on December 3, 18h at Claudiana, Innsbruck.
- Details
- Category: News Archive
In its assembly at the beginning of March the board of the Austrian Science Fund (FWF) accepted Martin Avanzini’s proposal on “Complexity Analysis of Higher-Order Rewrite Systems”. The volume of this Schrödinger fellowship is EUR 143K.
The aim of this project is to advance techniques for the static resource analysis of programs. Limited computational resources, such as memory and execution-time, render resource analysis a central topic in software verification. In his project, Martin Avanzini will focus on higher-order rewrite systems, one of the most general formal models of functional programming languages such as OCaml and Haskell.
Martin Avanzini will conduct a large part of his research during his 2 year stay at the University of Bologna before returning back to Innsbruck for a final year.
- Details
- Category: News Archive
The Computational Logic group just returned from the Vienna Summer of Logic, which was held in Vienna from July 9 until July 24.
With about 2500 participants in 12 large conferences, 82 workshops, and 14 tool competitions it is the largest event in the history of logic.
In 20 talks the Computational Logic group presented its eight conference and twelve workshop papers. Furthermore the tools developed in the group participated in three different competitions, took various first places, and were awarded three of the prestigious Kurt Gödel silver medals. Apart from numerous PC memberships, two workshops and one competition have been organized by CL members.
Pictures:
- Details
- Category: News Archive
Today Michael successfully defended his master thesis on “A Complexity Preserving Transformation from Jinja Bytecode to Rewrite Systems”. Michael will enroll in the PhD program in Innsbruck and becomes a research assistant of CL.
- Details
- Category: News Archive
Last Friday Thiemann could convince the international START-/Wittgenstein-Jury of his project “Certifying Termination and Complexity Proofs of Programs”. As a result, his 6-year project is now sponsored by the FWF by more than 1,000,000 EUR.
About the project:
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.
- Details
- Category: News Archive