{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T03:14:27Z","timestamp":1776482067548,"version":"3.51.2"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319661964","type":"print"},{"value":"9783319661971","type":"electronic"}],"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-66197-1_11","type":"book-chapter","created":{"date-parts":[[2017,8,11]],"date-time":"2017-08-11T21:02:30Z","timestamp":1502485350000},"page":"168-184","source":"Crossref","is-referenced-by-count":22,"title":["User Studies of Principled Model Finder Output"],"prefix":"10.1007","author":[{"given":"Natasha","family":"Danas","sequence":"first","affiliation":[]},{"given":"Tim","family":"Nelson","sequence":"additional","affiliation":[]},{"given":"Lane","family":"Harrison","sequence":"additional","affiliation":[]},{"given":"Shriram","family":"Krishnamurthi","sequence":"additional","affiliation":[]},{"given":"Daniel J.","family":"Dougherty","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,13]]},"reference":[{"issue":"2","key":"11_CR1","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1006\/jsco.1997.0175","volume":"25","author":"S Aitken","year":"1998","unstructured":"Aitken, S., Gray, P., Melham, T., Thomas, M.: Interactive theorem proving: an empirical study of user activity. J. Symb. Comput. 25(2), 263\u2013284 (1998)","journal-title":"J. Symb. Comput."},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Akhawe, D., Barth, A., Lam, P., Mitchell, J., Song, D.: Towards a formal foundation of web security. In: IEEE Computer Security Foundations Symposium (2010)","DOI":"10.1109\/CSF.2010.27"},{"key":"11_CR3","doi-asserted-by":"publisher","first-page":"4","DOI":"10.4204\/EPTCS.167.3","volume":"167","author":"Bernhard Beckert","year":"2014","unstructured":"Beckert, B., Grebing, S., B\u00f6hl, F.: How to put usability into focus: using focus groups to evaluate the usability of interactive theorem provers. In: Workshop on User Interfaces for Theorem Provers (UITP) (2014)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Beckert, B., Grebing, S., B\u00f6hl, F.: A usability evaluation of interactive theorem provers using focus groups. In: Workshop on Human Oriented Formal Methods (HOFM) (2014)","DOI":"10.1007\/978-3-319-15201-1_1"},{"issue":"1","key":"11_CR5","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1023\/A:1006291616338","volume":"25","author":"F Bry","year":"2000","unstructured":"Bry, F., Yahya, A.: Positive unit hyperresolution tableaux and their application to minimal model generation. J. Autom. Reason. 25(1), 35\u201382 (2000)","journal-title":"J. Autom. Reason."},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-642-54804-8_2","volume-title":"Fundamental Approaches to Software Engineering","author":"A Cunha","year":"2014","unstructured":"Cunha, A., Macedo, N., Guimar\u00e3es, T.: Target oriented relational model finding. In: Gnesi, S., Rensink, A. (eds.) FASE 2014. LNCS, vol. 8411, pp. 17\u201331. Springer, Heidelberg (2014). doi: 10.1007\/978-3-642-54804-8_2"},{"issue":"2","key":"11_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2723163","volume":"22","author":"Loris D'antoni","year":"2015","unstructured":"D\u2019Antoni, L., Kini, D., Alur, R., Gulwani, S., Viswanathan, M., Hartmann, B.: How can automatic feedback help students construct automata? Trans. Comput. Hum. Interact. 22(2), March 2015","journal-title":"ACM Transactions on Computer-Human Interaction"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"DeOrio, A., Bertacco, V.: Human computing for EDA. In: Proceedings of the 46th Annual Design Automation Conference, pp. 621\u2013622 (2009)","DOI":"10.1145\/1629911.1630073"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1007\/978-3-540-71209-1_41","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"SF Doghmi","year":"2007","unstructured":"Doghmi, S.F., Guttman, J.D., Thayer, F.J.: Searching for shapes in cryptographic protocols. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 523\u2013537. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-71209-1_41"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Fagin, R., Ullman, J.D., Vardi, M.Y.: On the semantics of updates in databases. In: Principles of Database Systems (PODS), pp. 352\u2013365. ACM (1983)","DOI":"10.1145\/588058.588100"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/11814948_25","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"Z Fu","year":"2006","unstructured":"Fu, Z., Malik, S.: On solving the partial MAX-SAT problem. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 252\u2013265. Springer, Heidelberg (2006). doi: 10.1007\/11814948_25"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Ghoniem, M., Fekete, J.D., Castagliola, P.: A comparison of the readability of graphs using node-link and matrix-based representations. In: Information Visualization (INFOVIS) (2004)","DOI":"10.1109\/INFVIS.2004.1"},{"key":"11_CR13","doi-asserted-by":"publisher","first-page":"19:1","DOI":"10.1145\/2928269","volume":"23","author":"S Gould","year":"2016","unstructured":"Gould, S., Cox, A.L., Brumby, D.P.: Diminished control in crowdsourcing: an investigation of crowdworker multitasking behavior. Trans. Comput. Hum. Interact. 23, 19:1\u201319:29 (2016)","journal-title":"Trans. Comput. Hum. Interact."},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Hentschel, M., H\u00e4hnle, R., Bubel, R.: An empirical evaluation of two user interfaces of an interactive program verifier. In: International Conference on Automated Software Engineering (2016)","DOI":"10.1145\/2970276.2970303"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Herman, G.L., Kaczmarczyk, L.C., Loui, M.C., Zilles, C.B.: Proof by incomplete enumeration and other logical misconceptions. In: International Computing Education Research Workshop, ICER, pp. 59\u201370 (2008)","DOI":"10.1145\/1404520.1404527"},{"key":"11_CR16","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D Jackson","year":"2012","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2012)"},{"key":"11_CR17","unstructured":"Janota, M.: SAT solving in interactive configuration. Ph.D. thesis, University College Dublin (2010)"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Kittur, A., Chi, E.H., Suh, B.: Crowdsourcing user studies with Mechanical Turk. In: Conference on Human Factors in Computing Systems (CHI) (2008)","DOI":"10.1145\/1357054.1357127"},{"key":"11_CR19","unstructured":"Koshimura, M., Nabeshima, H., Fujita, H., Hasegawa, R.: Minimal model generation with respect to an atom set. In: First-Order Theorem Proving (FTP), p. 49 (2009)"},{"key":"11_CR20","first-page":"314","volume-title":"Lecture Notes in Computer Science","author":"Ferney A. Maldonado-Lopez","year":"2014","unstructured":"Maldonado-Lopez, F.A., Chavarriaga, J., Donoso, Y.: Detecting network policy conflicts using Alloy. In: International Conference on Abstract State Machines, Alloy, B, and Z (2014)"},{"key":"11_CR21","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":"Shahar Maoz","year":"2011","unstructured":"Maoz, S., Ringert, J.O., Rumpe, B.: CD2Alloy: class diagrams analysis using Alloy revisited. In: Model Driven Engineering Languages and Systems (2011)"},{"key":"11_CR22","first-page":"230","volume-title":"Lecture Notes in Computer Science","author":"Shahar Maoz","year":"2011","unstructured":"Maoz, S., Ringert, J.O., Rumpe, B.: CDDiff: semantic differencing for class diagrams. In: European Conference on Object Oriented Programming (2011)"},{"issue":"1","key":"11_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.3758\/s13428-011-0124-6","volume":"44","author":"W Mason","year":"2012","unstructured":"Mason, W., Suri, S.: Conducting behavioral research on Amazon\u2019s Mechanical Turk. Behav. Res. Methods 44(1), 1\u201323 (2012)","journal-title":"Behav. Res. Methods"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"McCune, W.: Mace4 reference manual and guide. arXiv preprint cs\/0310055 (2003)","DOI":"10.2172\/822574"},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"Munzner, T.: Visualization Analysis and Design. CRC Press (2014)","DOI":"10.1201\/b17511"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Nelson, T., Danas, N., Dougherty, D.J., Krishnamurthi, S.: The power of \u201cwhy\u201d and \u201cwhy not\u201d: enriching scenario exploration with provenance. In: Foundations of Software Engineering (2017)","DOI":"10.1145\/3106237.3106272"},{"key":"11_CR27","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":"11_CR28","unstructured":"Nelson, T., Barratt, C., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: The Margrave tool for firewall analysis. In: Large Installation System Administration Conference (2010)"},{"key":"11_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/3-540-61208-4_18","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"I Niemel\u00e4","year":"1996","unstructured":"Niemel\u00e4, I.: A tableau calculus for minimal model reasoning. In: Miglioli, P., Moscato, U., Mundici, D., Ornaghi, M. (eds.) TABLEAUX 1996. LNCS, vol. 1071, pp. 278\u2013294. Springer, Heidelberg (1996). doi: 10.1007\/3-540-61208-4_18"},{"issue":"1","key":"11_CR30","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1109\/TVCG.2015.2467758","volume":"22","author":"A Ottley","year":"2016","unstructured":"Ottley, A., Peck, E.M., Harrison, L.T., Afergan, D., Ziemkiewicz, C., Taylor, H.A., Han, P.K., Chang, R.: Improving Bayesian reasoning: the effects of phrasing, visualization, and spatial ability. Vis. Comput. Graph. 22(1), 529\u2013538 (2016)","journal-title":"Vis. Comput. Graph."},{"issue":"4","key":"11_CR31","doi-asserted-by":"publisher","first-page":"1023","DOI":"10.3758\/s13428-013-0434-y","volume":"46","author":"E Peer","year":"2014","unstructured":"Peer, E., Vosgerau, J., Acquisti, A.: Reputation as a sufficient condition for data quality on Amazon Mechanical Turk. Behav. Res. Methods 46(4), 1023\u20131031 (2014)","journal-title":"Behav. Res. Methods"},{"key":"11_CR32","volume-title":"Handbook of Automated Reasoning","author":"A Robinson","year":"2001","unstructured":"Robinson, A., Voronkov, A.: Handbook of Automated Reasoning, vol. 1. Elsevier, Amsterdam (2001)"},{"issue":"4","key":"11_CR33","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1145\/2534169.2491711","volume":"43","author":"N Ruchansky","year":"2013","unstructured":"Ruchansky, N., Proserpio, D.: A (not) NICE way to verify the OpenFlow switch specification: formal modelling of the OpenFlow switch using Alloy. ACM Comput. Commun. Rev. 43(4), 527\u2013528 (2013)","journal-title":"ACM Comput. Commun. Rev."},{"key":"11_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"434","DOI":"10.1007\/978-3-319-21401-6_30","volume-title":"Automated Deduction - CADE-25","author":"S Saghafi","year":"2015","unstructured":"Saghafi, S., Danas, R., Dougherty, D.J.: Exploring theories with a model-finding assistant. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 434\u2013449. Springer, Cham (2015). doi: 10.1007\/978-3-319-21401-6_30"},{"issue":"1\u20133","key":"11_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1080\/135062800394658","volume":"7","author":"DJ Simons","year":"2000","unstructured":"Simons, D.J.: Current approaches to change blindness. Vis. Cogn. 7(1\u20133), 1\u201315 (2000)","journal-title":"Vis. Cogn."},{"key":"11_CR36","doi-asserted-by":"crossref","unstructured":"Torlak, E., Chang, F.S.H., Jackson, D.: Finding minimal unsatisfiable cores of declarative specifications. In: International Symposium on Formal Methods (FM) (2008)","DOI":"10.1007\/978-3-540-68237-0_23"},{"key":"11_CR37","unstructured":"Wills, G.J.: Visual exploration of large structured datasets. In: Proceedings of New Techniques and Trends in Statistics (NTTS), pp. 237\u2013246 (1997)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66197-1_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T06:03:08Z","timestamp":1569996188000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66197-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661964","9783319661971"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66197-1_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}