Reflexive transitive invariant relations: A basis for computing loop functions

DOI10.1016/J.JSC.2008.11.007zbMATH Open1208.68150OpenAlexW2006824750MaRDI QIDQ604384FDOQ604384

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

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

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

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)

Cites Work

• The Daikon system for dynamic detection of likely invariants
• Relational heuristics for the design of deterministic programs
• On the lattice of specifications: Applications to a specification methodology
• A lattice-theoretical fixpoint theorem and its applications
• Title not available (Why is that?)
• An axiomatic basis for computer programming
• Affine relationships among variables of a program
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The new math of computer programming
• Computer Aided Verification
• Strongest invariant functions: Their use in the systematic analysis of while statements
• Advanced symbolic analysis for compilers. New techniques and algorithms for symbolic program analysis and optimization.
• Properties of data flow frameworks: A unified model
• A Heuristic for Deriving Loop Functions
• Title not available (Why is that?)
• Theoretical Aspects of Computing - ICTAC 2004

Cited In (3)

• Strongest invariant functions: Their use in the systematic analysis of while statements
• Invariant relations for affine loops
• Convergence: integrating termination and abort-freedom

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)