{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:20:23Z","timestamp":1725456023548},"publisher-location":"Berlin\/Heidelberg","reference-count":20,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540566627"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0024647","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T05:09:15Z","timestamp":1132722555000},"page":"196-215","source":"Crossref","is-referenced-by-count":5,"title":["A proof environment for concurrent programs"],"prefix":"10.1007","author":[{"given":"Na\u00efma","family":"Brown","sequence":"first","affiliation":[]},{"given":"Dominique","family":"Mery","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","unstructured":"R.S. Boyer and J.S. Moore. A Computational Logic Handbook. Academic Press, 1988."},{"key":"14_CR2","unstructured":"N. Brown and D. Mery. Deriving Occam Programs through the Refinement of Unity-like Specifications. In W. Joosen and E. Milgrom, editors, Proceedings European Workshop on Parallel Computing. IOS PRESS, 1992."},{"key":"14_CR3","unstructured":"R.J.R. Back and K. Sere. Deriving an occam implementation of action systems. In C. Morgan and J.C.P. Woodcock, editors, 4rd Refinement Workshop. Springer-Verlag, January 1991. BCS-FACS, Workshops in Computing."},{"key":"14_CR4","unstructured":"BP Innovation Centre and Edinburgh Portable Compilers Ltd. B-Tool Versionl. 1, Reference Manual, 1991."},{"key":"14_CR5","unstructured":"BP Innovation Centre and Edinburgh Portable Compilers Ltd. B-Tool Versionl.1, Tutorial, 1991."},{"key":"14_CR6","unstructured":"P Innovation Centre and Edinburgh Portable Compilers Ltd. B-Tool Versionl.1, User Manual, 1991."},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Centaur. Version1.1, Reference Manual, 1991.","DOI":"10.1007\/978-1-4615-3678-9_1"},{"key":"14_CR8","unstructured":"Centaur. Version1.2, Reference Manual, 1992."},{"key":"14_CR9","unstructured":"K.M. Chandy and J. Misra. Parallel Program Design A Foundation. Addison-Wesley Publishing Company, 1988. ISBN 0-201-05866-9."},{"key":"14_CR10","unstructured":"E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976."},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"E.W. Dijkstra and C.S. Scholten. Predicate Calculus and Program Semantics. Texts and Monographs in Computer Science. Springer Verlag, 1990.","DOI":"10.1007\/978-1-4612-3228-5"},{"issue":"9","key":"14_CR12","doi-asserted-by":"publisher","first-page":"1005","DOI":"10.1109\/32.58787","volume":"16","author":"D.M. Goldschlag","year":"1990","unstructured":"D.M. Goldschlag. Mechanically verifying concurrent programs with the boyermoore prover. IEEE Transactions on Software Engineering, 16(9):1005\u20131023, September 1990.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"14_CR13","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1016\/0020-0190(90)90027-U","volume":"35","author":"A.J.M. Gasteren Van","year":"1990","unstructured":"A.J.M. Van Gasteren and G. Tel. Comments on \u201don the proof of a distributed algorithm\u201d: always true is not invariant. Information Processing Letters, 35:277\u2013279, 1990.","journal-title":"Information Processing Letters"},{"issue":"2","key":"14_CR14","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1145\/78942.78945","volume":"12","author":"E. Knapp","year":"1990","unstructured":"E. Knapp. An exercise in the formal derivation of parallel programs: Maximum flows in graphs. Transactions On Programming Languages and Systems, 12(2):203\u2013223, 1990.","journal-title":"Transactions On Programming Languages and Systems"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"L. Lamport. Proving the correctness of multiprocess programs. Trans. on Software Engineering 1, 1977.","DOI":"10.1109\/TSE.1977.229904"},{"key":"14_CR16","unstructured":"L. Lamport. A temporal logic of actions. Technical Report 57, DEC Palo Alto, april 1990."},{"key":"14_CR17","volume-title":"LNCS","author":"D. Mery","year":"1986","unstructured":"D. Mery. A proof system to derive eventuality properties under justice hypothesis. In LNCS, number 233. Mathematical Foundations of Computer Science, 1986. Bratislava, Tchecoslovaquie."},{"issue":"2","key":"14_CR18","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/0304-3975(92)90041-D","volume":"94","author":"D. Mery","year":"1992","unstructured":"D. Mery. The NU system as a development system for concurrent programs: \u03b4 NU. Theoretical Computer Science, 94(2):311\u2013334, march 1992.","journal-title":"Theoretical Computer Science"},{"key":"14_CR19","unstructured":"J. Misra. Soundness of the substitution axiom. Notes on Unity, pages 14\u201390, 1990."},{"key":"14_CR20","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/BF01898402","volume":"3","author":"B.A. Sanders","year":"1991","unstructured":"B.A. Sanders. Eliminating the substitution axiom from unity logic. Formal Aspects of Computing, 3:189\u2013205, 1991.","journal-title":"Formal Aspects of Computing"}],"container-title":["Lecture Notes in Computer Science","FME '93: Industrial-Strength Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0024647","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T00:53:13Z","timestamp":1586566393000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0024647"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540566627"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/bfb0024647","relation":{},"subject":[]}}