News Archive

May 2, 2018: CL welcomes Ralph Bottesch as new member

Ralph starts as a postdoc on the project Certifying Termination and Complexity Proofs of Programs. His expertise is on parametric complexity.

March 19, 2018: CL welcomes Max Haslbeck as new member

Max starts as a PhD-student on the project Certifying Termination and Complexity Proofs of Programs.

March 9, 2018: Julian Nagele defends his PhD thesis

Julian Nagele successfully defended his thesis on Mechanizing Confluence: Automated and Certified Analysis of First- and Higher-Order Rewrite Systems. He joined the School of Electronic Engineering and Computer Science at Queen Mary University of London as a postdoctoral research assistant.

December 15, 2017: Thomas Sternagel defends his PhD thesis

Thomas Sternagel successfully defended his thesis on automation, formalization, and certification of confluence of conditional term rewrite systems. He will leave for industry in January.

December 1, 2017: CL welcomes David Obwaller and Shawn Wang as new members

David starts as a PhD-student on the project Complexity Analysis-based Guaranteed Execution and Shawn is employed on the project SMART.

November 23, 2017: 3-year PhD student and postdoc position available

The Computational Logic research group at the University of Innsbruck has two open positions funded by the FWF (Austrian science fund) via the START project Certifying Termination and Complexity Proofs of Programs.


The project aims at increasing the reliability in current complexity and termination provers by independently checking the generated proofs. To this end, several analysis techniques will be formalized in the theorem prover Isabelle/HOL, with a focus on LLVM and integer transition systems.


For this project, we are looking for two enthusiastic researchers with a background in computational logic. Knowledge of automated termination analysis, complexity analysis, or theorem proving would be an asset. Candidates with a strong theoretical background in related areas are also encouraged to apply. The PhD-student candidate must have a Master’s or equivalent degree. Knowledge of German is not essential.


continue reading ...

November 8, 2017: CL welcomes Evan Marzion, Yutaka Nagashima and T. V. H. Prathamesh as new members

Evan and Yutaka work as researchers on the project Strong Modular Proof Assistance: Reasoning Across Theories and Prathamesh on the project FORTissimo: Automating the First-Order Theory of Rewriting.

September 8, 2017: CL Mini Seminar on Isabelle Tool Development

In a three day mini seminar from September 11 to September 13, Makarius Wenzel – the originator of the Isabelle proof language Isar and of Isabelle/jEdit – will tell us about Isabelle tool development with Isabelle’s derivatives of Standard ML and Scala.

June 1, 2017: FWF project “FORTissimo: Automating the First-Order Theory of Rewriting” approved

In its 63rd board meeting the Austrian Science Fund (FWF) approved Aart Middeldorp’s project proposal. The 3-year project will start on September 1 and has a grant amount of EUR 345K.

continue reading ...

May 18, 2017: PhD student or postdoc position available

We invite candidates for a PhD student or postdoc researcher position to start as soon as possible in the ongoing Certification Redux project. Click here for details.

September 15, 2016: Cezary Kaliszyk awarded ERC starting grant

CL is proud to announce that Cezary Kaliszyk’s project SMART: “Strong Modular proof Assistance: Reasoning across Theories” has been approved by the European Research Council. The project has a duration of 5 years and a total grant amount of EUR 1450K. The project will commence on March 1, 2017.

continue reading ...

September 12, 2016: Confluence Competition 2016

This month the 5th Confluence Competition (CoCo 2016) took place at CLA 2016 in Obergurgl. It ran live during IWC 2016. Four confluence tools and one certifier that are developed at CL participated and won several categories (results).

continue reading ...

September 12, 2016: Computational Logic hosts several international workshops

Between September 5 and 9, the international workshop on confluence, the international workshop on termination, the Austria-Japan workshop on rewriting, and the logic, complexity and automation project meeting have been conducted in the Obergurgl university center. With more than 50 presentations, eight invited speakers, two competitions, and nearly 70 international participants it was an exciting event, with ample discussion on new research areas as well as the strengthening and initiation of collaborations.

continue reading ...

April 8, 2016: ANR-FWF project “The Fine Structure of Formal Proof Systems and their Computational Interpretations” approved

The international cooperation project was approved by the French Science Fund (ANR) and the Austrian Science Fund (FWF). The project is carried out by a consortium of four partners, two Austrian and two French, all being internationally recognised for their work on structural proof theory, but each coming from a different tradition.
The project has a duration of 3 years and a total grant amount of EUR 630K. The project has started on January 1, 2016.

continue reading ...

February 5, 2016: Franziska Rapp completes her master studies

Today Franziska successfully defended her master thesis on “Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground TRSs”. Franziska will continue for a PhD and be employed on the FWF-funded project “From Confluence to Unique Normal Forms: Certification and Complexity“.

August 20, 2015: Termination Competition 2015

The Termination Competition 2015 is over. Five termination/complexity tools and one certifier developed by CL members participated and won in several categories (results).

continue reading ...

August 19, 2015: Confluence Competition 2015

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).

continue reading ...

April 30, 2015: Bertram Felgenhauer defends his PhD thesis

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”.

April 27, 2015: Sarah Winkler MS Research & Maria Schett IBM

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.

April 21, 2015: Harald Zankl completes his habilitation procedure

