Software and Computational Systems Lab

We are currently looking for several student research assistants for our cloud solution for distributed execution of verification benchmarks. The BenchCloud is the fundamental component for running international scientific competitions (SV-COMP, Test-Comp), and large-scale experiments for publications at our chair. In this context, the BenchCloud 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 BenchCloud 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 us directly via Zulip or mail.

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

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.

We aim to scale software verification through a distributed algorithm that continuously refines formal summaries of program code. In this role, you are part of a small team that designs and develops algorithms, abstract domains, and microservices to scale code analysis across large codebases and hundreds of workers. Our focus is on adapting existing practices in software verification to a distributed setting and on the development of efficient algorithms for information exchange and code-block analysis.

This job is for you, if:

• you proud yourself with high-quality code
• you are enthusiastic about the safety of software and the static analysis of code
• you are interested in the formal methods of software analysis (for example automata, graphs, C semantics, program abstractions)
• you enjoy designing algorithms and debugging code in-depth to fully understand it, in a highly autonomous work setting

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

We aim to apply our achievements in software verification to various real-world applications. In this role, you are 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 of verification. You 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 enjoy designing algorithms and debugging code in-depth to fully understand it, in a highly autonomous work setting

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.