A PROPERTY OF 2‐SORTED PEANO MODELS AND PROGRAM VERIFICATION

DOI10.1002/malq.19840301907zbMath0564.03049OpenAlexW2087126378MaRDI QIDQ3677763

Jeffrey Bruce Paris, László Csirmaz

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

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

Related Items (7)

Non-standard algorithmic and dynamic logic ⋮ Changing a Semantics: Opportunism or Courage? ⋮ Recursive programs and denotational semantics in absolute logics of programs ⋮ Hoare's logic for nondeterministic regular programs: A nonstandard approach ⋮ A faithful embedding of parallel computations in star-finite models ⋮ 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