Dennis Müller will join CL to work on the DAAD project “From Informal to Formal Mathematics” as a postdoc.
- Details
- Category: News Archive
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.
- Details
- Category: News Archive
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!
- Details
- Category: News Archive
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.
- Details
- Category: News Archive
Michael Färber successfully defended his PhD thesis on Learning Proof Search in Proof Assistants. Congratulations!
- Details
- Category: News Archive
Ralph starts as a postdoc on the project Certifying Termination and Complexity Proofs of Programs. His expertise is on parametric complexity.
- Details
- Category: News Archive
Max starts as a PhD-student on the project Certifying Termination and Complexity Proofs of Programs.
- Details
- Category: News Archive
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.
- Details
- Category: News Archive
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.
- Details
- Category: News Archive
David starts as a PhD-student on the project Complexity Analysis-based Guaranteed Execution and Shawn is employed on the project SMART.
- Details
- Category: News Archive
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.
- Details
- Category: News Archive