{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T16:41:35Z","timestamp":1725900095413},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642305603"},{"type":"electronic","value":"9783642305610"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-30561-0_2","type":"book-chapter","created":{"date-parts":[[2012,5,25]],"date-time":"2012-05-25T18:31:43Z","timestamp":1337970703000},"page":"9-16","source":"Crossref","is-referenced-by-count":3,"title":["Poporo: A Formal Methods Tool for Fast-Checking of Social Network Privacy Policies"],"prefix":"10.1007","author":[{"given":"N\u00e9stor","family":"Cata\u00f1o","sequence":"first","affiliation":[]},{"given":"Sorren","family":"Hanvey","sequence":"additional","affiliation":[]},{"given":"Camilo","family":"Rueda","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","unstructured":"Appel, A.W.: Foundational proof-carrying code. In: LCS (2001)"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Backes, M., Bagga, W., Karjoth, G., Schunter, M.: Efficient Comparison of Enterprise Privacy Policies. IBM Research, Zurich Research Laboratory (September 2003)","DOI":"10.1145\/967900.967983"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-92188-2_1","volume-title":"Formal Methods for Components and Objects","author":"G. Barthe","year":"2008","unstructured":"Barthe, G., Cr\u00e9gut, P., Gr\u00e9goire, B., Jensen, T., Pichardie, D.: The MOBIUS Proof Carrying Code Infrastructure. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol.\u00a05382, pp. 1\u201324. Springer, Heidelberg (2008)"},{"issue":"1-3","key":"2_CR4","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/j.scico.2004.05.011","volume":"55","author":"C. Breunesse","year":"2005","unstructured":"Breunesse, C., Cata\u00f1o, N., Huisman, M., Jacobs, B.: Formal methods for smart cards: An experience report. Science of Computer Programming\u00a055(1-3), 53\u201380 (2005)","journal-title":"Science of Computer Programming"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/978-3-642-11811-1_20","volume-title":"Abstract State Machines, Alloy, B and Z","author":"N. Cata\u00f1o","year":"2010","unstructured":"Cata\u00f1o, N., Rueda, C.: Matelas: A Predicate Calculus Common Formal Definition for Social Networking. In: Frappier, M., Gl\u00e4sser, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol.\u00a05977, pp. 259\u2013272. Springer, Heidelberg (2010)"},{"key":"2_CR6","unstructured":"Cata\u00f1o, N., Rueda, C., Hanvey, S.: The Poporo tool (2011), \n                  \n                    http:\/\/poporo.uma.pt\/~ncatano\/Projects\/wespfm\/Poporo\/poporo.php"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Cata\u00f1o, N., Rueda, C., Hanvey, S.: Verification of jml generic types with yices. In: CCC (2011)","DOI":"10.1109\/COLOMCC.2011.5936279"},{"key":"2_CR8","unstructured":"Cata\u00f1o, N., Wahls, T., Rueda, C., Rivera, V., Yu, D.: Translating B machines to JML specifications. In: SAC-SVT (to appear, 2012)"},{"key":"2_CR9","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Inc. (October 1976)"},{"key":"2_CR10","unstructured":"Duterte, B., de Moura, L.: The Yices SMT solver. Technical report, Computer Science Laboratory, SRI International (2006)"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"issue":"3","key":"2_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"G.T. Leavens","year":"2006","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. ACM SIGSOFT\u00a031(3), 1\u201338 (2006)","journal-title":"ACM SIGSOFT"},{"key":"2_CR13","unstructured":"Moses, T.: eXtensible Access Control Markup Language (XACML) Version 2.0. OASIS (2005)"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Sadeh, N., Gandon, F.: Semantic web technologies to reconcile privacy and context awareness. Journal of Web Semantics\u00a01 (2004)","DOI":"10.2139\/ssrn.3199020"}],"container-title":["Lecture Notes in Computer Science","Objects, Models, Components, Patterns"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-30561-0_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T07:44:51Z","timestamp":1620114291000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-30561-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642305603","9783642305610"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-30561-0_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}