Logical analysis of programs
From MaRDI portal
Publication:4124273
DOI10.1145/360032.360048zbMATH Open0353.68016OpenAlexW2075913776MaRDI QIDQ4124273FDOQ4124273
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
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
- Current methods for proving program correctness
- Verification conditions for source-level imperative programs
- 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)
