{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T21:24:04Z","timestamp":1742937844669,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319681665"},{"type":"electronic","value":"9783319681672"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-68167-2_23","type":"book-chapter","created":{"date-parts":[[2017,9,25]],"date-time":"2017-09-25T23:50:53Z","timestamp":1506383453000},"page":"344-362","source":"Crossref","is-referenced-by-count":5,"title":["Exploiting Partial Knowledge for Efficient Model Analysis"],"prefix":"10.1007","author":[{"given":"Nuno","family":"Macedo","sequence":"first","affiliation":[]},{"given":"Alcino","family":"Cunha","sequence":"additional","affiliation":[]},{"given":"Eduardo","family":"Pessoa","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,9,27]]},"reference":[{"key":"23_CR1","unstructured":"Abrial, J.: The B-book - Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)"},{"key":"23_CR2","unstructured":"Audemard, G., Simon, L.: Glucose, version 4.0, October 2014. \nhttp:\/\/alloy.mit.edu\/kodkod\/download.html"},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-319-09284-3_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"G Audemard","year":"2014","unstructured":"Audemard, G., Simon, L.: Lazy clause exchange policy for parallel SAT solvers. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 197\u2013205. Springer, Cham (2014). doi:\n10.1007\/978-3-319-09284-3_15"},{"key":"23_CR4","unstructured":"Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT race 2010. Technical report 10\/1, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University (2010)"},{"key":"23_CR5","unstructured":"Biere, A.: Plingeling, version ayv-86bf266-140429, April 2014. \nhttp:\/\/fmv.jku.at\/lingeling\/"},{"key":"23_CR6","unstructured":"Crawford, J.M., Ginsberg, M.L., Luks, E.M., Roy, A.: Symmetry-breaking predicates for search problems. In: KR 1996, pp. 148\u2013159. Morgan Kaufmann (1996)"},{"key":"23_CR7","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: MiniSat, version 2.2.0, July 2010. \nhttp:\/\/minisat.se\/MiniSat.html"},{"key":"23_CR8","unstructured":"H\u00f6lldobler, S., Manthey, N., Nguyen, V.H., Stecklina, J., Steinke, P.: A short overview on modern parallel SAT-solvers. In: AICACSIS 2011, pp. 201\u2013206. IEEE (2011)"},{"key":"23_CR9","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis, revised edition. MIT Press, Cambridge (2012)"},{"key":"23_CR10","unstructured":"Lamport, L.: Specifying Systems, The TLA\n            $$^+$$\n           Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)"},{"key":"23_CR11","unstructured":"Macedo, N.: Pardinus, version 0.3, September 2016. \nhttps:\/\/github.com\/nmacedo\/Pardinus\/"},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"Macedo, N., Brunel, J., Chemouil, D., Cunha, A., Kuperberg, D.: Lightweight specification and analysis of dynamic systems with rich configurations. In: FSE 2016. ACM (2016)","DOI":"10.1145\/2950290.2950318"},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-3-662-46675-9_20","volume-title":"Fundamental Approaches to Software Engineering","author":"N Macedo","year":"2015","unstructured":"Macedo, N., Cunha, A., Guimar\u00e3es, T.: Exploring scenario exploration. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 301\u2013315. Springer, Heidelberg (2015). doi:\n10.1007\/978-3-662-46675-9_20"},{"issue":"3","key":"23_CR14","doi-asserted-by":"crossref","first-page":"304","DOI":"10.1007\/s10601-012-9121-3","volume":"17","author":"R Martins","year":"2012","unstructured":"Martins, R., Manquinho, V.M., Lynce, I.: An overview of parallel SAT solving. Constraints 17(3), 304\u2013347 (2012)","journal-title":"Constraints"},{"key":"23_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-30885-7_9","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"V Montaghami","year":"2012","unstructured":"Montaghami, V., Rayside, D.: Extending alloy with partial instances. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 122\u2013135. Springer, Heidelberg (2012). doi:\n10.1007\/978-3-642-30885-7_9"},{"issue":"4","key":"23_CR16","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1145\/2699417","volume":"58","author":"C Newcombe","year":"2015","unstructured":"Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How Amazon web services uses formal methods. Commun. ACM 58(4), 66\u201373 (2015)","journal-title":"Commun. ACM"},{"key":"23_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-54108-7_5","volume-title":"Verified Software: Theories, Tools, Experiments","author":"N Rosner","year":"2014","unstructured":"Rosner, N., L\u00f3pez Pombo, C.G., Aguirre, N., Jaoua, A., Mili, A., Frias, M.F.: Parallel bounded verification of alloy models by transcoping. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 88\u2013107. Springer, Heidelberg (2014). doi:\n10.1007\/978-3-642-54108-7_5"},{"key":"23_CR18","doi-asserted-by":"crossref","unstructured":"Rosner, N., Siddiqui, J.H., Aguirre, N., Khurshid, S., Frias, M.F.: Ranger: parallel analysis of alloy models by range partitioning. In: ASE 2013, pp. 147\u2013157. IEEE (2013)","DOI":"10.1109\/ASE.2013.6693075"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-540-68111-3_27","volume-title":"Parallel Processing and Applied Mathematics","author":"D Singer","year":"2008","unstructured":"Singer, D., Monnet, A.: JaCk-SAT: a new parallel scheme to solve the satisfiability problem (SAT) based on join-and-check. In: Wyrzykowski, R., Dongarra, J., Karczewski, K., Wasniewski, J. (eds.) PPAM 2007. LNCS, vol. 4967, pp. 249\u2013258. Springer, Heidelberg (2008). doi:\n10.1007\/978-3-540-68111-3_27"},{"key":"23_CR20","unstructured":"Torlak, E.: Kodkod, version 2.1, September 2015. \nhttp:\/\/alloy.mit.edu\/kodkod\/download.html"},{"key":"23_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632\u2013647. Springer, Heidelberg (2007). doi:\n10.1007\/978-3-540-71209-1_49"},{"key":"23_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-540-68237-0_22","volume-title":"FM 2008: Formal Methods","author":"E Uzuncaova","year":"2008","unstructured":"Uzuncaova, E., Khurshid, S.: Constraint prioritization for efficient analysis of declarative models. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 310\u2013325. Springer, Heidelberg (2008). doi:\n10.1007\/978-3-540-68237-0_22"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-68167-2_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,10,3]],"date-time":"2017-10-03T03:53:55Z","timestamp":1507002835000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68167-2_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319681665","9783319681672"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68167-2_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}