Regular Path Clauses and Their Application in Solving Loops

Bishoksan Kafle
(IMDEA Software Institute, Spain)
John P. Gallagher
(Roskilde University, Denmark and IMDEA Software Institute, Spain)
Manuel V. Hermenegildo
(IMDEA Software Institute, Spain and U. Politecnica de Madrid, Spain)
Maximiliano Klemen
(IMDEA Software Institute, Spain and U. Politecnica de Madrid, Spain)
Pedro López-García
(IMDEA Software Institute, Spain and Spanish Council for Sci. Research (CSIC))
José F. Morales
(IMDEA Software Institute, Spain and U. Politecnica de Madrid, Spain)

A well-established approach to reasoning about loops during program analysis is to capture the effect of a loop by extracting recurrences from the loop; these express relationships between the values of variables, or program properties such as cost, on successive loop iterations. Recurrence solvers are capable of computing closed forms for some recurrences, thus deriving precise relationships capturing the complete loop execution. However, many recurrences extracted from loops cannot be solved, due to their having multiple recursive cases or multiple arguments. In the literature, several techniques for approximating the solution of unsolvable recurrences have been proposed. The approach presented in this paper is to define transformations based on regular path expressions and loop counters that (i) transform multi-path loops to single-path loops, giving rise to recurrences with a single recursive case, and (ii) transform multi-argument recurrences to single-argument recurrences, thus enabling the use of recurrence solvers on the transformed recurrences. Using this approach, precise solutions can sometimes be obtained that are not obtained by approximation methods.

In Hossein Hojjat and Bishoksan Kafle : Proceedings 8th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2021), Virtual, 28th March 2021, Electronic Proceedings in Theoretical Computer Science 344, pp. 22–35.
Published: 13th September 2021.

ArXived at: https://dx.doi.org/10.4204/EPTCS.344.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org