The synthesis of loop predicates
From MaRDI portal
Publication:5180828
DOI10.1145/360827.360850zbMath0273.68014MaRDI QIDQ5180828
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
68N01: General topics in the theory of software
Related Items
Elimination Techniques for Program Analysis, Reasoning Algebraically About P-Solvable Loops, A formalization of programs in first-order logic with a discrete linear order, 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, Efficient symbolic analysis of programs, A near-optimal method for reasoning about action, Generating all polynomial invariants in simple loops, Aligator: A Mathematica Package for Invariant Generation (System Description), Synthesis of the programmed functions offor loops on data structures