Bernhard Gleiss

Loop Analysis by Quantification over Iterations

2018 · EPiC series in computing

We present a framework to analyze and verify programs containing loops by using a first-order language of so-called extended expressions. This language can express both functional and temporal properties of loops. We prove soundness and …