Definition Softwaretechnik

0 views

Skip to first unread message

Prince Aboubakar

unread,

Aug 3, 2024, 4:23:48 PM8/3/24

to lopparecharz

Please contact us if you are interested in one of these topics or if you want to propose your own topic that is related to our chair. Please include your transcript in the request so that we can meet and assess suitable topics that fit your qualification. You can also have a look at our collection of past student reports and theses to get an impression of what a thesis at our chair could look like.

Applicants should have experience with SQL, Databases and be proficient in one of Python, Java, Kotlin, Go or C++ as well as have some experience with web technologies. Experience with Docker/Podman and Web Development is a plus.

Software Verification Witnesses are a widely adopted tool to exchange information about tools centered on quality assurance, like fuzzers, model checkers, deductive verifiers, between many others. Currently only witnesses can only express a subset of what is required to present a complete violation or proof for all possible programs. Goal of this thesis would be to do an extension of the format and implement support for this extension in one of multiple directions. For example, for other program features like arrays and concurrency, for other programming languages like Java and Rust or for other specifications like memory safety.

Many incremental reverification techniques assume that the same technique is used for the original and the modified program. However, this might not be ensured if we use an algorithm selector for choosing the most suitable verification technique. Therefore, this thesis should study how robust algorithm selection, in particular algorithm selection based on Boolean Features [1], is with respect to program changes. To this end, the thesis must extract the Boolean features, both for original and modified program, study which Boolean Features change and remain identical between original and modified program. In a second step, the selection strategy from CPA-seq [1,2,3,4,5] for the reach-error property should be extracted and based on the extracted features it should be analyzed whether the selected technique stays the same between original and modified program. Ideally, the thesis also analyzes whether or or under which conditions the successful analysis stays the same. As set of pairs of original and modified programs, the thesis shall consider the Linux regression verification tasks [6] and the combination tasks [7].

Many incremental reverification techniques assume that the same technique is used for the original and the modified program. However, this might not be ensured if we use an algorithm selector for choosing the most suitable verification technique. Therefore, this thesis should study how robust algorithm selection, in particular PeSCo's algorithm selection [1,2], is with respect to program changes. To this end, the thesis must extract from the logfile the verification sequence applied by PeSCo for a given task (program) and analyze whether the extracted sequence stays the same for original and modified program. In addition, the thesis may need to execute PeSCo on the original and modified programs to get the required logfiles. Ideally, the thesis also analyzes whether or or under which conditions the successful analysis stays the same. As set of pairs of original and modified programs, the thesis shall consider the Linux regression verification tasks [3] and the combination tasks [4].

Many incremental reverification techniques assume that the same technique is used for the original and the modified program. However, this might not be ensured if we use an algorithm selector for choosing the most suitable verification technique. Therefore, this thesis should study how robust algorithm selection, in particular PeSCo-CPA's algorithm selection [1,2], is with respect to program changes. To this end, the thesis must extract from the logfile the verification sequence applied by PeSCo-CPA for a given task (program) and analyze whether the extracted sequence stays the same for original and modified program. In addition, the thesis may need to execute PeSCo-CPA on the original and modified programs to get the required logfiles. Ideally, the thesis also analyzes whether or or under which conditions the successful analysis stays the same. As set of pairs of original and modified programs, the thesis shall consider the Linux regression verification tasks [3] and the combination tasks [4].

When an automatic model checker finds a proof or a bug, it exports it as a witness. These outputs of the verification process can be independently validated by using a Validator. One of these validators is Metaval, which instruments the program using the information present in the witnesses. Goal of this Thesis is to reimplement Metaval for the new witness format 2.0.

When an automatic model checker finds a but, it reports it as constraints on the possible execution paths in form of a violation witness. These constraints are then used by a witness validator in order to replay the violation. The goal of this thesis is to make the restrictions on the state space available to all automatic verifiers by introducing them into the source code of the program.

Automatic software verification tries to automatically proof that a program fulfills a specification without human input. On the other hand deductive verification requires manually writing annotations to proof the program correct. Usually everything required to build a deductive verifier is inside an automatic verifier. The goal of this thesis is to create a deductive verifier out of the highly successful automatic verifier CPAchecker.

Automatic software verification tries to automatically proof that a program fulfills a specification without human input. On the other hand deductive verification requires manually writing annotations to proof the program correct. The goal of this thesis is to combine the strengths of both approaches by writing a tools which generates proof goals using information information provided by the user, but allow some of the information to be missing for it to be automatically verified by an automatic verifier.

k-induction is a verification technique for reachability analysis. Ranking function analysis can prove the termination of a loop and map states reachable inside the loop into numbers satisfying multiple conditions. Plain k-induction sometimes assumes unreachable states when trying to infer k-inductive invariant. These states are often pruned by using auxiliary invariants either provided by different reachability analyses or written by human. The goal of the thesis is to use termination analysis to compute ranking function and then use these ranking functions to boost k-induction.

C program satisfies termination specification if all the possible executions of the program eventually terminate. It is usually very challenging to automatically prove that a given program satisfies this property. T2R is an algorithm that transforms the program so that the transformed program can be verified using well-performing fine-tuned reachability algorithms. It is implemented in our modular framework for program transformations. Current transformation is inefficient for some reachability techniques like symbolic execution. The goal of this thesis is to implement another transformation that would make the symbolic tree easier to explore for symbolic execution.

Algorithms for analysis of C programs are usually designed to verify a concrete class of properties of the C programs. Many of the properties of C programs that are checked by verifiers have a similar form. Memory-Safety and Reach-Safety property are both safety properties of the program with different atomic propositions. By instrumenting C programs, we can convert the Memory-Safety property to the Reach-Safety property, which opens new options for Memory-Safety analysis using algorithms that are used for Reach-safety tasks. After having solved the transformed task, we want to transform the witness i.e. the information the verifier provided for the verdict of the program to a witness for the original program. The goal of the thesis is to implement such a transformation of witnesses.

The SV-Benchmarks repository is a collection of verification tasks and used for example in competitions of verifiers and other tools. Compilers like GCC and Clang likely have test suites with C programs that would be suitable as verification tasks, if adjusted to the expected format. This should be done systematically for at least these two compilers and potentially others, and the result should be submitted to SV-Benchmarks. If not enough potential tasks can be found, another source of tasks would be regression-test suites of verifiers and testing tools.

Algorithms for analysis of C programs are usually designed to verify a concrete class of properties of the C programs. Many of the properties of C programs that are checked by verifiers have a similar form. No-Datarace and Reach-Safety property are both safety properties of the program with different atomic propositions. By instrumenting C programs, we can convert the No-Datarace property to the Reach-Safety property, which opens new options for No-Datarace analysis using algorithms that are used for Reach-safety tasks. The goal of the thesis is to develop an idea of transformation C programs so that Reach-Safety analysis proves No-Datarace, implement the transformation in a tool and observe whether it is more efficient to solve No-Overflow using Reach-Safety analysis.

Algorithms for analysis of C programs are usually designed to verify a concrete class of properties of the C programs. Many of the properties of C programs that are checked by verifiers have a similar form. Memory-Safety and Reach-Safety property are both safety properties of the program with different atomic propositions. By instrumenting C programs, we can convert the Memory-Safety property to the Reach-Safety property, which opens new options for Memory-Safety analysis using algorithms that are used for Reach-safety tasks. The goal of the thesis is to develop an idea of transformation C programs so that Reach-Safety analysis proves Memory-Safety, implement the transformation in a tool and observe whether it is more efficient to solve Memory-Safety using Reach-Safety analysis.