Research Assistant and Tutor Positions
The Software and Computational Systems Lab is constantly looking for research assistants. If you have good grades and are interested in research in the area of software verification, please consider the below positions. We offer flexible working hours, a shared workspace in our offices, and the chance to contribute to novel research in multiple areas of software verification.
Doctoral Researcher
Positions for doctoral researchers require a Master degree in computer science or related fields.
🔬 Continuous Verification of CYber-Physical Systems (ConVeY)
ConVeY is a joint DFG research training group between TU Munich and LMU Munich. We offer a strong academic environment and a comprehensive qualification program to our PhD students. Currently, we are looking for new PhD candidates. Please submit your application via this portal by April 21, 2024. For more information, please visit the project website.
Student Research Assistant
Our job positions target students with a place of residence (Wohnort) in Germany. If this does not apply please still contact us - we will organize a student exchange or internship.
🔬 BenchCloud: A Cloud Platform for Benchmarking
Required Skills:
- Java programming
- Basic Linux knowledge
Useful knowledge/areas of interest:
- Software Verification
- Web technologies
- Parallel programming
The employment is as a student assistant (HiWi), whereby the number of hours per week can be flexibly adjusted (but should not be less than 5 hours per week). The working hours can be arranged flexibly. A long-term cooperation over several semesters is generally desired from our side. If you are interested or if any questions are left, please contact us directly via Zulip or mail.
Languages: German and English
🔬 CPAchecker: The Configurable Software-Verification Platform
Required Skills:
- Java programming
- Basic Linux knowledge
- First experiences with formal methods in software verification
Useful knowledge/areas of interest:
- Software Verification
- Interest in research and experimenting
The employment is as a student assistant (HiWi), whereby the number of hours per week can be flexibly adjusted (but should not be less than 5 hours per week). The working hours can be arranged flexibly. A long-term cooperation over several semesters is generally desired from our side. If you are interested or if any questions are left, please contact me directly via Zulip or mail.
Languages: German and English
🔬 Development of Tools and Microservices for Code Analysis
We aim to apply our achievements in software-verification research to various real-world applications. In this role, you will be part of a small team that designs and develops tools to make code analysis more accessible and better scalable for everday software development. A focus is on increasing the usability and the speed. You will have the opportunity to work on projects like IDE plugins, micro-service infrastructures, and integrations in CI pipelines.
This job is for you, if:
- you proud yourself with high-quality code
- you are enthusiastic about developer tooling
- you are interested in the field of compilers and software analysis (parsers, code transformations, static analysis)
- you can manage yourself well
Required Skills:
- Programming experience in Java, Kotlin, or C++
- Basic knowledge in code analysis and/or software verification (example: lectures on formal specification and verification).
Employment: The employment is as a student assistant (HiWi) with 7 to 12 hours per week. The day and time of work can be arranged flexibly in certain bounds. A long-term cooperation over several semesters is generally desired from our side.
Languages: German and English
Please contact us via Zulip or mail. We're always available for questions.
🔬 Bridging Hardware and Software Analysis
Background: Computational systems consisting of both hardware and software components are used everywhere in modern society. The correctness assurance of theses systems is thus an indispensable research area. In this project, we aim at utilizing the joint knowledge of both hardware and software verification communities by
- optimizing the applicability of software analyzers to hardware designs,
- constructing a framework that facilitates the utilization of off-the-shelf hardware analyzers for software, and
- combining strengths of hardware and software verification algorithms to solve practical problems.
Job description: We are looking for students that can assist us in the following tasks.
- Develop and optimize the translation flow of Btor2C
- Extend word-level hardware model-checking benchmark set
- Incorporate more hardware verifiers into our benchmarking framework
- Implement a Btor2 parser in Python
- ... and more!
Requirements:
- Programming experience in C/C++ and Python
- Basic Linux skills
- Knowledge in formal verification and testing
Employment: The employment is as a student assistant (HiWi) with 7 to 12 hours per week. The day and time of work can be arranged flexibly in certain bounds. A long-term cooperation over several semesters is generally desired from our side.
Languages: English
Supervisors: Po-Chun Chien and Nian-Ze Lee
🔬 Formalization of cyber-physical systems logics in Isabelle/HOL
When computers control real-world systems (e.g. brake assistant systems in modern cars) their correctness has impact on human health and life. Said casually the failure of heavy machines could cause harm beyond the mere malfunction of, e.g., a printer or smartphone. To achieve high reliability, logical methods for cyber-physical systems strive for a formal proof of their correct behavior. However, the logical methods do only ensure correctness if they are in turn proven correct themselves.
We are searching for a student research assistant to work on the formalization of existing correctness proofs of logical methods for the analysis of cyber-physical systems in the proof assistant Isabelle/HOL. You will have the opportunity to participate in active research in the area of formal methods and logics in computer science.
This job is for you, if:
- mathematical problems don't scare you but arouse your curiosity
- you are enthusiastic about digging into challenging problems
- you are interested in logics and theorem-proving
- you can manage yourself well
Required Skills:
- Experience (e.g. from a lecture) in interactive theorem proving (e.g. with Isabelle/HOL, Coq, or Lean)
- Knowledgeable in logics (e.g. Hoare-logic)
- Ability to understand and play with mathematical proofs
Employment: The employment is as a student assistant (HiWi) with 7 to 12 hours per week. The day and time of work can be arranged flexibly in certain bounds. A long-term cooperation over several semesters is generally desired from our side.
Languages: German and English
Please contact us via Zulip or mail. We're always available for questions.
🔬 Exploring Synergies between Machine Learning and Formal Methods
Background: Machine learning (ML) has become a popular tool for solving complex problems in various domains. In particular there are some synergies between ML and formal methods. Not only can ML methods be used to improve the performance of formal methods, but formal methods can also be used to improve the reliability and explainability of ML models. We are searching for a student who would be interested in exploring synergies between ML and formal methods in at least one of the following directions:
- Using ML to improve the performance of formal methods
- Using formal methods to improve the reliability of ML models
Job description: We are looking for students that can assist us in one or more of the following tasks:
- Use generative AI to provide information to formal method tools, like Code2Inv
- Finding invariants from program executions using ML
- Use generative AI and formal methods to automatically generate function contracts in ACSL
- Use formal methods to verify the reliability of ML models
- Discover rules underlying how an ML model makes decisions using formal methods
- ... and much more!
Requirements:
- Programming experience in Python
- Basic Linux skills
- Knowledge in formal verification and testing
- Knowledge in machine learning
Employment: The employment is as a student assistant (HiWi) with 7 to 20 hours per week. The day and time of work can be arranged flexibly in certain bounds. A long-term cooperation over several semesters is generally desired from our side.
Languages: German and English
Supervisor: Marian Lingsch-Rosenfeld
🔬 Exploring Interactions between Model Checkers, Deductive Verifiers and Interactive Theorem Provers
Background: Formal Methods are a set of techniques to verify the correctness of software and hardware systems. Some popular methods are model checking, deductive verification, and interactive theorem proving. Each of these methods has its own strengths and weaknesses. The goal is to explore how these methods can be combined to leverage their strengths and mitigate their weaknesses.
Job description: We are looking for students that can assist us in one or more of the following tasks:
- Translate the results of a model checker into a proof for a deductive verifier
- Improve the information output of a model checker to be more useful for a deductive verifier
- Translate the results of a model checker into a proof for an interactive theorem prover
- Use the proof of an interactive theorem prover to obtain hints for a model checker
- ... and much more!
Requirements:
- Programming experience in Python or Java
- Basic Linux skills
- Basic knowledge in format methods
Employment: The employment is as a student assistant (HiWi) with 7 to 20 hours per week. The day and time of work can be arranged flexibly in certain bounds. A long-term cooperation over several semesters is generally desired from our side.
Languages:German and English
Supervisor: Marian Lingsch-Rosenfeld
Tutorship
Wir suchen für das Wintersemester 2024/2025 Tutorinnen und Tutoren für die unten gelisteten Veranstaltungen. Bei Interesse melde dich unverbindlich bei Thomas Lemberger via Mail or Zulip. Wir freuen uns auf deine Bewerbung!
📝 Einführung in die Informatik (mit Python)
Anmerkung: Die Veranstaltung "Einführung in die Informatik" wird ab dem WS 2022/23 von Java zu Python als primäre Programmiersprache wechseln.
Wir können Dir einen der folgenden Verträge anbieten:
- Bei einer Gruppe: 9h / Woche
- Bei zwei Gruppen: 13h / Woche (Bei zwei Gruppen sind es in Summe etwas weniger Stunden, da das Tutorentreffen ja nur einmal anfällt.)
Vertragsbeginn: 01.10.2024 oder 17.10.2024, jeweils bis 14.04.2025
Sprache: Deutsch
📝 Softwaretechnik
Die Vertragsdauer beträgt 5 Monate (17.10.2024-15.03.2025) mit folgenden möglichen Arbeitszeiten:
- 9h / Woche für Aufgabenkorrektur, ohne dass du eine Übung hältst.
- 13h / Woche für Aufgabenkorrektur und eine wöchentliche, zweistündige Übung für Studentinnen und Studenten.
- 19h / Woche für Aufgabenkorrektur und zwei wöchentliche, zweistündge Übungen für Studentinnen und Studenten.
Sprache: Deutsch
📝 Compiler Construction
The contract duration is 7 months (August to March 15, 2025) with 13 hours per week for assignment grading (including exams), the preparation of the weekly two-hour exercise session for students, the preparation of the practical part of the course, and the preparation of teaching materials until October.
Language: English