Software and Computational Systems Lab

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