Logical analysis of programs

DOI10.1145/360032.360048zbMath0353.68016OpenAlexW2075913776MaRDI QIDQ4124273

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)

Related Items

Efficient symbolic analysis of programs, A decomposition rule for the Hoare logic, A method for computing the number of iterations in data dependent loops, Automatic synthesis of logical models for order-sorted first-order theories, An integrated approach to high integrity software verification, 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, Automatic generation of invariants and intermediate assertions, Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic, Solving invariant generation for unsolvable loops, Verification conditions for source-level imperative programs, Synthesis of the programmed functions offor loops on data structures, Generating all polynomial invariants in simple loops, Current methods for proving program correctness, An algorithm for finding invariant relations in programs, Logical debugging