Mathematics for reasoning about loop functions

DOI10.1016/j.scico.2009.09.009zbMath1192.68160OpenAlexW2049413589MaRDI QIDQ1044182

Chaitanya Nadkarni, Shir Aharon, Ali Milli

Publication date: 11 December 2009

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.scico.2009.09.009

zbMATH Keywords

functional extractionloop functionMills' theoremsub-goal induction theorem

Mathematics Subject Classification ID

Theory of software (68N99)

Related Items (3)

Convergence: integrating termination and abort-freedom ⋮ A versatile concept for the analysis of loops ⋮ Computing Preconditions and Postconditions of While Loops

Uses Software

• Daikon

Cites Work

• 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
• On the lattice of specifications: Applications to a specification methodology
• Affine relationships among variables of a program
• Reasoning algebraically about loops
• 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
• Transition Invariants and Transition Predicate Abstraction for Program Termination
• A Heuristic for Deriving Loop Functions
• Non-linear loop invariant generation using Gröbner bases
• Grammar Analysis and Parsing by Abstract Interpretation
• The new math of computer programming
• Subgoal induction
• An axiomatic basis for computer programming
• Theoretical Aspects of Computing - ICTAC 2004
• On the calculus of relations
• Computer Aided Verification

This page was built for publication: Mathematics for reasoning about loop functions