Holonomic Sequences in Program Verification

When being dependent on complex software systemson a plane, in a hospital, or in a carone has to be able to trust that they perform their tasks faultlessly. In order to ensure this, automated program analysis and verification utilizes computers to generate formal proofs that confirm the correctness of the underlying algorithms by mathematical means. An integral part of program analysis is the characterization of the possible data that is stored in variables, manipulated, and processed during the program execution. This can be achieved with the help of equations and inequalities which describe the boundaries of the data values that are reachable during the computation. Can a variable in an algorithm have negative values? Is the sum of the values in two given variables ever the number zero? Answers to this kind of questions are necessary to prevent incidents caused by software bugs like the explosion of the unmanned Ariane 5 rocket in the year 1994. Coincidentally, discovering these answers is among the hardest problems in program analysis. Our goal is to develop algorithmic methods for automatically generating suitable equations and inequalities, based on techniques coming from computer algebra and static program analysis. The values of variables do not change randomly but form regular number sequences. In the vast majority of programs, these number sequences belong to the class of holonomic sequences, which, for example, also includes the famous Fibonacci sequence. In the mathematical theory of holonomic sequences, many tools for their study have been developed, but even in some deceptively simple looking cases, these turn out to be insufficient for a full analysis. Additionally, these methods have only found sporadic application in program verification. In this project, we investigate ways to combine methods from program analysis and the mathematics of holonomic sequences in order to advance theory and practice in both disciplines. On the one hand, we work on adapting the methods developed for the analysis of sequences for the systematic use in program verification. Thus, the classification of the possible range of data stored in variables can be performed more precisely and effectively. On the other hand, we investigate how open questions regarding holonomic sequences can be answered by employing new and existing techniques in program verification. This will lead to new insight in the mathematical theory that is at the basis of these sequences and moreover we will give researchers and users of computer-aided mathematics access to powerful techniques for handling number sequences and inequalities.

The main focus of the Project "Holonomic Sequences in Program Verification" was the automated, mathematical analysis of algorithms, like they are used in countless computer programs in all areas of daily life. Such an analysis makes it possible to prove the correct behaviour of the program, which is of utmost importance in security critical application domains. Despite numerous efforts ranging back to the beginning of the 20th century and the first formulation of the modern interpretation of the term "computer", automated program analysis has not lost its status as a fundamental problem which can only be solved efficiently in a very few special cases. With a new, innovative approach, the researchers in the project aimed to explore new ways to solve this problem. To this end, they employed numerous theories from the mathematical toolbox. By combining modern results from different mathematical areas like discrete mathematics, computer algebra, and algorithmic geometry, they were able to gain valuable insight which may prove essential in future endeavours to find new methods for automated program verification and help to elevate future research in that direction. In addition to the theoretical contributions, the project also helped creating a framework for obtaining precise experimental data. This framework comes in the form of a collection of computer programs-referred to as a "library" in computer science-which allow a detailed analysis of systems of differential and difference equations. Such systems of equations form the central objects of interest in the mathematical representation of complex phenomena, including the variations in stored data during the execution of a computer program. The library and its source code are freely available for anyone interested. Despite the severe impact that the Covid-pandemic had during the last twelve months on the academic working environment in general and the project in particular, the researchers have succeeded in supporting the scientific community with important contributions, and in further strengthening the status of fundamental research In Austria.