cl-banner

News Archive DE


  • September 9, 2020: Congratulations: Fabian Mitterwallner completes his master studies

Today Fabian successfully defended his master thesis on “Extending Tools for Confluence and Related Properties of Rewrite systems”. We are happy that Fabian will be employed on a university position to pursue a PhD.

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

  • February 1, 2020: Georg Moser becomes full professor

Georg Moser, who joined CL in 2004, has been appointed as professor at the Department of Computer Science. He will head the “Theoretical Computer Science” group. We wish him all the best and look forward to fruitful collaboration.

  • January 9, 2020: Congratulations: Christina Kohl completes her master studies

Today Christina successfully defended her master thesis on “Proof Terms”. We are happy that Christina 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.
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.

  • 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. His thesis "Challenges in Automation of Rewriting" explains how several properties of rewrite systems can be investigated automatically.

  • 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 10, 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”. The award ceremony will take place on December 3, 18h at Claudiana, Innsbruck.

  • 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 »

Nach oben scrollen