{'fraction_non_alphanumeric': 0.017889087656529516, 'fraction_numerical': 0.0, 'mean_word_length': 5.416393442622951, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Automatic generation of specifications using verification tools = Automatische Spezifikationserzeugung mit Hilfe von Verifikationswerkzeugen

This dissertation deals with the automatic generation of sound specifications from a given program in the form of loop invariants and method contracts. Sound specifications are extremely useful, in that without them analysis of non-trivial programs becomes almost impossible. Verification tools can be used to prove complex properties for real-world programs, but this requires the presence of sound specifications for unbounded loops and unbounded recursive method calls. If even one simple specification is missing, the proof may become impossible to close. In general automation and precision are two goals which are often mutually exclusive. To ensure that the generation of specifications is fully automatic, precision will suffer. Approaches exist which perform abstraction on programs, replacing all types with abstracted counterparts with only finitely many different abstract values. Thus algorithms relying on fixed points for these abstract values can be used in the automatic generation of specifications, ensuring termination thereof. Precision is lost not only at the loops and method calls where this is required to ensure automation, however, but in the entire program. The automatic generation of specifications illustrated in this dissertation is characterized by the following: (i) abstraction is restricted to the loops and method calls themselves, ensuring that precision is kept for the remaining program, (ii) the loss of precision due to abstraction is partially reduced, by coupling the abstraction with introduction of new invariants which aim to counteract this loss of precision to a certain degree, and (iii) non-standard control flows of real-world programming languages are supported, rather than restricting the analysis to an academic toy language. In order to restrict the loss of precision to loops and method calls, abstraction is performed on program states, rather than the entire program. This allows full precision to be kept where possible, while program states related to loops and method calls are abstracted in order to ensure the termination of fixed point algorithms. The abstraction of program states is performed using abstract domains for the corresponding types. These abstract values can then be used outside of the loop or method call as normal values for which only partial knowledge is present. Real-world programming languages, such as Java, can contain, for example, a program heap which can be modified in loops or method calls, as well as objects and arrays as types in addition to the simpler primitive types such as booleans and integers. This leads to abstract domains being presented for objects and program heaps. As abstract domains are hard to fine-tune, additional invariants are introduced when abstracting, to counteract the coarse overapproximations. This allows abstraction of an array’s elements, for example, by a coarse overapproximation of the program heap on which the elements reside, in addition to the introduction of invariants regarding the values of said array elements. Real-world programming languages contain many elements that make the automatic generation of specifications much harder than these are on academic toy languages or strongly reduced subsets of real-world languages. Both loops and simple recursion are comparatively easy to reason about by themselves, however combining these, where a method calls itself recursively inside a loop, makes automatic generation of specifications a much harder task. Mutual recursion and non-standard control flows such as breaking out of a loop, throwing exceptions or returning from a method call while inside a loop add further complications. This dissertation describes how to automatically generate specifications in all of these cases.