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

(17)

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

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)