A PROPERTY OF 2‐SORTED PEANO MODELS AND PROGRAM VERIFICATION

DOI10.1002/MALQ.19840301907MaRDI QIDQ3677763zbMATH OpenOpenAlexFDO

Authors László Csirmaz, Jeff Paris

Publication date 1984

Published in Mathematical Logic Quarterly (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1002/malq.19840301907

zbMATH Keywords

2-sorted Peano modelsFloyd-Hoare program verification methodNonstandard Dynamic Logic

Mathematics Subject Classification ID

Classical first-order logic (03B10) Modal logic (including the logic of norms) (03B45) Nonstandard models of arithmetic (03H15) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Non-standard algorithmic and dynamic logic
• Peano arithmetic as axiomatization of the time frame in logics of programs and in dynamic logics
• scientific article; zbMATH DE number 4080898
• scientific article; zbMATH DE number 3905832
• Program correctness on finite fields

Cited in

(7)

• Non-standard algorithmic and dynamic logic
• Hoare's logic for nondeterministic regular programs: A nonstandard approach
• A faithful embedding of parallel computations in star-finite models
• Recursive programs and denotational semantics in absolute logics of programs
• Changing a Semantics: Opportunism or Courage?
• The axiomatic semantics of programs based on Hoare's logic
• On the strength of temporal proofs

This page was built for publication: A PROPERTY OF 2‐SORTED PEANO MODELS AND PROGRAM VERIFICATION

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