{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:10:21Z","timestamp":1725455421702},"publisher-location":"Berlin\/Heidelberg","reference-count":17,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540167838"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0016280","type":"book-chapter","created":{"date-parts":[[2005,11,13]],"date-time":"2005-11-13T05:39:17Z","timestamp":1131860357000},"page":"536-544","source":"Crossref","is-referenced-by-count":1,"title":["A proof system to derive eventuality properties under justice hypothesis"],"prefix":"10.1007","author":[{"given":"Dominique","family":"Mery","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"51_CR1","unstructured":"APT and DELPORTE (1983):\"Syntax-directed analysis of liveness properties\" in RR83-42, october 1983,LITP,Universite de PARIS VII,FRANCE."},{"key":"51_CR2","doi-asserted-by":"crossref","unstructured":"BEN-ARI (1982):\"On-the-fly garbage collection:New algorithms inspired from proofs\" in 9th ICALP, LNCS No140, july 1982.","DOI":"10.1007\/BFb0012753"},{"key":"51_CR3","unstructured":"BURSTALL (1974):\"Program proving as hand simulation with a little induction\" in Proc. IFIP 1974,pp 308\u2013312,Amsterdam,The Netherlands."},{"key":"51_CR4","unstructured":"COUSOT (1985):\"Fondements des m\u00e9thodes de preuves d'invariance et de fatalit\u00e9 de programmes parall\u00e8les\", Th\u00e8se d'\u00e9tat,nov. 1985,INPL,NANCY,FRANCE."},{"key":"51_CR5","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"Hoare","year":"1969","unstructured":"HOARE (1969):\"An axiomatic basis for computer programming\" in Com. of ACM 12,576\u2013583, 1969.","journal-title":"Com. of ACM"},{"key":"51_CR6","doi-asserted-by":"crossref","unstructured":"LAMPORT (1980a):\"'sometime\u2019 is sometimes better than Always\" in POPL 1980.","DOI":"10.1145\/567446.567463"},{"key":"51_CR7","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/BF00289062","volume":"14","author":"Lamport","year":"1980","unstructured":"LAMPORT (1980b):\"The HOARE logic of concurrent programs\" in Acta Informatica 14,21\u201337, 1980.","journal-title":"Acta Informatica"},{"key":"51_CR8","doi-asserted-by":"crossref","unstructured":"LEHMAN,PNUELI and STAVI (1981):\"Impartiality,Justice and Fairness:the ethics of concurrent termination\" in ICALP 1981, LNCS No115.","DOI":"10.1007\/3-540-10843-2_22"},{"key":"51_CR9","unstructured":"MANNA and PNUELI (1982):\"Verification of concurrent programs:proving eventuality by well-founded ranking\" in Report STAN-CS-82-915,may 1982,STANFORD university."},{"key":"51_CR10","unstructured":"MANNA and PNUELI (1983):\"Proving precedence properties:the temporal way\" in Report STAN-CS-83-964, STANFORD university."},{"key":"51_CR11","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/0167-6423(84)90003-0","volume":"4","author":"Manna","year":"1984","unstructured":"MANNA and PNUELI (1984):\"Adequate proof principles for invariance and liveness properties of concurrent programs\" in Science of Computer Programming 4, 1984,pp257\u2013289.","journal-title":"Science of Computer Programming"},{"key":"51_CR12","unstructured":"MERY (1983):\"Une m\u00e9thode axiomatique de preuves de propri\u00e9t\u00e9s de fatalit\u00e9 de programmes parall\u00e8les avec hypoth\u00e8se d'ex\u00e9cution \u00e9quitable\",Th\u00e8se 3ieme cycle,INPL,mai 1983, NANCY,FRANCE."},{"key":"51_CR13","unstructured":"MERY (1985):\"Preuves de propri\u00e9t\u00e9s de fatalit\u00e9 et de prec\u00e9dence sous hypoth\u00e8se d'ex\u00e9cution \u00e9quitable\", in Report LRIM-85-02,may 1985,Universit\u00e9 de METZ,FRANCE."},{"key":"51_CR14","unstructured":"MERY (1986):\"Quelques exemples de preuves de propri\u00e9t\u00e9s de fatalit\u00e9 dans le systeme axiomatique FEPS\",in Report LRIM-86-02,march 1986,Universit\u00e9 de METZ,FRANCE."},{"issue":"3","key":"51_CR15","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"Owicki","year":"1982","unstructured":"OWICKI and LAMPORT (1982):\"Proving liveness properties of concurrent programs\" in TOPLAS-ACM 4 (3), 1982,455\u2013495.","journal-title":"TOPLAS-ACM"},{"key":"51_CR16","unstructured":"PARK (1981):\"A predicate transformer for weak fair iteration\" in Proc. of the 6th IBM Symposium on mathematical foundations of computer science,hakone,Japan, 1981."},{"key":"51_CR17","unstructured":"PNUELI (1977):\"The temporal logic of programs\" in Proc. of the 18th FOCS, 1977."}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Computer Science 1986"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0016280.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T21:35:59Z","timestamp":1607549759000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0016280"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540167838"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/bfb0016280","relation":{},"subject":[]}}