{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T16:52:33Z","timestamp":1742921553292,"version":"3.40.3"},"publisher-location":"Cham","reference-count":52,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030324087"},{"type":"electronic","value":"9783030324094"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-32409-4_21","type":"book-chapter","created":{"date-parts":[[2019,10,28]],"date-time":"2019-10-28T00:03:00Z","timestamp":1572220980000},"page":"336-352","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Solution Enumeration Abstraction: A Modeling Idiom to Enhance a Lightweight Formal Method"],"prefix":"10.1007","author":[{"given":"Allison","family":"Sullivan","sequence":"first","affiliation":[]},{"given":"Darko","family":"Marinov","sequence":"additional","affiliation":[]},{"given":"Sarfraz","family":"Khurshid","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,10,28]]},"reference":[{"key":"21_CR1","unstructured":"Alloy analyzer Website (2019). http:\/\/alloytools.org"},{"key":"21_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809163","volume-title":"Introduction to Software Testing","author":"P Ammann","year":"2008","unstructured":"Ammann, P., Offutt, J.: Introduction to Software Testing. Cambridge University Press, Cambridge (2008)"},{"key":"21_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-017-0445-z","volume-title":"Formal Aspects of Computing","author":"H Bagheri","year":"2018","unstructured":"Bagheri, H., Kang, E., Malek, S., Jackson, D.: A Formal Approach for Detection of Security Flaws in the Android Permission System. Formal Aspects of Computing. Springer, London (2018). https:\/\/doi.org\/10.1007\/s00165-017-0445-z"},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: Automated testing based on Java predicates. In: ISSTA (2002)","DOI":"10.1145\/566172.566191"},{"key":"21_CR5","unstructured":"CheckMate GitHub (2019). https:\/\/github.com\/ctrippel\/checkmate"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Chong, N., Sorensen, T., Wickerson, J.: The semantics of transactions and weak memory in x86, Power, ARM, and C++. In: PLDI (2018)","DOI":"10.1145\/3192366.3192373"},{"key":"21_CR7","volume-title":"Introduction to Algorithms","author":"TH Cormen","year":"2009","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. The MIT Press, Cambridge (2009)","edition":"3"},{"key":"21_CR8","unstructured":"Crawford, J.: A theoretical analysis of reasoning by symmetry in first-order logic (extended abstract). In: AAAI 1992 Workshop on Tractable Reasoning (1992)"},{"key":"21_CR9","unstructured":"CryptoMiniSat Solver Website (2019). https:\/\/www.msoos.org\/cryptominisat5\/"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Dutra, R., Bachrach, J., Sen, K.: SMTSampler: efficient stimulus generation from complex SMT constraints. In: ICCAD (2018)","DOI":"10.1145\/3240765.3240848"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"Een, N., Sorensson, N.: An extensible SAT-solver. In: SAT (2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Filieri, A., Pasareanu, C.S., Visser, W.: Reliability analysis in Symbolic PathFinder. In: ICSE (2013)","DOI":"10.1109\/ICSE.2013.6606608"},{"issue":"9","key":"21_CR13","first-page":"1283","volume":"39","author":"JP Galeotti","year":"2013","unstructured":"Galeotti, J.P., Rosner, N., Pombo, C.G.L., Frias, M.F.: TACO: efficient SAT-based bounded verification using symmetry breaking and tight bounds. TSE 39(9), 1283\u20131307 (2013)","journal-title":"TSE"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Ghiya, R., Hendren, L.J.: Is it a tree, a DAG, or a cyclic graph? a shape analysis for heap-directed pointers in C. In: POPL (1996)","DOI":"10.1145\/237721.237724"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Gligoric, M., Gvero, T., Jagannath, V., Khurshid, S., Kuncak, V., Marinov, D.: Test generation through programming in UDITA. In: ICSE (2010)","DOI":"10.1145\/1806799.1806835"},{"key":"21_CR16","unstructured":"Glucose Solver Website (2019). https:\/\/www.labri.fr\/perso\/lsimon\/glucose\/"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"Gopinath, D., Malik, M.Z., Khurshid, S.: Specification-based program repair using SAT. In: TACAS (2011)","DOI":"10.1007\/978-3-642-19835-9_15"},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Guttag, J.V., Horning, J.J.: Larch: Languages and Tools for Formal Specification (1993)","DOI":"10.1007\/978-1-4612-2704-5"},{"key":"21_CR19","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge (2006)"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Jackson, D., Sullivan, K.J.: COM revisited: Tool-assisted modelling of an architectural framework. In: SIGSOFT FSE (2000)","DOI":"10.1145\/355045.355065"},{"key":"21_CR21","doi-asserted-by":"crossref","unstructured":"Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: ISSTA (2000)","DOI":"10.1145\/347324.383378"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"Khurshid, S., Jackson, D.: Exploring the design of an intentional naming scheme with an automatic constraint analyzer. In: ASE (2000)","DOI":"10.1109\/ASE.2000.873646"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Khurshid, S., Marinov, D., Shlyakhter, I., Jackson, D.: A case for efficient solution enumeration. In: SAT (2003)","DOI":"10.1007\/978-3-540-24605-3_21"},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"Kuraj, I., Kuncak, V., Jackson, D.: Programming with enumerable sets of structures. In: OOPSLA (2015)","DOI":"10.1145\/2814270.2814323"},{"issue":"3","key":"21_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"GT Leavens","year":"2006","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. Softw. Eng. Notes 31(3), 1\u201338 (2006)","journal-title":"Softw. Eng. Notes"},{"key":"21_CR26","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., M\u00fcller, P.: A verification methodology for model fields. In: ESOP (2006)","DOI":"10.1007\/11693024_9"},{"key":"21_CR27","unstructured":"Lingeling, Plingeling, and Treengeling Website (2019). http:\/\/fmv.jku.at\/lingeling\/"},{"key":"21_CR28","unstructured":"Liskov, B., Guttag, J.: Program development in Java: Abstraction, Specification, and Object-Oriented Design (2000)"},{"key":"21_CR29","doi-asserted-by":"crossref","unstructured":"Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate abstraction and canonical abstraction for singly-linked lists. In: VMCAI, pp. 181\u2013198 (2005)","DOI":"10.1007\/978-3-540-30579-8_13"},{"key":"21_CR30","unstructured":"Marinov, D., Khurshid, S.: TestEra: a novel framework for automated testing of Java programs. In: ASE (2001)"},{"key":"21_CR31","unstructured":"Meel, K.S., et al.: Constrained sampling and counting: universal hashing meets SAT solving. In: Beyond NP, AAAI Workshop (2016)"},{"key":"21_CR32","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bjorner, N.: Z3: an efficient SMT solver. In: TACAS (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"21_CR33","doi-asserted-by":"crossref","unstructured":"Nelson, T., Saghafi, S., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Aluminum: principled scenario exploration through minimality. In: ICSE, pp. 232\u2013241 (2013)","DOI":"10.1109\/ICSE.2013.6606569"},{"key":"21_CR34","doi-asserted-by":"crossref","unstructured":"Pacheco, C., Ernst, M.D.: Randoop: feedback-directed random testing for Java. In: OOPSLA Companion, pp. 815\u2013816 (2007)","DOI":"10.1145\/1297846.1297902"},{"key":"21_CR35","doi-asserted-by":"crossref","unstructured":"Ponzio, P., Aguirre, N., Frias, M.F., Visser, W.: Field-exhaustive testing. In: SIGSOFT FSE (2016)","DOI":"10.1145\/2950290.2950336"},{"key":"21_CR36","doi-asserted-by":"crossref","unstructured":"Porncharoenwase, S., Nelson, T., Krishnamurthi, S.: CompoSAT: specification-guided coverage for model finding. In: FM (2018)","DOI":"10.1007\/978-3-319-95582-7_34"},{"key":"21_CR37","doi-asserted-by":"crossref","unstructured":"P\u0103s\u0103reanu, C.S., Pel\u00e1nek, R., Visser, W.: Concrete model checking with abstract matching and refinement. In: CAV (2005)","DOI":"10.1007\/11513988_7"},{"key":"21_CR38","doi-asserted-by":"crossref","unstructured":"Rayside, D., Benjamin, Z., Singh, R., Near, J.P., Milicevic, A., Jackson, D.: Equality and hashing for (almost) free: generating implementations from abstraction functions. In: ICSE (2009)","DOI":"10.1109\/ICSE.2009.5070534"},{"key":"21_CR39","doi-asserted-by":"crossref","unstructured":"Rayside, D., Montaghami, V., Leung, F., Yuen, A., Xu, K., Jackson, D.: Synthesizing iterators from abstraction functions. In: GPCE (2012)","DOI":"10.1145\/2371401.2371407"},{"key":"21_CR40","doi-asserted-by":"crossref","unstructured":"Ringer, T., Grossman, D., Schwartz-Narbonne, D., Tasiran, S.: A solver-aided language for test input generation. In: PACMPL OOPSLA (2017)","DOI":"10.1145\/3133915"},{"key":"21_CR41","doi-asserted-by":"crossref","unstructured":"Samimi, H., Aung, E.D., Millstein, T.D.: Falling back on executable specifications. In: ECOOP (2010)","DOI":"10.1007\/978-3-642-14107-2_26"},{"key":"21_CR42","unstructured":"SAT4J Solver Website (2019). https:\/\/www.sat4j.org\/"},{"key":"21_CR43","doi-asserted-by":"crossref","unstructured":"Shlyakhter, I.: Generating effective symmetry-breaking predicates for search problems. In: SAT (2001)","DOI":"10.1016\/S1571-0653(04)00311-7"},{"key":"21_CR44","doi-asserted-by":"crossref","unstructured":"Sullivan, A., Wang, K., Zaeem, R.N., Khurshid, S.: Automated test generation and mutation testing for Alloy. In: ICST (2017)","DOI":"10.1109\/ICST.2017.31"},{"key":"21_CR45","unstructured":"Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: TACAS (2007)"},{"key":"21_CR46","doi-asserted-by":"crossref","unstructured":"Trippel, C., Lustig, D., Martonosi, M.: CheckMate: automated synthesis of hardware exploits and security litmus tests. In: MICRO (2018)","DOI":"10.1109\/MICRO.2018.00081"},{"key":"21_CR47","doi-asserted-by":"crossref","unstructured":"Trippel, C., Lustig, D., Martonosi, M.: Security verification via automatic hardware-aware exploit synthesis: The CheckMate approach. In: IEEE Micro (2019)","DOI":"10.1109\/MM.2019.2910010"},{"key":"21_CR48","doi-asserted-by":"crossref","unstructured":"Wickerson, J., Batty, M., Sorensen, T., Constantinides, G.A.: Automatically comparing memory consistency models. In: POPL (2017)","DOI":"10.1145\/3009837.3009838"},{"key":"21_CR49","doi-asserted-by":"crossref","unstructured":"Xie, T., Marinov, D., Notkin, D.: Rostra: a framework for detecting redundant object-oriented unit tests. In: ASE (2004)","DOI":"10.1007\/978-3-540-31980-1_24"},{"key":"21_CR50","unstructured":"Zaeem, R.N., Khurshid, S.: Contract-based data structure repair using Alloy. In: ECOOP (2010)"},{"issue":"12","key":"21_CR51","doi-asserted-by":"publisher","first-page":"1144","DOI":"10.1109\/TSE.2017.2655056","volume":"43","author":"P Zave","year":"2017","unstructured":"Zave, P.: Reasoning about identifier spaces: how to make chord correct. IEEE Trans. Softw. Eng. 43(12), 1144\u20131156 (2017)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"21_CR52","unstructured":"Zhang, J.: The generation and application of finite models. Ph.D. thesis, Institute of Software, Academia Sinica, Beijing (1994)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-32409-4_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,2]],"date-time":"2022-10-02T19:44:10Z","timestamp":1664739850000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-32409-4_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030324087","9783030324094"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-32409-4_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"28 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICFEM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Engineering Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Shenzhen","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 November 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 November 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icfem2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/csse.szu.edu.cn\/icfem2019\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"94","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}