+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +**********************************************************************

Zeit: Montag, 28. Januar 2019, 16:30 Uhr Ort: Gebäude E3, Seminarraum 9222, Ahornstr. 55

Referent: Thomas Ströder, Dipl.-Inform. Lehr- und Forschungsgebiet Informatik 2

Thema: Symbolic Execution and Program Synthesis: A General Methodology for Software Verification

Abstract:

We are concerned with the correctness of software and present a general methodology for verifying properties of programs in virtually any programming language. This methodology consists of two stages: First, we symbolically execute the program in question to obtain a finite over-approximation of all possible program executions for all possible inputs. We call this over-approximation a symbolic execution graph. The difference of this graph compared to most existing approaches using abstract domains is that its construction is strongly guided by the analyzed program rather than using program-independent widening operators. Afterwards, we synthesize programs in simple programming languages from the symbolic execution graph capturing the essence of the program properties that we want to analyze. Thus, the subsequent analysis of these properties on the synthesized programs is substantially simplified. So we exploit synergies between program analysis and synthesis techniques to obtain powerful verification approaches.

Although the over-approximation induced by the symbolic execution graph and subsequent program synthesis might lose precision, our empirical evaluations demonstrate that the abstract domains introduced in this thesis are more precise than other existing domains while still allowing efficient analyses in practice (in particular due to the simplification obtained by program synthesis and the exploitation of powerful existing analysis techniques for the simple target languages). Hence, our methodology proved to be very successful in the leading international competitions in the fields of our analyses.

We apply our methodology to prove determinacy, termination, and upper runtime complexity bounds of Prolog programs, memory safety and termination of LLVM programs (compiled from C programs), deadlock and livelock freedom of concurrent imperative programs with shared memory, and to provide a solution to the Behavior Composition Problem, a program synthesis problem trying to reliably achieve a deterministic target behavior with a set of non-deterministic agents acting in a non-deterministic environment.

Our methodology is particularly useful for analyzing “universal” properties that hold for all program executions (e.g., termination, memory safety, or upper bounds on runtime complexity). Here, our empirical results show that our approach clearly outperforms any previous existing approach. While our methodology can to some extent also be applied to analyze “existential” properties that only need to hold for some program executions (e.g., proving the presence of defects like non-termination or violations of memory safety), additional effort is necessary to make our approach sound for such analyses due to the over-approximation inherently involved. In principle, we can detect candidates satisfying such existential properties in our symbolic execution graph but must prove their feasibility separately.

Many of our contributions have been implemented in the verification tool AProVE and empirically evaluated by extensive experiments. Our contributions advance the state of the art in automated program verification and offer a guideline for creating future verification techniques following our methodology.

Es laden ein: Die Dozenten der Informatik