Open Positions at Software and Computational Systems Lab

Student Positions @ SoSy

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. The positions for doctoral researchers require a Mater degree in computer science or related fields. The other job positions target students at German universities and with a residence in Germany. If this does not apply please still contact us - you may qualify for a student exchange or internship.

Doctoral Researcher

🔬 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

🔬 JavaScript/React development for BenchExec

The chair maintains and developers the open-source benchmarking framework BenchExec that is used by many researchers. An important part of BenchExec are the interactive result tables (example) that users use to look at and interactively analyze their benchmarking results. We are currently looking for a student assistant who would be the primary developer of this web application and supported by the BenchExec maintainer Philipp Wendler.

This application is based on the React framework from Facebook and some libraries for features like tables and plots. A list of potential tasks can be found in our issue tracker. We also welcome own ideas and suggestions on how to improve it.

Required Skills:

JavaScript programming

Useful knowledge/areas of interest:

React
Web technologies
UI

The employment is as a student assistant (HiWi) with up to 12 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

Contact: Philipp Wendler

🔬 VerifierCloud: Cloud Service for Benchmarks

We are currently looking for several student research assistants for our cloud solution for distributed execution of verification benchmarks. The VerifierCloud is the fundamental component for running international scientific competitions (SV-COMP, Test-Comp) and meaningful experiments for publications at our chair. In this context, the VerifierCloud dynamically manages the reliable distribution of benchmarks to our chair-owned cluster. In addition, computing resources are also made available via a web frontend for experiments in the context of student work at our chair. If you have found fun in Java programming in the SEP and would like to expand your knowledge by working on a real project, this is the right place for you. The VerifierCloud has been actively developed for several years and is in productive use on a daily basis (e.g., over 50,000 benchmarks on quiet days alone).

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 me directly via Zulip or mail.

Languages: German and English

Contact: Marek Jankola and Daniel Baier

🔬 CPAchecker: The Configurable Software-Verification Platform

We are currently looking for student research assistants at the chair. We are mainly concerned with software safety. The internationally awarded framework CPAchecker supports a variety of analyses and approaches for the verification of C programs. CPAchecker offers several thousand different configuration options and allows to easily integrate new ideas. Basically, it verifies a given C program with respect to a specification, such as "the reach_error function is never called", and tells the user if there are paths through the program that violate that specification. CPAchecker annually participates very successfully in SV-COMP, the largest international competition for software verifiers. If you have found fun in Java programming and want to expand your knowledge in the world of formal verification by working on a real project, this is the right place for you. CPAchecker has been under active development for several years and is used, among other things, to verify parts of the Linux kernel.

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

Languages: German and English

Contact: Thomas Lemberger

🔬 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

Contact: Thomas Lemberger
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

Languages: English

Contact: 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

Languages: German and English

Contact: Marvin Brieger
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

Contact: 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

Languages:German and English

Contact: Marian Lingsch-Rosenfeld

Tutorship

Wir suchen für das Sommersemester 2024 TutorInnen für die unten gelisteten Veranstaltungen. Bitte melde dich gerne unverbindlich bei mir, falls du Interesse hast. Wir freuen uns auf deine Bewerbung!

📝 Softwareentwicklungspraktikum Java (SEP-Java)

Tätigkeit:

Für unser Softwareentwicklungspraktikum Java (SEP-Java) suchen wir noch Tutor:innen. Du kannst gut Java programmieren, möchtest dein Wissen weitergeben und dich selbst weiterentwickeln? Dann hast du hier die Möglichkeit, mitzugestalten. Im Rahmen deiner Arbeit übernimmst du die eigenständige Betreuung von mindestens 2 Gruppen mit je ca. 5 Studierenden. Du unterstützt sie durch technische und organisatorische Beratung. Die Tutorentätigkeit wird bezahlt und kann für das Modul "Fachübergreifende Kompetenzen" im Studium angerechnet werden.

Ablauf des Praktikums:

Das Praktikum ist in 2 Phasen eingeteilt: Bis Juni läuft die 1. Phase, in der die Studierenden Einzelaufgaben lösen müssen. Ab Juni startet die 2. Phase, in der die Studierenden in Gruppen von etwa 5 Personen ein größeres Projekt in Java implementieren (meist ein Online-Spiel). Das Projekt läuft bis 19. Juli.

Deine Aufgaben:

Während der ersten Phase korrigierst du die Abgaben der Studierenden und gibst ihnen damit wertvolles Feedback, das ihnen hilft ihr Programmieren zu verbessern. Während der zweiten Phase coachst du Studierenden-Teams, um ihnen zu einem erfolgreichen Projektabschluss zu verhelfen. Dazu triffst du dich einmal in der Woche mit deinen Teams, beurteilst den aktuellen Projektstand und unterstützt bei Fragen.

Dein Profil:

Sehr gute Noten im SEP-Java oder Praxiserfahrung in der objektorientierten Programmierung
Spaß und Interesse, Verantwortung für Projektgruppen zu übernehmen

Vertrag:

Vertragslaufzeit ist vom 15.04.2024 bis 31.07.2024. Unterschiedliche Arbeitszeiten sind möglich, beispielsweise 9h/Woche zur Betreuung von 2 Gruppen oder 12h/Woche zur Betreuung von 3 Gruppen. Bei Interesse melde dich unverbindlich mit deinem Transcript of Records und einem kurzen Satz zu deiner bisherigen Programmiererfahrung.

Sprache: Deutsch

Contact: Thomas Lemberger