Invariant relations for affine loops

Wided Ghardallou; Hessamaldin Mohammadi; Richard C. Linger; Mark Pleszkoch; Ji Meng Loh; Ali Mili

doi:10.1007/s00236-024-00457-9

Invariant relations for affine loops

Wided Ghardallou, Hessamaldin Mohammadi, Richard C. Linger, Mark Pleszkoch, Ji Meng Loh, Ali Mili

Research output: Contribution to journal › Article › peer-review

Abstract

Invariant relations are used to analyze while loops; while their primary application is to derive the function of a loop, they can also be used to derive loop invariants, weakest preconditions, strongest postconditions, sufficient conditions of correctness, necessary conditions of correctness, and termination conditions of loops. In this paper we present two generic invariant relations that capture the semantics of loops whose loop body applies affine transformations on numeric variables.

Original language	English (US)
Pages (from-to)	261-314
Number of pages	54
Journal	Acta Informatica
Volume	61
Issue number	3
DOIs	https://doi.org/10.1007/s00236-024-00457-9
State	Published - Sep 2024

All Science Journal Classification (ASJC) codes

Software
Information Systems
Computer Networks and Communications

Access to Document

10.1007/s00236-024-00457-9

Cite this

@article{0358ff598d1d435d822f1e623d2414e4,

title = "Invariant relations for affine loops",

abstract = "Invariant relations are used to analyze while loops; while their primary application is to derive the function of a loop, they can also be used to derive loop invariants, weakest preconditions, strongest postconditions, sufficient conditions of correctness, necessary conditions of correctness, and termination conditions of loops. In this paper we present two generic invariant relations that capture the semantics of loops whose loop body applies affine transformations on numeric variables.",

author = "Wided Ghardallou and Hessamaldin Mohammadi and Linger, {Richard C.} and Mark Pleszkoch and Loh, {Ji Meng} and Ali Mili",

note = "Publisher Copyright: {\textcopyright} The Author(s) 2024.",

year = "2024",

month = sep,

doi = "10.1007/s00236-024-00457-9",

language = "English (US)",

volume = "61",

pages = "261--314",

journal = "Acta Informatica",

issn = "0001-5903",

publisher = "Springer New York",

number = "3",

}

TY - JOUR

T1 - Invariant relations for affine loops

AU - Ghardallou, Wided

AU - Mohammadi, Hessamaldin

AU - Linger, Richard C.

AU - Pleszkoch, Mark

AU - Loh, Ji Meng

AU - Mili, Ali

N1 - Publisher Copyright: © The Author(s) 2024.

PY - 2024/9

Y1 - 2024/9

N2 - Invariant relations are used to analyze while loops; while their primary application is to derive the function of a loop, they can also be used to derive loop invariants, weakest preconditions, strongest postconditions, sufficient conditions of correctness, necessary conditions of correctness, and termination conditions of loops. In this paper we present two generic invariant relations that capture the semantics of loops whose loop body applies affine transformations on numeric variables.

AB - Invariant relations are used to analyze while loops; while their primary application is to derive the function of a loop, they can also be used to derive loop invariants, weakest preconditions, strongest postconditions, sufficient conditions of correctness, necessary conditions of correctness, and termination conditions of loops. In this paper we present two generic invariant relations that capture the semantics of loops whose loop body applies affine transformations on numeric variables.

UR - http://www.scopus.com/inward/record.url?scp=85192832309&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85192832309&partnerID=8YFLogxK

U2 - 10.1007/s00236-024-00457-9

DO - 10.1007/s00236-024-00457-9

M3 - Article

AN - SCOPUS:85192832309

SN - 0001-5903

VL - 61

SP - 261

EP - 314

JO - Acta Informatica

JF - Acta Informatica

IS - 3

ER -

Invariant relations for affine loops

Abstract

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this