{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:24:10Z","timestamp":1725560650292},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540283720"},{"type":"electronic","value":"9783540318200"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11541868_6","type":"book-chapter","created":{"date-parts":[[2010,7,20]],"date-time":"2010-07-20T19:12:52Z","timestamp":1279653172000},"page":"82-97","source":"Crossref","is-referenced-by-count":1,"title":["Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS"],"prefix":"10.1007","author":[{"given":"N\u00e9stor","family":"Cata\u00f1o","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"FMICS: Eighth International Workshop on Formal Methods for Industrial Critical Systems","author":"N. Cata\u00f1o","year":"2003","unstructured":"Cata\u00f1o, N.: Slicing event spaces: Towards a Java programs checking framework. In: Arts, T., Fokkink, W. (eds.) Pictorial Information Systems. LNCS, vol.\u00a080. Elsevier, Amsterdam (2003)"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/3-540-48737-9_5","volume-title":"Formal Syntax and Semantics of Java","author":"P. Cenciarelli","year":"1999","unstructured":"Cenciarelli, P., Knapp, A., Reus, B., Wirsing, M.: An event-based structural operational semantics of multi-threaded Java. In: Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java. LNCS, vol.\u00a01523, pp. 157\u2013200. Springer, Heidelberg (1999)"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/3-540-36577-X_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Ciardo","year":"2003","unstructured":"Ciardo, G., Marmorstein, R., Siminiceanu, R.: Saturation unbound. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 379\u2013393. Springer, Heidelberg (2003)"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proceedings of Logics of Programs, Yorktown Heights, New York, May 1981. LNCS, pp. 52\u201371 (1981)","DOI":"10.1007\/BFb0025774"},{"key":"6_CR5","first-page":"169","volume-title":"Proceedings of 14th Symposium on Theory of Computing (STOC 1982)","author":"E.A. Emerson","year":"1982","unstructured":"Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. In: Proceedings of 14th Symposium on Theory of Computing (STOC 1982), San Francisco, CA, pp. 169\u2013180. ACM, New York (1982)"},{"key":"6_CR6","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem","author":"P. Godefroid","year":"1996","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems, vol.\u00a01032, p. 142. Springer, Heidelberg (1996)"},{"key":"6_CR7","series-title":"The Java Series","volume-title":"The Java Language Specification","author":"J. Gosling","year":"2000","unstructured":"Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 2nd edn. The Java Series. Addison-Wesley, Reading (2000)","edition":"2"},{"key":"6_CR8","volume-title":"PVS Language Reference","author":"S. Owre","year":"2001","unstructured":"Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Language Reference. Computer Science Laboratory, Menlo Park (2001)"},{"key":"6_CR9","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1145\/304065.304106","volume-title":"Proceedings of the ACM 1999 conference on Java Grande","author":"W. Pugh","year":"1999","unstructured":"Pugh, W.: Fixing the Java memory model. In: Proceedings of the ACM 1999 conference on Java Grande, pp. 89\u201398. ACM Press, New York (1999)"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/3-540-44659-1_30","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Reus","year":"2000","unstructured":"Reus, B., Hein, T.: Towards a machine-checked Java specification book. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 480\u2013497. Springer, Heidelberg (2000)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11541868_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:18:15Z","timestamp":1605644295000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11541868_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540283720","9783540318200"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/11541868_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}