The synthesis of loop predicates

DOI10.1145/360827.360850MaRDI QIDQ5180828zbMATH OpenOpenAlexWikidataFDO

Authors 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)

Cited in

(11)

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

This page was built for publication: The synthesis of loop predicates

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5180828)