Reflexive transitive invariant relations: A basis for computing loop functions

Ali Mili, Shir Aharon, Chaitanya Nadkarni, Lamia Labed Jilani, Asma Louhichi, Olfa Mraihi

Research output: Contribution to journalArticlepeer-review

3 Scopus citations


Invariant assertions play an important role in the analysis and verification of iterative programs. In this paper, we introduce a related but distinct concept, namely that of invariant relation. While invariant assertions are useful to prove the correctness of a loop with respect to a specification (represented by a precondition/ postcondition pair) in Hoare's logic, invariant relations are useful to derive the function of the loop in Mills' logic.

Original languageEnglish (US)
Pages (from-to)1114-1143
Number of pages30
JournalJournal of Symbolic Computation
Issue number11
StatePublished - Nov 2010

All Science Journal Classification (ASJC) codes

  • Algebra and Number Theory
  • Computational Mathematics


  • Computing loop behavior
  • Function extraction
  • Invariant assertions
  • Invariant functions
  • Invariant relations
  • Loop functions
  • Refinement calculus
  • Relational calculus


Dive into the research topics of 'Reflexive transitive invariant relations: A basis for computing loop functions'. Together they form a unique fingerprint.

Cite this