Nissim Francez, Michael Rodeh
IEEE Transactions on Software Engineering
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. © 1983 Springer-Verlag.
Nissim Francez, Michael Rodeh
IEEE Transactions on Software Engineering
Tzilla Elrad, Nissim Francez
Theoretical Computer Science
Martín Abadi, Bowen Alpern, et al.
Information Processing Letters
Tzilla Elrad, Nissim Francez
Science of Computer Programming