Reflexive transitive invariant relations: A basis for computing loop functions

DOI10.1016/J.JSC.2008.11.007MaRDI QIDQ604384zbMATH OpenOpenAlexFDO

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

Publication date 10 November 2010

Published in Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jsc.2008.11.007

zbMATH Keywords

invariant relationsrefinement calculusinvariant functionsrelational calculusloop functionscomputing loop behaviorfunction extractioninvariant assertions

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of software (68N99)

Recommendations

• Invariant functions and invariant relations: an alternative to invariant assertions
• A versatile concept for the analysis of loops
• Relational methods in the analysis of while loops: observations of versatility
• Strongest invariant functions: Their use in the systematic analysis of while statements
• On the mechanical derivation of loop invariants

Cites work

• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• scientific article; zbMATH DE number 3768939 (Why is no real title available?)
• scientific article; zbMATH DE number 46740 (Why is no real title available?)
• scientific article; zbMATH DE number 3550181 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• A Heuristic for Deriving Loop Functions
• A lattice-theoretical fixpoint theorem and its applications
• Advanced symbolic analysis for compilers. New techniques and algorithms for symbolic program analysis and optimization.
• Affine relationships among variables of a program
• An axiomatic basis for computer programming
• Computer Aided Verification
• Computing properties of numerical imperative programs by symbolic computation
• On the lattice of specifications: Applications to a specification methodology
• Properties of data flow frameworks: A unified model
• Relational heuristics for the design of deterministic programs
• Strongest invariant functions: Their use in the systematic analysis of while statements
• The Daikon system for dynamic detection of likely invariants
• The new math of computer programming
• Theoretical Aspects of Computing - ICTAC 2004

Cited in

(6)

• Invariant relations for affine loops
• Strongest invariant functions: Their use in the systematic analysis of while statements
• Relational methods in the analysis of while loops: observations of versatility
• A versatile concept for the analysis of loops
• Invariant functions and invariant relations: an alternative to invariant assertions
• Convergence: integrating termination and abort-freedom

Describes a project that uses

Uses Software

• Daikon

This page was built for publication: Reflexive transitive invariant relations: A basis for computing loop functions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q604384)