Proving total correctness of nondeterministic programs in infinitary logic

DOI10.1007/BF00289263zbMath0467.03028MaRDI QIDQ1155605

Ralph-Johan Back

Publication date: 1981

Published in: Acta Informatica (Search for Journal in Brave)

zbMATH Keywords

Dijkstra's guarded commandshierarchically structured programs

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Other infinitary logic (03C75)

Related Items (11)

Stratified least fixpoint logic ⋮ While-programs with nondeterministic assignments and the logic ALNA ⋮ The Rely-Guarantee method for verifying shared variable concurrent programs ⋮ A calculus of refinements for program derivations ⋮ In praise of algebra ⋮ A continuous semantics for unbounded nondeterminism ⋮ Formalizing Dijkstra's predicate transformer wp in weak second-order logic ⋮ Combining dynamic and static slicing for analysing assembler ⋮ A logic of recursion ⋮ Verifiable properties of database transactions ⋮ A simple fixpoint argument without the restriction to continuity

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Large infinitary languages. Model theory
• First-order dynamic logic
• Model theory for infinitary logic. Logic with countable conjunctions and finite quantifiers
• A Weaker Precondition for Loops

This page was built for publication: Proving total correctness of nondeterministic programs in infinitary logic