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

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningpeer 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.
OriginalsprogEngelsk
TitelProceedings 8th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2021)
RedaktørerHossein Hojjat, Bishoksan Kafle
Antal sider14
Vol/bind344
ForlagEPTCS
Publikationsdato13 sep. 2021
Sider22-35
DOI
StatusUdgivet - 13 sep. 2021
Begivenhed8th Workshop on Horn Clauses for Verification and Synthesis - Luxembourg (Online), Luxembourg
Varighed: 28 mar. 202128 mar. 2021
Konferencens nummer: 8
https://www.sci.unich.it/hcvs21/

Workshop

Workshop8th Workshop on Horn Clauses for Verification and Synthesis
Nummer8
LokationLuxembourg (Online)
ByLuxembourg
Periode28/03/202128/03/2021
Internetadresse
NavnElectronic Proceedings in Theoretical Computer Science
Vol/bind344
ISSN2075-2180

Emneord

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

Citer dette