Programs and program verifications in a general setting

DOI10.1016/0304-3975(81)90076-1zbMath0481.68016OpenAlexW2006220572MaRDI QIDQ1162355

László Csirmaz

Publication date: 1981

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(81)90076-1

zbMATH Keywords

completeness of the Floyd-Hoare derivabilityhalting configurationsPeano models

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Non-standard algorithmic and dynamic logic, On the programs-as-formulas interpretation of parallel programs in Peano arithmetic, Recursive programs and denotational semantics in absolute logics of programs, Weak second order characterizations of various program verification systems, A complete logic for reasoning about programs via nonstandard model theory. I, A complete logic for reasoning about programs via nonstandard model theory. II, Total correctness in nonstandard logics of programs, On the Completeness of Dynamic Logic, Inductive Completeness of Logics of Programs, Hoare's logic for nondeterministic regular programs: A nonstandard approach, Is ``Some-other-time sometimes better than ``Sometime for proving partial correctness of programs?, A faithful embedding of parallel computations in star-finite models, Program correctness on finite fields, A simple proof for the completeness of Floyd's method, On the strength of temporal proofs

Cites Work

• Model theory
• Soundness and Completeness of an Axiom System for Program Verification
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item