Invariant Relations: A Bridge from Programs to Equations

TL;DR

This paper introduces a relations-based approach using invariant relations to derive the functions of complex C-like programs with nested loops, overcoming limitations of traditional unrolling methods.

Contribution

It presents a novel method that captures loop semantics through invariant relations, enabling the derivation of program functions with arbitrary nested loops.

Findings

Successfully derives functions for programs with nested loops

Overcomes limitations of loop unrolling techniques

Provides a formal framework for program semantics analysis

Abstract

Great advances in program analysis would be enabled if it were possible to derive the function of a program from inputs to outputs (or from initial states to final states, depending on how we model program semantics). Efforts to do so have always stalled against the difficulty to derive the function of loops; the expedient solution to capture the function of loops by unrolling them an arbitrary number of iterations is clearly inadequate. In this paper, we propose a relations-based method to derive the function of a C-like program, including programs that have loops nested to an arbitrary level. To capture the semantics of loops, we use the concept of invariant relation.