Reflexive transitive invariant relations: A basis for computing loop functions
From MaRDI portal
Publication:604384
DOI10.1016/j.jsc.2008.11.007zbMath1208.68150MaRDI QIDQ604384
Olfa Mraihi, Asma Louhichi, Lamia Labed Jilani, Shir Aharon, Chaitanya Nadkarni, 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
refinement calculus; relational calculus; invariant functions; invariant relations; loop functions; computing loop behavior; function extraction; invariant assertions
68Q60: Specification and verification (program logics, model checking, etc.)
68N99: Theory of software
Uses Software
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