The synthesis of loop predicates

DOI10.1145/360827.360850zbMath0273.68014OpenAlexW1978367838WikidataQ128523490 ScholiaQ128523490MaRDI QIDQ5180828

Ben Wegbreit

Publication date: 1974

Published in: Communications of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/360827.360850

Mathematics Subject Classification ID

General topics in the theory of software (68N01)

Related Items

A formalization of programs in first-order logic with a discrete linear order, Efficient symbolic analysis of programs, Recent advances in program verification through computer algebra, Mechanical inference of invariants for FOR-loops, A quantifier-elimination based heuristic for automatically generating inductive assertions for programs, A near-optimal method for reasoning about action, Aligator: A Mathematica Package for Invariant Generation (System Description), Synthesis of the programmed functions offor loops on data structures, Generating all polynomial invariants in simple loops, Elimination Techniques for Program Analysis, Reasoning Algebraically About P-Solvable Loops