Product properties and their direct verification
Copyright policy )Product properties and their direct verification
The paper presents a family of properties of programs, called product (and power) properties, for which the verification method of Floyd and Hoare are inconvenient. A (semantically) complete alternative method is proposed' The paper presents the method in both the endogenous and exogenous versions and applies them to examples. Semantic completeness and soundness are shown. The method is particularly useful for some second-order programs, having procedures as parameters.
- IBM (United States) United States
Specification and verification (program logics, model checking, etc.), Floyd method, soundness, semantic completeness, second- order programs, Hoare method
Specification and verification (program logics, model checking, etc.), Floyd method, soundness, semantic completeness, second- order programs, Hoare method
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).7 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Top 10% influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!