Reflexive transitive invariant relations: A basis for computing loop functions

DOI10.1016/j.jsc.2008.11.007zbMath1208.68150MaRDI 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 calculus; relational calculus; invariant functions; invariant relations; loop functions; computing loop behavior; function extraction; invariant assertions

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

68N99: Theory of software

Related Items

Convergence: integrating termination and abort-freedom

Uses Software

• Daikon

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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