Logical analysis of programs

DOI10.1145/360032.360048MaRDI QIDQ4124273zbMATH OpenOpenAlexFDO

Authors Shmuel Katz, Zohar Manna

Publication date 1976

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

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

Mathematics Subject Classification ID

General topics in the theory of software (68N01)

Cited in

(19)

• Efficient symbolic analysis of programs
• A decomposition rule for the Hoare logic
• Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic
• Logical debugging
• Automatic generation of invariants and intermediate assertions
• Automatic synthesis of logical models for order-sorted first-order theories
• Generating all polynomial invariants in simple loops
• Recent advances in program verification through computer algebra
• Synthesis of the programmed functions offor loops on data structures
• Current methods for proving program correctness
• An algorithm for finding invariant relations in programs
• Verification conditions for source-level imperative programs
• Mechanical inference of invariants for FOR-loops
• Solving invariant generation for unsolvable loops
• (Un)solvable loop analysis
• Algebraic and algorithmic methods for computing polynomial loop invariants
• A method for computing the number of iterations in data dependent loops
• An integrated approach to high integrity software verification
• A quantifier-elimination based heuristic for automatically generating inductive assertions for programs

This page was built for publication: Logical analysis of programs

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