abstract.txt

Analyzing program loops is an important part of multiple software engineering tasks, such as bug detection,
test case generation, and optimization. Loop analysis is, however, one of the most challenging aspects of program 
analysis, especially with complex loops that feature multiple paths and nested loops. 
A widely used loop analysis technique is computing overapproximative loop summaries that represent 
the relationship between inputs and outputs as a set of constraints. 
But overapproximation is prone to imprecision. Kincaid and Silverman proposed a novel overapproximation approach, 
based on rational vector addition systems with resets (QVASR), 
that guarantees a certain degree of precision. 
In this master's thesis we adapted the \qvasr based loop summarization scheme to the trace abstraction 
method for proving program safety by implementing a summarization library that is used in two techniques: 
Firstly, directly on traces in the accelerated interpolation framework, which uses loop summaries for creating 
program state assertions that contain every trace through a loop. 
Secondly, as a preprocessor that transforms a given program's control-flow graph by replacing loops with the 
loop summarization such that trace abstraction considers traces that already contain every trace through a loop.