News

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.

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.