{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T04:32:49Z","timestamp":1725769969853},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642541070"},{"type":"electronic","value":"9783642541087"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54108-7_5","type":"book-chapter","created":{"date-parts":[[2014,1,15]],"date-time":"2014-01-15T05:09:36Z","timestamp":1389762576000},"page":"88-107","source":"Crossref","is-referenced-by-count":4,"title":["Parallel Bounded Verification of Alloy Models by TranScoping"],"prefix":"10.1007","author":[{"given":"Nicol\u00e1s","family":"Rosner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carlos Gustavo","family":"L\u00f3pez Pombo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nazareno","family":"Aguirre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ali","family":"Jaoua","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ali","family":"Mili","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcelo F.","family":"Frias","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press (1996)","DOI":"10.1017\/CBO9780511624162"},{"issue":"1","key":"5_CR2","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s10270-008-0110-3","volume":"9","author":"K. Anastasakis","year":"2010","unstructured":"Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: On challenges of model trans- formation from UML to Alloy. Software and Systems Modeling\u00a09(1), 69\u201386 (2010)","journal-title":"Software and Systems Modeling"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/11804192_16","volume-title":"Formal Methods for Components and Objects","author":"P. Chalin","year":"2006","unstructured":"Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond Assertions: Advanced Specification and Verification with JML and ESC\/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 342\u2013363. Springer, Heidelberg (2006)"},{"key":"5_CR4","unstructured":"Chrabakh, W., Wolski, R.: GrADSAT: A Parallel SAT Solver for the Grid. In: UCSB Computer Science Technical Report Number 2003-05"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"5_CR6","unstructured":"MPI2: A Message Passing Interface Standard. Message Passing Interface Forum, High Performance Computing Applications\u00a012, 1\u20132, 1\u2013299 (1998)"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Dalcin, L., Paz, R., Storti, M., D\u2019Elia, J.: MPI for Python: Performance improvements and MPI-2 extensions. J. Parallel Distrib. Comput.\u00a068(5), 655\u2013662","DOI":"10.1016\/j.jpdc.2007.09.005"},{"key":"5_CR8","unstructured":"http:\/\/www.msoos.org\/cryptominisat2"},{"key":"5_CR9","unstructured":"Davies, J., Woodcock, J.: Using Z: Specification, Refinement and Proof. International Series in Computer Science. Prentice Hall (1996)"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Dennis, G., Chang, F., Jackson, D.: Modular Verification of Code with SAT. In: ISSTA 2006, pp. 109\u2013120 (2006)","DOI":"10.1145\/1146238.1146251"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Galeotti, J.P., Rosner, N., Pombo, C.L., Frias, M.F.: Analysis of invariants for efficient bounded verification. In: ISSTA 2010, pp. 25\u201336 (2010)","DOI":"10.1145\/1831708.1831712"},{"key":"5_CR12","doi-asserted-by":"crossref","first-page":"71","DOI":"10.3233\/SAT190063","volume":"6","author":"L. Gil","year":"2008","unstructured":"Gil, L., Flores, P., Silveira, L.M.: PMSat: a parallel version of MiniSAT. Journal on Satisfiability, Boolean Modeling and Computation\u00a06, 71\u201398 (2008)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Jackson, D., Schechter, I., Shlyakhter, I.: Alcoa: the alloy constraint analyzer. In: Proceedings of ICSE 2000, Limerick, Ireland (2000)","DOI":"10.1145\/337180.337616"},{"key":"5_CR14","unstructured":"Jackson, D.: Software Abstractions. MIT Press (2006)"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-642-24485-8_44","volume-title":"Model Driven Engineering Languages and Systems","author":"S. Maoz","year":"2011","unstructured":"Maoz, S., Ringert, J.O., Rumpe, B.: CD2Alloy: Class Diagrams Analysis Using Alloy Revisited. In: Whittle, J., Clark, T., K\u00fchne, T. (eds.) MODELS 2011. LNCS, vol.\u00a06981, pp. 592\u2013607. Springer, Heidelberg (2011)"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-642-11811-1_28","volume-title":"Abstract State Machines, Alloy, B and Z","author":"P. Malik","year":"2010","unstructured":"Malik, P., Groves, L., Lenihan, C.: Translating Z to Alloy. In: Frappier, M., Gl\u00e4sser, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol.\u00a05977, pp. 377\u2013390. Springer, Heidelberg (2010)"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-540-87603-8_34","volume-title":"Abstract State Machines, B and Z","author":"P.J. Matos","year":"2008","unstructured":"Matos, P.J., Marques-Silva, J.: Model Checking Event-B by Encoding into Alloy. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol.\u00a05238, pp. 346\u2013346. Springer, Heidelberg (2008)"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1007\/978-3-642-02777-2_47","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"K. Ohmura","year":"2009","unstructured":"Ohmura, K., Ueda, K.: c-sat: A Parallel SAT Solver for Clusters. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 524\u2013537. Springer, Heidelberg (2009)"},{"issue":"1","key":"5_CR19","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s00165-007-0058-z","volume":"20","author":"T. Ramananandro","year":"2008","unstructured":"Ramananandro, T.: Mondex, an electronic purse: specification and refinement checks with the Alloy model-finding method. Formal Aspects of Computing\u00a020(1), 21\u201339 (2008)","journal-title":"Formal Aspects of Computing"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Shao, D., Gopinath, D., Khurshid, S., Perry, D.: Optimizing Incremental Scope-Bounded Checking with Data-Flow Analysis. In: ISSRE 2010, pp. 408\u2013417 (2010)","DOI":"10.1109\/ISSRE.2010.27"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"757","DOI":"10.1007\/978-3-642-05089-3_48","volume-title":"FM 2009: Formal Methods","author":"D. Shao","year":"2009","unstructured":"Shao, D., Khurshid, S., Perry, D.: An Incremental Approach to Scope-Bounded Checking Using a Lightweight Formal Method. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 757\u2013772. Springer, Heidelberg (2009)"},{"key":"5_CR22","unstructured":"Sperberg-McQueen, C.M.: Alloy version of XPath 1.0 data model, http:\/\/www.blackmesatech.com\/2010\/01\/xpath10.als"},{"key":"5_CR23","unstructured":"World Wide Web Consortium (W3C), XML Path Language (XPath) Version 1.0, W3C Recommendation (November 16, 1999)"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/11813040_23","volume-title":"FM 2006: Formal Methods","author":"P. Zave","year":"2006","unstructured":"Zave, P.: Compositional binding in network domains. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 332\u2013347. Springer, Heidelberg (2006)"},{"key":"5_CR25","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1006\/jsco.1996.0030","volume":"21","author":"H. Zhang","year":"1996","unstructured":"Zhang, H., Bonacina, M.P., Hsiang, J.: PSATO: a distributed propositional prover and its application to quasigroup problems. J. Symb. Comput.\u00a021, 4\u20136 (1996)","journal-title":"J. Symb. Comput."},{"key":"5_CR26","unstructured":"http:\/\/cecar.fcen.uba.ar\/"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54108-7_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,14]],"date-time":"2020-08-14T01:23:33Z","timestamp":1597368213000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54108-7_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642541070","9783642541087"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54108-7_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}