{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T03:52:53Z","timestamp":1725594773462},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642221095"},{"type":"electronic","value":"9783642221101"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22110-1_43","type":"book-chapter","created":{"date-parts":[[2011,7,4]],"date-time":"2011-07-04T09:08:45Z","timestamp":1309770525000},"page":"541-556","source":"Crossref","is-referenced-by-count":12,"title":["Formalization and Automated Verification of RESTful Behavior"],"prefix":"10.1007","author":[{"given":"Uri","family":"Klein","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kedar S.","family":"Namjoshi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"43_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.K.: General decidability theorems for infinite-state systems. In: LICS (1996)","DOI":"10.1109\/LICS.1996.561359"},{"key":"43_CR2","volume-title":"Compilers: Principles, Techniques, & Tools","author":"A.V. Aho","year":"2007","unstructured":"Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, & Tools, 2nd edn. Addison-Wesley, Reading (2007)","edition":"2"},{"key":"43_CR3","unstructured":"Bizer, C., Heath, T., Idehen, K., Berners-Lee, T.: Linked data on the web (LDOW2008). In: WWW, pp. 1265\u20131266 (2008), talk by Tim Berners-Lee at TED (2009), http:\/\/www.w3.org\/2009\/Talks\/0204-ted-tbl\/"},{"key":"43_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, Springer, Heidelberg (1982)"},{"key":"43_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Automata, Languages and Programming","author":"E. Emerson","year":"1980","unstructured":"Emerson, E., Clarke, E.: Proving correctness of parallel programs using fixpoints. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol.\u00a085, Springer, Heidelberg (1980)"},{"key":"43_CR6","doi-asserted-by":"crossref","unstructured":"Erenkrantz, J.R., Gorlick, M.M., Suryanarayana, G., Taylor, R.N.: From representations to computations: the evolution of web architectures. In: ESEC\/SIGSOFT FSE, pp. 255\u2013264 (2007)","DOI":"10.1145\/1287624.1287660"},{"key":"43_CR7","unstructured":"Fielding, R., Gettys, J., Mogul, J., Frystyk, H., Masinter, L., Leach, P., Berners-Lee, T.: W3C RFC 2616 (June 1999), http:\/\/www.w3.org\/Protocols\/rfc2616\/rfc2616.html"},{"key":"43_CR8","unstructured":"Fielding, R.T.: Architectural Styles and the Design of Network-based Software Architectures. Ph.D. thesis, University of California, Irving (2000)"},{"key":"43_CR9","unstructured":"Fielding, R.T.: (2008), http:\/\/roy.gbiv.com\/untangled\/2008\/no-rest-in-cmis#comment-697"},{"key":"43_CR10","unstructured":"Fielding, R.T.: (2008), http:\/\/roy.gbiv.com\/untangled\/2008\/rest-apis-mustbe-hypertext-driven"},{"key":"43_CR11","doi-asserted-by":"crossref","unstructured":"German, S., Sistla, A.: Reasoning about systems with many processes. Journal of the ACM (1992)","DOI":"10.1145\/146637.146681"},{"issue":"3","key":"43_CR12","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M. Herlihy","year":"1990","unstructured":"Herlihy, M., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst.\u00a012(3), 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"43_CR13","doi-asserted-by":"crossref","unstructured":"Hern\u00e1ndez, A.G., Garc\u00eda, M.N.M.: A formal definition of RESTful semantic web services. In: WS-REST, pp. 39\u201345 (2010)","DOI":"10.1145\/1798354.1798384"},{"key":"43_CR14","volume-title":"The SPIN Model Checker","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker. Addison-Wesley, Reading (2003), http:\/\/spinroot.com"},{"key":"43_CR15","doi-asserted-by":"crossref","unstructured":"Klein, U., Namjoshi, K.S.: Formalization and Automated Verification of RESTful Behavior. Tech. rep., Bell Labs; Courant Institute of Mathematical Sciences, NYU TR2011-938 (2011)","DOI":"10.1007\/978-3-642-22110-1_43"},{"key":"43_CR16","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Proc. of the Conf. on Logics of Programs (1985)","DOI":"10.1007\/3-540-15648-8_16"},{"key":"43_CR17","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1990","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1990)"},{"key":"43_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-69738-1_22","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"K.S. Namjoshi","year":"2007","unstructured":"Namjoshi, K.S.: Symmetry and completeness in the analysis of parameterized systems. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 299\u2013313. Springer, Heidelberg (2007)"},{"key":"43_CR19","volume-title":"Computational Complexity","author":"C.H. Papadimitriou","year":"1994","unstructured":"Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)"},{"key":"43_CR20","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"43_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"2001","unstructured":"Pnueli, A., Ruah, S., Zuck, L.D.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 82\u201397. Springer, Heidelberg (2001)"},{"key":"43_CR22","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"43_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J. Queille","year":"1982","unstructured":"Queille, J., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol.\u00a0137, Springer, Heidelberg (1982)"},{"key":"43_CR24","unstructured":"Vardi, M., Wolper, P.: An automata-theoretic approach to automatic program verification. In: IEEE Symposium on Logic in Computer Science (1986)"},{"issue":"2","key":"43_CR25","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W. Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng.\u00a010(2), 203\u2013232 (2003), http:\/\/babelfish.arc.nasa.gov\/trac\/jpf","journal-title":"Autom. Softw. Eng."},{"key":"43_CR26","unstructured":"SOAP version 1.2 part 1: Messaging framework (second edition). W3C Recommendation (2007), http:\/\/www.w3.org\/TR\/soap12-part1\/"},{"key":"43_CR27","unstructured":"Uniform Resource Identifier (URI): Generic Syntax. W3C RFC 3986 (2005)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22110-1_43","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T13:41:00Z","timestamp":1560346860000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22110-1_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642221095","9783642221101"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22110-1_43","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}