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