Reflexive transitive invariant relations: A basis for computing loop functions

DOI10.1016/j.jsc.2008.11.007zbMath1208.68150OpenAlexW2006824750MaRDI QIDQ604384

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

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

refinement calculusrelational calculusinvariant functionsinvariant relationsloop functionscomputing loop behaviorfunction extractioninvariant assertions

Mathematics Subject Classification ID

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

Related Items (1)

Convergence: integrating termination and abort-freedom

Uses Software

• Daikon

Cites Work

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

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