Harald Zankl’s research is concerned with the automated analysis of programs.

continue reading ...

April 1, 2015: CL welcomes Akihisa Yamada as new member

Akihisa works as a researcher on the project “Certifying Termination and Complexity Proofs of Programs.“

January 22, 2015: FWF project “Certification Redux” 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.

continue reading ...

December 5, 2014: 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.

continue reading ...

November 10th, 2014: CL congratulates Michael Färber for winning the “Prix de la France”.

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”.

continue reading ...

July 23, 2014: Vienna Summer of Logic

The Computational Logic group just returned from the Vienna Summer of Logic, which was held in Vienna from July 9 until July 24.

continue reading ...

July 8, 2014: Michael Schaper completed his master studies

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.

June 16, 2014: CL member René Thiemann is entering the START program

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.

continue reading ...

June 16, 2014: CL welcomes Michael Färber as new member

Michael works as a researcher on the project “Interactive Proof: Proof Translation, Premise Selection, Rewriting “.

March 13, 2014: 10th project headed by CL member accepted by the FWF

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.

continue reading ...

February 3, 2014: CL welcomes Thibault Gauthier as new member

Thibault works as a researcher on the project “Interactive Proof: Proof Translation, Premise Selection, Rewriting “.

November 26, 2013: Simon Legner completed his master studies

Today Simon Legner successfully defended his master thesis on “Non Linear Arithmetic”.

November 14, 2013: 2 PhD-student and 2 postdoc positions available

In the FWF projects “Automated Complexity Analysis via Transformations” of Georg Moser and “Interactive Proof: Proof Translation, Premise Selection, Rewriting” of Cezary Kaliszyk there are openings for both a PhD-student and a postdoctoral research assistant each.

continue reading ...

November 12, 2013: Martin Avanzini passed his final examination

Martin Avanzini MA, passed his rigorosum (cum laude) and will soon be officially honoured with his doctorate. Congratulations!

continue reading ...

September 30, 2013: FWF project “Interactive Proof: Proof Translation, Premise Selection, Rewriting” accepted

Cezary Kaliszyk’s project proposal “Interactive Proof: Proof Translation, Premise Selection, Rewriting” has been accepted by the Austrian Science Fund. The project is planned for 3 years and will commence shortly. The volume of the project is EUR 323K.

continue reading ...

August 16, 2013: Benjamin Höller completed his master studies

Today Benjamin Höller successfully defended his master thesis on “Confluence of Rewrite Systems with AC Rules”.

August 8, 2013: René Thiemann successfully completed his habilitation procedure

After the final presentation of his habilitation thesis on July 4, today René Thiemann was officially authorized to teach the subject “computer science”.

continue reading ...

May 14, 2013: FWF project “Automated Complexity Analysis via Transformations” accepted

Georg Moser’s project proposal on “Automated Complexity Analysis via Transformations” was accepted by the Austrian Science Fund (FWF) and has a duration of 3 years. The volume of the project is EUR 400K.

continue reading ...

March 28, 2013: Julian Nagele completed his master studies

Today Julian Nagele successfully defended his master thesis on higher-order termination.

continue reading ...

March 21, 2013: Sarah Winkler passed her final examination

Today MSc Sarah Winkler passed the rigorosum (cum laude) to obtain her doctorate degree.

continue reading ...

December 3, 2012: Thomas Sternagel completed his master studies

Thomas Sternagel successfully defended his master thesis on “Automatic Proofs in Equational Logic”.

continue reading ...

CL @ BeSt^3

CL will actively participate at this year’s BeSt3 by providing logic puzzles software and personal guidance by master students and senior researchers.

continue reading ...

Computation with Bounded Resources

CL proudly presents its research group on Computation with Bounded Resources. The group is concerned with fundamental questions on computations with limited resources.

continue reading ...

September 16, 2012: CL @ Brückenkurs

As part of the Brückenkurs, a new initiative to provide additional tutoring to freshmen, Harald Zankl gives a course on formal concepts.

continue reading ...

September 4, 2012: CL welcomes Benjamin Winder as new member

Benjamin is our new system administrator. He joined us on September 4, 2012.

continue reading ...

August 23, 2012: Friedrich Neurauter passed his final examination

DI Friedrich Neurauter passed his rigorosum (cum laude) and will soon be officially honoured with his doctorate.

continue reading ...

June 15, 2012: CL welcomes Cynthia Kop as new member

Cynthia Kop joined the CL group on June 15.

continue reading ...

April 28, 2012: Logic Puzzles @ Tiroler Forschungsnacht

The Computational Logic group showed how computers can solve logic puzzles such as Sudoku at the Tiroler Forschungsnacht.

continue reading ...

April 27, 2012: Andreas Schnabl passed his final examination

Today DI Andreas Schnabl passed his rigorosum (cum laude) and will soon be officially honoured with his doctorate.

continue reading ...

FWF-JSPS Joint Project Austria-Japan Accepted (March 20, 2012)

The project “Constrained Rewriting and SMT: Emerging Trends in Rewriting”, funded by Austrian Science Fund (FWF) and the Japan Society for Promotion of Science (JSPS) has been accepted. The project is a joint project between Austria and Japan. It is planned for 3 years and will commence shortly. The volume of the project is EUR 463K.

continue reading ...