{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T16:20:14Z","timestamp":1743006014625,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540408284"},{"type":"electronic","value":"9783540452362"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45236-2_39","type":"book-chapter","created":{"date-parts":[[2010,6,26]],"date-time":"2010-06-26T00:08:38Z","timestamp":1277510918000},"page":"719-738","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Composing Temporal-Logic Specifications with Machine Assistance"],"prefix":"10.1007","author":[{"given":"Jei-Wen","family":"Teng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yih-Kuen","family":"Tsay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,9,25]]},"reference":[{"key":"39_CR1","doi-asserted-by":"crossref","unstructured":"Clarke, E., Long, D., McMillan, K.: Compositional model checking. In: Proceedings of the 4th IEEE Symposium on Logic in Computer Science, pp. 353\u2013362 (1989)","DOI":"10.1109\/LICS.1989.39190"},{"key":"39_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/3-540-56922-7_14","volume-title":"Computer Aided Verification","author":"R. Kurshan","year":"1993","unstructured":"Kurshan, R., Lamport, L.: Verification of a multiplier: 64 bits and beyond. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 166\u2013179. Springer, Heidelberg (1993)"},{"key":"39_CR3","volume-title":"Component Software: Beyond Object-Oriented Programming","author":"C. Szyperski","year":"1998","unstructured":"Szyperski, C.: Component Software: Beyond Object-Oriented Programming. Addison-Wesley, Reading (1998)"},{"key":"39_CR4","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1982","unstructured":"Pnueli, A.: The temporal semantics of concurrent programs. Theoretical Computer Science\u00a013, 45\u201360 (1982)","journal-title":"Theoretical Computer Science"},{"key":"39_CR5","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Transactions on Programming Languages and Systems\u00a016, 872\u2013923 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"39_CR6","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1995)"},{"key":"39_CR7","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1145\/203095.201069","volume":"17","author":"M. Abadi","year":"1995","unstructured":"Abadi, M., Lamport, L.: Conjoining specifications. ACM Transactions on Programming Languages and Systems\u00a017, 507\u2013534 (1995)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"#cr-split#-39_CR8.1","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Tsay, Y.K.: Assumption\/guarantee specifications in linear-time temporal logic. Theoretical Computer Science\u00a0167, 47-72 (1996)","DOI":"10.1016\/0304-3975(96)00069-2"},{"key":"#cr-split#-39_CR8.2","unstructured":"An extended abstract appeared earlier in Mosses, P.D., Schwartzbach, M.I., Nielsen, M. (eds.): CAAP 1995, FASE 1995, and TAPSOFT 1995. LNCS, vol.\u00a0915. Springer, Heidelberg (1995)"},{"key":"39_CR9","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C. Hoare","year":"1969","unstructured":"Hoare, C.: An axiomatic basis for computer programs. Communications of the ACM\u00a012, 576\u2013580 (1969)","journal-title":"Communications of the ACM"},{"key":"39_CR10","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"7","author":"J. Misra","year":"1981","unstructured":"Misra, J., Chandy, K.: Proofs of networks of processes. IEEE Transactions on Software Engineering\u00a07, 417\u2013426 (1981)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"39_CR11","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"C. Jones","year":"1983","unstructured":"Jones, C.: Tentative steps towards a development method for interfering programs. ACM Transactions on Programming Languages and Systems\u00a05, 596\u2013619 (1983)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"39_CR12","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1145\/69624.357207","volume":"5","author":"L. Lamport","year":"1983","unstructured":"Lamport, L.: Specifying concurrent program modules. ACM Transactions on Programming Languages and Systems\u00a05, 190\u2013222 (1983)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"39_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/3-540-46432-8_23","volume-title":"Foundation of Software Science and Computation Structures","author":"Y.K. Tsay","year":"2000","unstructured":"Tsay, Y.K.: Compositional verification in linear-time temporal logic. In: Tiuryn, J. (ed.) FOSSACS 2000. LNCS, vol.\u00a01784, pp. 344\u2013358. Springer, Heidelberg (2000)"},{"key":"39_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1992)"},{"key":"39_CR15","unstructured":"Crow, J., Owre, S., Rushby, J., Shankar, N., Srivas, M.: A tutorial introduction to PVS. Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA (1995)"},{"key":"39_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/3-540-15670-4_2","volume-title":"Seminar on Concurrency","author":"H. Barringer","year":"1984","unstructured":"Barringer, H., Kuiper, R.: Hierarchical development of concurrent systems in a temporal logic framework. In: Brookes, S.D., Winskel, G., Roscoe, A.W. (eds.) Seminar on Concurrency. LNCS, vol.\u00a0197, pp. 35\u201361. Springer, Heidelberg (1984)"},{"key":"39_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/3-540-53487-3_55","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"P. Gr\u00f8nning","year":"1991","unstructured":"Gr\u00f8nning, P., Nielsen, T., L\u00f8vengreen, H.: Refinement and composition of transition-based rely-guarantee specifications with auxiliary variables. In: Veni Madhavan, C.E., Nori, K.V. (eds.) FSTTCS 1990. LNCS, vol.\u00a0472, pp. 332\u2013348. Springer, Heidelberg (1991)"},{"key":"39_CR18","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/151646.151649","volume":"15","author":"M. Abadi","year":"1993","unstructured":"Abadi, M., Lamport, L.: Composing specifications. ACM Transactions on Programming Languages and Systems\u00a015, 73\u2013132 (1993)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"39_CR19","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(93)90151-I","volume":"114","author":"M. Abadi","year":"1993","unstructured":"Abadi, M., Plotkin, G.: A logical view of composition. Theoretical Computer Science\u00a0114, 3\u201330 (1993)","journal-title":"Theoretical Computer Science"},{"key":"39_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/3-540-56610-4_67","volume-title":"TAPSOFT \u201993: Theory and Practice of Software Development","author":"P. Collette","year":"1993","unstructured":"Collette, P.: Application of the composition principle to Unity-like specifications. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) CAAP 1993, FASE 1993, and TAPSOFT 1993. LNCS, vol.\u00a0668, pp. 230\u2013242. Springer, Heidelberg (1993)"},{"key":"39_CR21","unstructured":"Collette, P.: Design of Compositional Proof Systems Based on Assumption- Guarantee Specifications \u2014 Application to UNITY. PhD thesis, Universit\u00e9 Catholique de Louvain (1994)"},{"key":"39_CR22","series-title":"Lecture Notes in Computer Science","first-page":"267","volume-title":"CONCUR \u201994: Concurrency Theory","author":"Q. Xu","year":"1994","unstructured":"Xu, Q., Cau, A., Collette, P.: On unifying assumption-commitment style proof rules for concurrency. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol.\u00a0836, pp. 267\u2013282. Springer, Heidelberg (1994)"},{"key":"39_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/BFb0105408","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Heckman","year":"1996","unstructured":"Heckman, M., Zhang, C., Becker, B., Peticolas, D., Levitt, K., Olsson, R.: Towards applying the composition principle to verify a microkernel operating system. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 235\u2013250. Springer, Heidelberg (1996)"},{"key":"39_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/3-540-56496-9_5","volume-title":"Computer Aided Verification","author":"U. Engberg","year":"1992","unstructured":"Engberg, U., Gr\u00f8nning, P., Lamport, L.: Mechanical verification of concurrent systems with TLA. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol.\u00a0663, pp. 44\u201355. Springer, Heidelberg (1992)"},{"key":"39_CR25","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1002\/j.1538-7305.1990.tb00102.x","volume":"69","author":"Z. Har\u2019El","year":"1990","unstructured":"Har\u2019El, Z., Kurshan, R.: Software for analytical development of communication protocols. AT&T Technical Journal\u00a069, 45\u201359 (1990)","journal-title":"AT&T Technical Journal"},{"key":"39_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/3-540-49213-5_21","volume-title":"Compositionality: The Significant Difference","author":"N. Shankar","year":"1998","unstructured":"Shankar, N.: Lazy compositional verification. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol.\u00a01536, pp. 541\u2013564. Springer, Heidelberg (1998)"},{"key":"39_CR27","first-page":"499","volume":"158","author":"N. Shankar","year":"1997","unstructured":"Shankar, N.: Machine-assisted verification using theorem proving and model checking. Computer and Systems Science\u00a0158, 499\u2013528 (1997)","journal-title":"Computer and Systems Science"},{"key":"39_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-57826-9_121","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"F. Andersen","year":"1994","unstructured":"Andersen, F., Petersen, K., Petterson, J.: Program verification using HOL-UNITY. In: Joyce, J.J., Seger, C.-J.H. (eds.) HUG 1993. LNCS, vol.\u00a0780, pp. 1\u201316. Springer, Heidelberg (1994)"},{"key":"39_CR29","volume-title":"Parallel Program Design: A Foundation","author":"K. Chandy","year":"1988","unstructured":"Chandy, K., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Reading (1988)"},{"key":"39_CR30","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-1-4613-2007-4_3","volume-title":"VLSI Specification, Verification and Synthesis","author":"M. Gordon","year":"1988","unstructured":"Gordon, M.: HOL: A proof generating system for higher-order logic. In: Birtwistle, G., Subrahmanyam, P. (eds.) VLSI Specification, Verification and Synthesis, pp. 73\u2013128. Kluwer, Dordrecht (1988)"},{"key":"39_CR31","doi-asserted-by":"crossref","unstructured":"L\u00e5ngbacka, T.: A HOL formalization of the temporal logic of actions. In: Higher Order Logic Theorem Proving System and Its Applications, 7th International Workshop (1994)","DOI":"10.1007\/3-540-58450-1_52"},{"key":"39_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/3-540-63533-5_31","volume-title":"FME \u201997 Industrial Applications and Strengthened Foundations of Formal Methods","author":"P. Kellom\u00e4ki","year":"1997","unstructured":"Kellom\u00e4ki, P.: Verification of reactive systems using DisCo and PVS. In: Fitzgerald, J.S., Jones, C.B., Lucas, P. (eds.) FME 1997. LNCS, vol.\u00a01313, pp. 589\u2013604. Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","FME 2003: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45236-2_39","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T08:02:04Z","timestamp":1740211324000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45236-2_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540408284","9783540452362"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45236-2_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"25 September 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}