Regular Path Clauses and Their Application in Solving Loops

Bishoksan Kafle, John Patrick Gallagher, Manuel V. Hermenegildo, Maximiliano Klemen, Pedro López-García, José F. Morales

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

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.
Original languageEnglish
Title of host publicationProceedings 8th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2021)
EditorsHossein Hojjat, Bishoksan Kafle
Number of pages14
Volume344
PublisherEPTCS
Publication date13 Sep 2021
Pages22-35
DOIs
Publication statusPublished - 13 Sep 2021
Event8th Workshop on Horn Clauses for Verification and Synthesis - Luxembourg (Online), Luxembourg
Duration: 28 Mar 202128 Mar 2021
Conference number: 8
https://www.sci.unich.it/hcvs21/

Workshop

Workshop8th Workshop on Horn Clauses for Verification and Synthesis
Number8
LocationLuxembourg (Online)
CityLuxembourg
Period28/03/202128/03/2021
Internet address
SeriesElectronic Proceedings in Theoretical Computer Science
Volume344
ISSN2075-2180

Keywords

  • Horn clauses
  • Multi-argument recurrences
  • Multi-path recurrences
  • Path programs

Cite this