×

Méthode axiomatique pour les propriétés de fatalité des programmes pralleles. (French) Zbl 0623.68027

Eventuality properties under fairness hypothesis have led us to design a temporal-based proof system. This proof system takes into account the fairness hypothesis and contains an induction rule relative to the number of concurrent processes. We limit our investigations to concurrent programs sharing common variables and using semaphores as synchronization primitives.

MSC:

68N25 Theory of operating systems
PDFBibTeX XMLCite
Full Text: DOI EuDML

References:

[1] 1. APT et DELPORTE [1983], Syntax-Directed Analysis of Liveness Properties, RR83-42, octobre 1983, L.I.T.P., Université de Paris-VII, France.
[2] 2. BARRINGER, KUIPER et PNUELI [1984], Now You May Compose Your Temporal Logic Specification, dans A.C.M.-Proceedings Theory of Computing.
[3] 3. BURSTALL [1974], Program Proving as Hand Simulation with a Little Induction, dans Proceedings I.F.I.P, 1974, p. 308-312, Amsterdam 1974, The Netherlands. Zbl0299.68012 MR448980 · Zbl 0299.68012
[4] 4. COUSOT [1985], Fondements des méthodes de preuve d’invariance et de fatalité de programmes parallèles, Thèse d’état, novembre 1985, I.N.P.L.
[5] 5. FLOYD [1967], Assigning Meaning to Programs, dans Proc. A.M.S. Symposium dans Applied Hath. Amer. Math. Soc., 1967, p. 19-31. Zbl0189.50204 MR235771 · Zbl 0189.50204
[6] 6. GERTH [1984], TRANSITION LOGIC: How to Reason About Temporal Properties of Programs in a Compositional Way, dans RUU-CS-83-17, février 1984, Rijsuni-versiteit Utrecht, The Netherlands.
[7] 7. HOARE [1969], An Axiomatic Basis for Computer Programming, dans Communications of A.C.M., vol. 12, 1969, p. 576-583. Zbl0179.23105 · Zbl 0179.23105 · doi:10.1145/363235.363259
[8] 8. LAMPORT [1980 a], SOMETIME is Sometimes Better than ALWAYS, dans Proceedings of the A.C.M. Symposium on the Principles of Programming Languages, 1980.
[9] 9. LAMPORT [1980 b], The HOARE Logic of Concurrent Programs, dans Acta Informatica, vol. 14, 1980, p. 21-37. Zbl0416.68032 MR581379 · Zbl 0416.68032 · doi:10.1007/BF00289062
[10] 10. LEHMAN, PNUELI et STAVI [1981], Impartiality, Justice and Fairness: the Ethics of Concurrent Termination, dans I.C.A.L.P., 1981, L.N.C.S., n^\circ 115, p. 264-277. Zbl0468.68026 MR635142 · Zbl 0468.68026
[11] 11. MANNA et PNUELI [1982], Verification of Concurrent Programs: Proving Eventuality by Well-Founded Ranking, dans Report N.STAN-CS-82-915, mai 1982, Department of Computer Science, Stanford University, U.S.A.
[12] 12. MANNA et PNUELI [1983 a], How to Cook Your Temporal Proof System for Your Pet Language, dans Proceedings of P.O.P.L., 1983, Austin, Texas, janvier 1983.
[13] 13. MANNA et PNUELI [1983 b], Proving Precedence Properties: the Temporal Way, dans Report N.STAN-CS-83-964, Department of Computer Science, Stanford University, U.S.A. · Zbl 0528.68008
[14] 14. MANNA et PNUELI [1984], Adequate Proof Principles for Invariance and Liveness Properties of Concurrent Programs, dans Science of Computer Programming, vol. 4, 1984, p. 257-289, North-Holland. Zbl0542.68014 MR776776 · Zbl 0542.68014 · doi:10.1016/0167-6423(84)90003-0
[15] 15. OWICKI et LAMPORT [1982], Proving Liveness Properties of Concurrent Programs, dans ACM-TOPLAS, vol. 4, (3), 1982, p. 455-495. Zbl0483.68013 · Zbl 0483.68013 · doi:10.1145/357172.357178
[16] 16. PARK [1981], A Predicate Transformer for Weak Fair Iteration, dans Proc. of The sixth I.B.M. Symposium on mathematical Foundations of Computer Science, Hakone, Japan, 1981.
[17] 17. PNUELI [1977], The Temporal Logic of Programs, dans Proc. 18th Symposium on Foundations of Computer Science, Ri, 1977, p. 46-57. MR502161
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.