{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:16:41Z","timestamp":1763468201064},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662436516"},{"type":"electronic","value":"9783662436523"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-43652-3_32","type":"book-chapter","created":{"date-parts":[[2014,5,29]],"date-time":"2014-05-29T02:22:12Z","timestamp":1401330132000},"page":"318-323","source":"Crossref","is-referenced-by-count":9,"title":["Staged Evaluation of Partial Instances in a Relational Model Finder"],"prefix":"10.1007","author":[{"given":"Vajih","family":"Montaghami","sequence":"first","affiliation":[]},{"given":"Derek","family":"Rayside","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Abad, P., Aguirre, N., Bengolea, V., Ciolek, D., Frias, M.F., Galeotti, J.P., Maibaum, T., Moscato, M., Rosner, N., Vissani, I.: Improving Test Generation under Rich Contracts by Tight Bounds and Incremental SAT Solving. In: ICST 2013 (2013)","key":"32_CR1","DOI":"10.1109\/ICST.2013.46"},{"unstructured":"Biere, A.: Handbook of Satisfiability, vol. 185. Ios PressInc. (2009)","key":"32_CR2"},{"unstructured":"Cunha, A.: Bounded model checking of temporal formulas with Alloy. arXiv preprint arXiv:1207.2746 (2012)","key":"32_CR3"},{"key":"32_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","year":"2012","unstructured":"Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.): ABZ 2012. LNCS, vol.\u00a07316. Springer, Heidelberg (2012)"},{"doi-asserted-by":"crossref","unstructured":"Dietrich, D., Shaker, P., Atlee, J., Rayside, D., Gorzny, J.: Feature Interaction Analysis of the Feature-Oriented Requirements-Modelling Language Using Alloy. In: MoDeVVa Workshop at MODELS Conference (2012)","key":"32_CR5","DOI":"10.1145\/2427376.2427380"},{"doi-asserted-by":"crossref","unstructured":"Dietrich, D., Shaker, P., Gorzny, J., Atlee, J., Rayside, D.: Translating the Feature-Oriented Requirements Modelling Language to Alloy. Tech. Rep. CS-2012-12, University of Waterloo, David R. Cheriton School of Computer Science (2012)","key":"32_CR6","DOI":"10.1145\/2427376.2427380"},{"key":"32_CR7","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)"},{"unstructured":"Fraikin, B., Frappier, M., St-Denis, R.: Modeling the supervisory control theory with Alloy. In: Derrick, et al. (eds.) [4]","key":"32_CR8"},{"doi-asserted-by":"crossref","unstructured":"Galeotti, J.P., Rosner, N., L\u00f3pez Pombo, C.G., Frias, M.F.: Analysis of Invariants for Efficient Bounded Verification. In: Tonella, P., Orso, A. (eds.) Proc. 19th ISSTA, pp. 25\u201336. ACM (2010)","key":"32_CR9","DOI":"10.1145\/1831708.1831712"},{"key":"32_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/978-3-642-34281-3_29","volume-title":"Formal Methods and Software Engineering","author":"S. Ganov","year":"2012","unstructured":"Ganov, S., Khurshid, S., Perry, D.E.: Annotations for Alloy: Automated Incremental Analysis Using Domain Specific Solvers. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol.\u00a07635, pp. 414\u2013429. Springer, Heidelberg (2012)"},{"unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press (2011)","key":"32_CR11"},{"issue":"4","key":"32_CR12","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1023\/B:AUSE.0000038938.10589.b9","volume":"11","author":"S. Khurshid","year":"2004","unstructured":"Khurshid, S., Marinov, D.: TestEra: Specification-based testing of Java programs using SAT. Automated Software Engineering\u00a011(4), 403\u2013434 (2004)","journal-title":"Automated Software Engineering"},{"key":"32_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-540-24605-3_21","volume-title":"Theory and Applications of Satisfiability Testing","author":"S. Khurshid","year":"2004","unstructured":"Khurshid, S., Marinov, D., Shlyakhter, I., Jackson, D.: A Case for Efficient Solution Enumeration. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 272\u2013286. Springer, Heidelberg (2004)"},{"unstructured":"Montaghami, V., Rayside, D.: Extending Alloy with partial instances. In: Derrick, et al. (eds.) [4]","key":"32_CR14"},{"unstructured":"Nelson, T., Barratt, C., Dougherty, D., Fisler, K., Krishnamurthi, S.: The Margrave tool for firewall analysis. In: Proceedings of the 24th International Conference on Large Installation System Administration, pp. 1\u20138. USENIX Association (2010)","key":"32_CR15"},{"unstructured":"Nelson, T., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Toward a more complete Alloy. In: Derrick, et al. (eds.) [4]","key":"32_CR16"},{"doi-asserted-by":"crossref","unstructured":"Toda, S.: On the computational power of PP and (+)P. In: 30th Annual Symposium on Foundations of Computer Science, pp. 514\u2013519 (October 1989)","key":"32_CR17","DOI":"10.1109\/SFCS.1989.63527"},{"key":"32_CR18","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.\u00a04424, pp. 632\u2013647. Springer, Heidelberg (2007)"},{"unstructured":"Vakili, A., Day, N.A.: Temporal logic model checking in Alloy. In: Derrick, et al. (eds.) [4]","key":"32_CR19"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B, TLA, VDM, and Z"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-43652-3_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T23:09:57Z","timestamp":1558912197000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-43652-3_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662436516","9783662436523"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-43652-3_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}