Eliminating the substitution axiom from UNITY logic

DOI10.1007/BF01898402zbMath0715.68059WikidataQ114693749 ScholiaQ114693749MaRDI QIDQ751848

Beverly A. Sanders

Publication date: 1991

Published in: Formal Aspects of Computing (Search for Journal in Brave)

zbMATH Keywords

completenessUNITYprogram compositionsubstitution axiom

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (15)

Distributed maximum maintenance on hierarchically divided graphs ⋮ Error in the UNITY substitution rule for subscripted operators ⋮ Invariants, composition, and substitution ⋮ DUALITY: A simple formalism for the analysis of UNITY ⋮ A predicate transformer for the progress property `to-always' ⋮ Logical foundations for compositional verification and development of concurrent programs in UNITY ⋮ On mechanizing proofs within a complete proof system for Unity ⋮ A foundation for modular reasoning about safety and progress properties of state-based concurrent programs ⋮ Comments on Always-true is not invariant: Assertional reasoning about invariance ⋮ A simple proof of a completeness result for \(leads\)-\(to\) in the UNITY logic ⋮ On the logic of UNITY ⋮ Web Cube ⋮ Composing leads-to properties ⋮ Models for the substitution axiom of UNITY logic ⋮ Program refinement in fair transition systems

Uses Software

• UNITY

Cites Work

• A predicate transformer for progress
• Formal verification of parallel programs
• Soundness and Completeness of an Axiom System for Program Verification
• Unnamed Item
• Unnamed Item

This page was built for publication: Eliminating the substitution axiom from UNITY logic