{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T21:55:34Z","timestamp":1742939734396,"version":"3.40.3"},"publisher-location":"Cham","reference-count":73,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030916305"},{"type":"electronic","value":"9783030916312"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-91631-2_9","type":"book-chapter","created":{"date-parts":[[2021,11,18]],"date-time":"2021-11-18T21:02:24Z","timestamp":1637269344000},"page":"156-174","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Model Finding for Exploration"],"prefix":"10.1007","author":[{"given":"Daniel J.","family":"Dougherty","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,11,19]]},"reference":[{"issue":"1\u20132","key":"9_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0168-0072(91)90065-T","volume":"51","author":"S Abramsky","year":"1991","unstructured":"Abramsky, S.: Domain theory in logical form. Ann. Pure Appl. Logic 51(1\u20132), 1\u201377 (1991)","journal-title":"Ann. Pure Appl. Logic"},{"key":"9_CR2","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.SMT-LIB.org"},{"key":"9_CR3","unstructured":"Barto, L., DeMeo, W.J., Mottet, A.: The complexity of the homomorphism problem for boolean structures (2020). CoRR abs\/2010.04958, https:\/\/arxiv.org\/abs\/2010.04958"},{"issue":"1","key":"9_CR4","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1016\/j.jal.2007.07.005","volume":"7","author":"P Baumgartner","year":"2009","unstructured":"Baumgartner, P., Fuchs, A., Nivelle, H.D., Tinelli, C.: Computing finite models by reduction to function-free clause logic. J. Appl. Logic 7(1), 58\u201374 (2009)","journal-title":"J. Appl. Logic"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/11591191_18","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M Bezem","year":"2005","unstructured":"Bezem, M., Coquand, T.: Automating coherent logic. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 246\u2013260. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11591191_18"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2010","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131\u2013146. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_11"},{"key":"9_CR7","unstructured":"Bodirsky, M., Feller, T., Kn\u00e4uer, S., Rudolph, S.: On logics and homomorphism closure (2021). CoRR abs\/2104.11955, https:\/\/arxiv.org\/abs\/2104.11955"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/BFb0023733","volume-title":"Computer-Aided Verification","author":"A Bouajjani","year":"1991","unstructured":"Bouajjani, A., Fernandez, J.-C., Halbwachs, N.: Minimal model generation. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 197\u2013203. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/BFb0023733"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/3-540-61208-4_10","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"F Bry","year":"1996","unstructured":"Bry, F., Yahya, A.: Minimal model generation with positive unit hyper-resolution tableaux. In: Miglioli, P., Moscato, U., Mundici, D., Ornaghi, M. (eds.) TABLEAUX 1996. LNCS, vol. 1071, pp. 143\u2013159. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61208-4_10"},{"key":"9_CR10","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. Reas 25, 35\u201382 (2000)","journal-title":"J. Autom. Reas"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-35308-6_10","volume-title":"Certified Programs and Proofs","author":"L Bulwahn","year":"2012","unstructured":"Bulwahn, L.: The new quickcheck for isabelle. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 92\u2013108. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-35308-6_10"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Chamarthi, H.R., Dillinger, P.C., Kaufmann, M., Manolios, P.: Integrating testing and interactive theorem proving. In: Hardin, D., Schmaltz, J. (eds.) Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, 3\u20134 November 2011. EPTCS, vol. 70, pp. 4\u201319 (2011)","DOI":"10.4204\/EPTCS.70.0"},{"key":"9_CR13","unstructured":"Claessen, K., Sorensson, N.: New techniques that improve MACE-style finite model finding. In: Proceedings of the CADE-19 Workshop: Model Computation-Principles, Algorithms, Applications. Citeseer (2003)"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Claessen, K., Hughes, J.: QuickCheck. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming - ICFP \u201900. ACM Press (2000)","DOI":"10.1145\/351240.351266"},{"key":"9_CR15","unstructured":"Coquand, T.: A completeness proof for geometric logic. In: Logic, Methodology and Philosophy of Science. Proceedings of the Twelfth International Congress, pp. 79\u201390 (2010)"},{"issue":"3","key":"9_CR16","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/S0168-0072(01)00026-4","volume":"111","author":"M Coste","year":"2001","unstructured":"Coste, M., Lombardi, H., Roy, M.F.: Dynamical method in algebra: effective nullstellens\u00e4tze. Ann. Pure Appl. Logic 111(3), 203\u2013256 (2001)","journal-title":"Ann. Pure Appl. Logic"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-319-66197-1_11","volume-title":"Software Engineering and Formal Methods","author":"N Danas","year":"2017","unstructured":"Danas, N., Nelson, T., Harrison, L., Krishnamurthi, S., Dougherty, D.J.: User studies of principled model finder output. In: Cimatti, A., Sirjani, M. (eds.) SEFM 2017. LNCS, vol. 10469, pp. 168\u2013184. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66197-1_11"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/11814771_28","volume-title":"Automated Reasoning","author":"H de Nivelle","year":"2006","unstructured":"de Nivelle, H., Meng, J.: Geometric resolution: a proof procedure based on finite model search. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 303\u2013317. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814771_28"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Deutsch, A., Nash, A., Remmel, J.: The chase revisited. In: ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, pp. 149\u2013158 (2008)","DOI":"10.1145\/1376916.1376938"},{"key":"9_CR20","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). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_41"},{"key":"9_CR21","unstructured":"Dougherty, D.J., Guttman, J.D., Ramsdell, J.D.: Homomorphisms and Minimality for Enrich-by-Need Security Analysis. ArXiv e-prints (2018)"},{"key":"9_CR22","unstructured":"Dougherty, D.J., Guttman, J.: Geometric logic and strand spaces. In: 5th International Workshop on Security and Rewriting Techniques (2010)"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Dougherty, D.J., Guttman, J.D.: Decidability for lightweight Diffie-Hellman protocols. In: IEEE 27th Computer Security Foundations Symposium, CSF 2014, Vienna, Austria, 19\u201322 July 2014, pp. 217\u2013231 (2014)","DOI":"10.1109\/CSF.2014.23"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-319-98938-9_8","volume-title":"Integrated Formal Methods","author":"DJ Dougherty","year":"2018","unstructured":"Dougherty, D.J., Guttman, J.D., Ramsdell, J.D.: Security protocol analysis in context: computing minimal executions using SMT and CPSA. In: Furia, C.A., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 130\u2013150. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-98938-9_8"},{"key":"9_CR25","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1017\/bsl.2015.7","volume":"21","author":"R Dyckhoff","year":"2015","unstructured":"Dyckhoff, R., Negri, S.: Geometrisation of first-order logic. Bull. Symb. Logic 21, 123\u2013163 (2015)","journal-title":"Bull. Symb. Logic"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Eastlund, C.: Doublecheck your theorems. In: Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications, pp. 42\u201346 (2009)","DOI":"10.1145\/1637837.1637844"},{"key":"9_CR27","unstructured":"El Ghazi, A.A., Taghdiri, M.: Analyzing alloy constraints using an SMT solver: a case study. In: 5th International Workshop on Automated Formal Methods (AFM) (2010)"},{"issue":"4","key":"9_CR28","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1007\/s00493-015-3003-4","volume":"37","author":"PL Erd\u0151s","year":"2017","unstructured":"Erd\u0151s, P.L., P\u00e1lv\u00f6lgyi, D., Tardif, C., Tardos, G.: Regular families of forests, antichains and duality pairs of relational structures. Combinatorica 37(4), 651\u2013672 (2017). https:\/\/doi.org\/10.1007\/s00493-015-3003-4","journal-title":"Combinatorica"},{"issue":"1","key":"9_CR29","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1145\/1061318.1061323","volume":"30","author":"R Fagin","year":"2005","unstructured":"Fagin, R., Kolaitis, P.G., Popa, L.: Data exchange: getting to the core. ACM Trans. Database Syst. (TODS) 30(1), 174\u2013210 (2005)","journal-title":"ACM Trans. Database Syst. (TODS)"},{"issue":"1","key":"9_CR30","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.tcs.2004.10.033","volume":"336","author":"R Fagin","year":"2005","unstructured":"Fagin, R., Kolaitis, P.G., Miller, R.J., Popa, L.: Data exchange: semantics and query answering. Theor. Comput. Sci. 336(1), 89\u2013124 (2005)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"9_CR31","doi-asserted-by":"publisher","first-page":"79","DOI":"10.3233\/FI-2009-0034","volume":"91","author":"J Fisher","year":"2009","unstructured":"Fisher, J., Bezem, M.: Skolem machines. Fundamenta Informaticae 91(1), 79\u2013103 (2009)","journal-title":"Fundamenta Informaticae"},{"key":"9_CR32","unstructured":"Garey, M.R., Johnson, D.S.: Computers and intractability. w. h (1979)"},{"issue":"2","key":"9_CR33","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1023\/A:1005851801356","volume":"18","author":"T Geisler","year":"1997","unstructured":"Geisler, T., Panne, S., Sch\u00fctz, H.: Satchmo - the compiling and functional variants. J. Autom. Reas. 18(2), 227\u2013236 (1997)","journal-title":"J. Autom. Reas."},{"key":"9_CR34","doi-asserted-by":"crossref","unstructured":"Gottlob, G.: Computing cores for data exchange: new algorithms and practical solutions. In: ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, pp. 148\u2013159 (2005)","DOI":"10.1145\/1065167.1065187"},{"issue":"1","key":"9_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1206035.1206036","volume":"54","author":"M Grohe","year":"2007","unstructured":"Grohe, M.: The complexity of homomorphism and constraint satisfaction problems seen from the other side. J. ACM (JACM) 54(1), 1\u201324 (2007)","journal-title":"J. ACM (JACM)"},{"key":"9_CR36","doi-asserted-by":"publisher","unstructured":"Guttman, J.D.: Security theorems via model theory. EXPRESS Express. Conc. (EPTCS) 8, 51 (2009). https:\/\/doi.org\/10.4204\/EPTCS.8.5","DOI":"10.4204\/EPTCS.8.5"},{"key":"9_CR37","unstructured":"Guttman, J.D.: Shapes: surveying crypto protocol runs. In: Cortier, V., Kremer, S. (eds.) Formal Models and Techniques for Analyzing Security Protocols. IOS Press, Cryptology and Information Security Series (2011)"},{"issue":"2","key":"9_CR38","doi-asserted-by":"publisher","first-page":"203","DOI":"10.3233\/JCS-140499","volume":"22","author":"JD Guttman","year":"2014","unstructured":"Guttman, J.D.: Establishing and preserving protocol security goals. J. Comput. Secur. 22(2), 203\u2013267 (2014)","journal-title":"J. Comput. Secur."},{"issue":"2","key":"9_CR39","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/S0304-3975(01)00139-6","volume":"283","author":"JD Guttman","year":"2002","unstructured":"Guttman, J.D., Thayer, F.J.: Authentication tests and the structure of bundles. Theor. Comput. Sci. 283(2), 333\u2013380 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-69611-7_1","volume-title":"Practical Aspects of Declarative Languages","author":"J Hughes","year":"2006","unstructured":"Hughes, J.: QuickCheck testing for fun and profit. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 1\u201332. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/978-3-540-69611-7_1"},{"issue":"9","key":"9_CR41","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/3338843","volume":"62","author":"D Jackson","year":"2019","unstructured":"Jackson, D.: Alloy: a language and tool for exploring software designs. Commun. ACM 62(9), 66\u201376 (2019)","journal-title":"Commun. ACM"},{"key":"9_CR42","unstructured":"Koshimura, M., Nabeshima, H., Fujita, H., Hasegawa, R.: Minimal model generation with respect to an atom set. In: International Workshop on First-Order Theorem Proving (2009)"},{"key":"9_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-30942-8_1","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"S Krishnamurthi","year":"2019","unstructured":"Krishnamurthi, S., Nelson, T.: The human in formal methods. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 3\u201310. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_1"},{"key":"9_CR44","series-title":"Universitext","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0927-0","volume-title":"Sheaves in Geometry and Logic: A First Introduction to Topos Theory","author":"S Mac Lane","year":"1992","unstructured":"Mac Lane, S., Moerdijk, I.: Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Universitext, Springer, New York (1992). https:\/\/doi.org\/10.1007\/978-1-4612-0927-0"},{"issue":"4","key":"9_CR45","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1145\/320107.320115","volume":"4","author":"D Maier","year":"1979","unstructured":"Maier, D., Mendelzon, A.O., Sagiv, Y.: Testing implications of data dependencies. ACM Trans. Database Syst. (TODS) 4(4), 455\u2013469 (1979)","journal-title":"ACM Trans. Database Syst. (TODS)"},{"key":"9_CR46","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066201","volume-title":"First Order Categorical Logic","author":"M Makkai","year":"1977","unstructured":"Makkai, M., Reyes, G.E.: First Order Categorical Logic. LNM, vol. 611. Springer, Heidelberg (1977). https:\/\/doi.org\/10.1007\/BFb0066201"},{"key":"9_CR47","doi-asserted-by":"publisher","unstructured":"Maldonado-Lopez, F.A., Chavarriaga, J., Donoso, Y.: Detecting network policy conflicts using Alloy. In: Ameur, Y.A., Schewe, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference, ABZ 2014, Toulouse, France, 2\u20136 June 2014. Proceedings. Lecture Notes in Computer Science, vol. 8477, pp. 314\u2013317. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-43652-3_31","DOI":"10.1007\/978-3-662-43652-3_31"},{"key":"9_CR48","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. 6981, pp. 592\u2013607. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24485-8_44"},{"key":"9_CR49","unstructured":"Marinov, D., Khurshid, S.: Testera: a novel framework for automated testing of java programs. In: Proceedings 16th Annual International Conference on Automated Software Engineering (ASE 2001), pp. 22\u201331. IEEE (2001)"},{"issue":"6","key":"9_CR50","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2535926","volume":"60","author":"D Marx","year":"2013","unstructured":"Marx, D.: Tractable hypergraph properties for constraint satisfaction and conjunctive queries. J. ACM (JACM) 60(6), 1\u201351 (2013)","journal-title":"J. ACM (JACM)"},{"key":"9_CR51","doi-asserted-by":"crossref","unstructured":"McCune, W.: Mace4 reference manual and guide (2003). arXiv preprint cs\/0310055","DOI":"10.2172\/822574"},{"key":"9_CR52","doi-asserted-by":"crossref","unstructured":"Milicevic, A., Misailovic, S., Marinov, D., Khurshid, S.: Korat: a tool for generating structurally complex test inputs. In: 29th International Conference on Software Engineering (ICSE\u201907), pp. 771\u2013774. IEEE (2007)","DOI":"10.1109\/ICSE.2007.48"},{"key":"9_CR53","doi-asserted-by":"crossref","unstructured":"Nelson, T., Danas, N., Dougherty, D.J., Krishnamurthi, S.: The power of Why and Why Not: enriching scenario exploration with provenance. In: Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, ESEC\/FSE 2017, Paderborn, Germany, 4\u20138 September 2017, pp. 106\u2013116 (2017)","DOI":"10.1145\/3106237.3106272"},{"key":"9_CR54","doi-asserted-by":"crossref","unstructured":"Nelson, T., Saghafi, S., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Aluminum: Principled scenario exploration through minimality. In: 35th International Conference on Software Engineering (ICSE), pp. 232\u2013241 (2013)","DOI":"10.1109\/ICSE.2013.6606569"},{"key":"9_CR55","unstructured":"Nelson, T., Barratt, C., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: The Margrave tool for firewall analysis. In: Proceedings of the 24th USENIX Large Installation System Administration Conference (LISA 2010) (2010)"},{"key":"9_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-319-22102-1_22","volume-title":"Interactive Theorem Proving","author":"Z Paraskevopoulou","year":"2015","unstructured":"Paraskevopoulou, Z., Hri\u0163cu, C., D\u00e9n\u00e8s, M., Lampropoulos, L., Pierce, B.C.: Foundational property-based testing. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 325\u2013343. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22102-1_22"},{"key":"9_CR57","unstructured":"Pombrio, J.L.: Protocol analysis via the chase. Technical report, Worcester Polytechnic Institute (2011)"},{"key":"9_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1007\/978-3-319-95582-7_34","volume-title":"Formal Methods","author":"S Porncharoenwase","year":"2018","unstructured":"Porncharoenwase, S., Nelson, T., Krishnamurthi, S.: CompoSAT: specification-guided coverage for model finding. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 568\u2013587. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-95582-7_34"},{"key":"9_CR59","unstructured":"Ramsdell, J.: Personal communication (2021)"},{"key":"9_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"640","DOI":"10.1007\/978-3-642-39799-8_42","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2013","unstructured":"Reynolds, A., Tinelli, C., Goel, A., Krsti\u0107, S.: Finite model finding in SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 640\u2013655. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_42"},{"issue":"3","key":"9_CR61","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1145\/1379759.1379763","volume":"55","author":"B Rossman","year":"2008","unstructured":"Rossman, B.: Homomorphism preservation theorems. J. ACM (JACM) 55(3), 15 (2008)","journal-title":"J. ACM (JACM)"},{"key":"9_CR62","unstructured":"Rowe, P.D., Ramsdell, J.D., Kretz, I.D.: Automated trust analysis for layered attestations. Submitted for publication (2021)"},{"key":"9_CR63","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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 (LNAI), vol. 9195, pp. 434\u2013449. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_30"},{"key":"9_CR64","unstructured":"Saghafi, S., Dougherty, D.J.: Razor: provenance and exploration in model-finding. In: 4th Workshop on Practical Aspects of Automated Reasoning (PAAR) (2014)"},{"key":"9_CR65","unstructured":"Saghafi, S., Nelson, T., Dougherty, D.J.: Geometric logic for policy analysis. In: International Workshop on Automated Reasoning in Security and Software Verification (ARSEC 2013), pp. 12\u201320 (2013)"},{"key":"9_CR66","doi-asserted-by":"crossref","unstructured":"Shao, D., Khurshid, S., Perry, D.E.: Whispec: white-box testing of libraries using declarative specifications. In: Proceedings of the 2007 Symposium on Library-Centric Software Design, pp. 11\u201320 (2007)","DOI":"10.1145\/1512762.1512764"},{"key":"9_CR67","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. J. Autom. Reas. 59(4), 483\u2013502 (2017)","DOI":"10.1007\/s10817-017-9407-7"},{"key":"9_CR68","unstructured":"Thorstensen, E.: Instance-Based Hyper-Tableaux for Coherent Logic. Master\u2019s thesis, University of Oslo (2009)"},{"key":"9_CR69","unstructured":"Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Conference on Tools and Algorithms for the Construction and Analysis of Systems (2007)"},{"key":"9_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1007\/978-3-319-48989-6_41","volume-title":"FM 2016: Formal Methods","author":"A Vakili","year":"2016","unstructured":"Vakili, A., Day, N.A.: Finite model finding using the logic of equality with uninterpreted functions. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 677\u2013693. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_41"},{"key":"9_CR71","doi-asserted-by":"publisher","unstructured":"Vickers, S.: Geometric logic in computer science. In: Burn, G.L., Gay, S.J., Ryan, M. (eds.) Theory and Formal Methods 1993, Proceedings of the First Imperial College Department of Computing Workshop on Theory and Formal Methods, Isle of Thorns Conference Centre, Chelwood Gate, Sussex, UK, 29\u201331 March 1993, pp. 37\u201354. Workshops in Computing, Springer, Heideleberg (1993). https:\/\/doi.org\/10.1007\/978-1-4471-3503-6_4","DOI":"10.1007\/978-1-4471-3503-6_4"},{"key":"9_CR72","unstructured":"Vickers, S.: Geometric logic as a specification language. In: Hankin, C., Mackie, I., Hankin, R.N., Mackie, I., Nagarajan, R. (eds.) Proceedings for the Second Imperial College Department of Computing Workshop on Theory and Formal Methods, pp. 321\u2013340 (1995)"},{"key":"9_CR73","unstructured":"Zhang, J., Zhang, H.: SEM: a system for enumerating models. In: IJCAI, vol. 95, pp. 298\u2013303 (1995)"}],"container-title":["Lecture Notes in Computer Science","Protocols, Strands, and Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-91631-2_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,9]],"date-time":"2022-05-09T13:06:39Z","timestamp":1652101599000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-91631-2_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030916305","9783030916312"],"references-count":73,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-91631-2_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"19 November 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}