News Archive

29 August, 2023: Johannes Niederhauser completes his master studies

Johannes Niederhauser successfully defends his master thesis, entitled “Left-linear Completion with AC Axioms”. Congratulations. We are delighted that Johannes will pursue a PhD degree.

6 July 2023: Stanislaw Purgal defends his PhD thesis

Stanislaw Purgal successfully defended his PhD thesis on “Abstract Reasoning with Deep Learning.” Congratulations!

23 June 2023: Max Haslbeck defends his PhD thesis

Max Haslbeck successfully defended his PhD thesis on “Certitying Termination Proofs of LLVM IR Programs.” Congratulations!

10 November 2022: CL congratulates Thomas Oberroither

Thomas Oberroither is the winner of the Best Bachelor Thesis award of the academic year 2021/2022. He was awarded at the inday students for his thesis “SWAp: A Student Wishlist Application”, supervised here at CL. Congratulations!

1 September 2022: CL welcomes Dohan Kim

Dohan Kim joins the ARI project as post-doc.

9 July 2022: Congratulations to Christina Kohl

Christina Kohl participated in the Gletscher Trailrun and finished 3rd in the top category: 62 kilometers with 3600 altitude meters. A tremendous achievement!

1 July 2022: CL welcomes Jonas Schöpf

Jonas Schöpf joins the ARI project as PhD student.

1 July 2022: start of new FWF-JSPS joint project

CL is proud to announce that Aart Middeldorp acquired an FWF International Project with JSPS (Japan Society for the Promotion of Science).

25 May 2022: 3 year postdoc position available

A 3 year postdoc position is available. Click here for details.

1 September 2021: CL welcomes Manuel Eberl as new member

Manuel joins the CL-team as post-doctoral researcher. He is a well known Isabelle user and one of the editors of the archive of formal proofs.

17 June 2021: Yutaka Nagashima defends his PhD thesis

Yutaka Nagashima successfully defended his PhD thesis “Artificial Intelligence and Domain-Specific Languages for Interactive Theorem Proving”. He joined Yale-NUS as a Research Associate.

May 4, 2020: René Thiemann is joint invited speaker of FSCD-IJCAR conference 2020

The international conference on formal structures for computation and deduction (FSCD) and the international joint conference on automated reasoning (IJCAR) are two major conferences in the areas of rewriting, verification, automated deduction, and automated reasoning. In 2020 these conferences are collocating as part of the Paris Nord Summer of LoVe 2020, a joint event on logic and verification. There will be two joint invited speakers: John Harrison of Amazon Web Services and René Thiemann from our research group. CL congratulates.

April 28, 2020: Congratulations: Jonas Schöpf completes his master studies

Today Jonas successfully defended his master thesis on “The Weighted Path Order in TTT2”. We are happy that Jonas will be employed on a university position to pursue a PhD.

December 1, 2019: CL welcomes Dennis Müller

Dennis Müller will join CL to work on the DAAD project “From Informal to Formal Mathematics” as a postdoc.

January 30, 2019: CL welcomes Ping Hou, Josh Chen, and Stanisław Purgał as new members

The three new members will work on the project “Strong Modular Proof Assistance: Reasoning Across Theories”. They will work on CoqHammer and learning for automated reasoning.

December 18, 2018: Thibault Gauthier defends his PhD thesis

Thibault Gauthier successfully defended his thesis on Learning-Assisted Reasoning within Proof Assistants. He joined the Automated Reasoning Group at the Czech Technical University in Prague as a postdoctoral research assistant.

December 1, 2018: Cezary Kaliszyk becomes associate professor

The CL group congratulates Cezary Kaliszyk. His research, his teaching qualities and his organisational skills have all been successfully evaluated and therefore he is now an associate professor.

November 28, 2018: Michael Färber defends his PhD thesis

Michael Färber successfully defended his PhD thesis on Learning Proof Search in Proof Assistants. Congratulations!

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.

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.

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.

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

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.

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.

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

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

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.

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.

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.

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

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.

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.

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.

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