{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T15:27:33Z","timestamp":1772119653479,"version":"3.50.1"},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2024,10,24]],"date-time":"2024-10-24T00:00:00Z","timestamp":1729728000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,24]],"date-time":"2024-10-24T00:00:00Z","timestamp":1729728000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2024,12]]},"DOI":"10.1007\/s10817-024-09713-6","type":"journal-article","created":{"date-parts":[[2024,10,24]],"date-time":"2024-10-24T05:02:27Z","timestamp":1729746147000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Practical Decision Procedure for Quantifier-Free, Decidable Languages Extended with Restricted Quantifiers"],"prefix":"10.1007","volume":"68","author":[{"given":"Maximiliano","family":"Cristi\u00e1","sequence":"first","affiliation":[]},{"given":"Gianfranco","family":"Rossi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,10,24]]},"reference":[{"key":"9713_CR1","unstructured":"Bell, D.E., LaPadula, L.: Secure computer systems: Mathematical foundations. MTR 2547. The MITRE Corporation, McLean, May 1973"},{"key":"9713_CR2","unstructured":"Bell, D.E., LaPadula, L.: Secure computer systems: mathematical model. ESD-TR 73-278. The MITRE Corporation, McLean, November 1973"},{"issue":"4","key":"9713_CR3","doi-asserted-by":"publisher","first-page":"1200","DOI":"10.2178\/jsl\/1164060452","volume":"71","author":"D Bell\u00e8","year":"2006","unstructured":"Bell\u00e8, D., Parlamento, F.: Truth in V for $$\\exists ^{{*}}\\forall \\forall $$-sentences is decidable. J. Symb. Log. 71(4), 1200\u20131222 (2006)","journal-title":"J. Symb. Log."},{"key":"9713_CR4","doi-asserted-by":"crossref","unstructured":"Berghammer, R., H\u00f6fner, P., Stucke, I.: Automated verification of relational while-programs. In: H\u00f6fner, P., Jipsen, P., Kahl, W., M\u00fcller, M.E. (eds.), Relational and Algebraic Methods in Computer Science\u201414th International Conference, RAMiCS 2014, Marienstatt, Germany, 28 April\u20131 May 2014. Proceedings. Lecture Notes in Computer Science, vol. 8428, pp. 173\u2013190. Springer, Berlin (2014)","DOI":"10.1007\/978-3-319-06251-8_11"},{"issue":"1","key":"9713_CR5","first-page":"27","volume":"26","author":"G Betarte","year":"2016","unstructured":"Betarte, G., Campo, J.D., Luna, C., Romano, A.: Formal analysis of Android\u2019s permission-based security model. Sci. Ann. Comput. Sci. 26(1), 27\u201368 (2016)","journal-title":"Sci. Ann. Comput. Sci."},{"key":"9713_CR6","unstructured":"Betarte, G., Campo, J.D., Luna, C.D., Romano, A.: Verifying Android\u2019s permission model. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) Theoretical Aspects of Computing - ICTAC 2015\u201412th International Colloquium Cali, Colombia, 29\u201331 October 2015, Proceedings. Lecture Notes in Computer Science, vol. 9399, pp. 485\u2013504. Springer, Berlin (2015)"},{"key":"9713_CR7","doi-asserted-by":"crossref","unstructured":"Boniol, F., Wiels, V.: The landing gear system case study. In: Boniol, F., Wiels, V., Ameur, Y.A., Schewe, K.-D. (eds.) ABZ 2014: The Landing Gear Case Study\u2014Case Study Track, Held at the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, Toulouse, France, 2\u20136 June 2014. Proceedings. Communications in Computer and Information Science, vol. 433, pp. 1\u201318. Springer (2014)","DOI":"10.1007\/978-3-319-07512-9_1"},{"key":"9713_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59207-2","volume-title":"The Classical Decision Problem. Perspectives in Mathematical Logic","author":"E B\u00f6rger","year":"1997","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, Berlin (1997)"},{"issue":"2","key":"9713_CR9","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1002\/cpa.3160340203","volume":"34","author":"M Breban","year":"1981","unstructured":"Breban, M., Ferro, A., Omodeo, E.G., Schwartz, J.T.: Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions. Commun. Pure Appl. Math. 34(2), 177\u2013195 (1981)","journal-title":"Commun. Pure Appl. Math."},{"key":"9713_CR10","volume-title":"Computable Set Theory","author":"D Cantone","year":"1989","unstructured":"Cantone, D., Ferro, A., Omodeo, E.: Computable Set Theory. Clarendon Press, New York (1989)"},{"key":"9713_CR11","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/j.tcs.2014.03.021","volume":"560","author":"D Cantone","year":"2014","unstructured":"Cantone, D., Longo, C.: A decidable two-sorted quantified fragment of set theory with ordered pairs and some undecidable extensions. Theor. Comput. Sci. 560, 307\u2013325 (2014)","journal-title":"Theor. Comput. Sci."},{"key":"9713_CR12","unstructured":"Cantone, D., Longo, C., Asmundo, M.N.: A decidable quantified fragment of set theory involving ordered pairs with applications to description logics. In: Bezem, M. (ed.) Computer Science Logic, 25th International Workshop\/20th Annual Conference of the EACSL, CSL 2011, 12\u201315 September 2011, Bergen, Norway, Proceedings. LIPIcs, vol. 12, pp. 129\u2013143. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik, Wadern (2011)"},{"key":"9713_CR13","doi-asserted-by":"crossref","unstructured":"Cantone, D., Omodeo, E.G., Policriti, A.: Set Theory for Computing\u2014From Decision Procedures to Declarative Programming with Sets. Monographs in Computer Science. Springer, Berlin (2001)","DOI":"10.1007\/978-1-4757-3452-2"},{"issue":"7","key":"9713_CR14","doi-asserted-by":"publisher","first-page":"1891","DOI":"10.1093\/comjnl\/bxab030","volume":"65","author":"M Cristi\u00e1","year":"2022","unstructured":"Cristi\u00e1, M., Katz, R.D., Rossi, G.: Proof automation in the theory of finite sets and finite set relation algebra. Comput. J. 65(7), 1891\u20131903 (2022)","journal-title":"Comput. J."},{"issue":"2","key":"9713_CR15","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/s10817-023-09666-2","volume":"67","author":"M Cristi\u00e1","year":"2023","unstructured":"Cristi\u00e1, M., De Luca, G., Luna, C.: An automatically verified prototype of the Android permissions system. J. Autom. Reason. 67(2), 17 (2023)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9713_CR16","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/s10817-019-09520-4","volume":"64","author":"M Cristi\u00e1","year":"2020","unstructured":"Cristi\u00e1, M., Rossi, G.: Solving quantifier-free first-order constraints over finite sets and binary relations. J. Autom. Reason. 64(2), 295\u2013330 (2020)","journal-title":"J. Autom. Reason."},{"issue":"4","key":"9713_CR17","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/s10817-020-09577-6","volume":"65","author":"M Cristi\u00e1","year":"2021","unstructured":"Cristi\u00e1, M., Rossi, G.: Automated proof of Bell-LaPadula security properties. J. Autom. Reason. 65(4), 463\u2013478 (2021)","journal-title":"J. Autom. Reason."},{"issue":"6","key":"9713_CR18","doi-asserted-by":"publisher","first-page":"809","DOI":"10.1007\/s10817-021-09589-w","volume":"65","author":"M Cristi\u00e1","year":"2021","unstructured":"Cristi\u00e1, M., Rossi, G.: Automated reasoning with restricted intensional sets. J. Autom. Reason. 65(6), 809\u2013890 (2021)","journal-title":"J. Autom. Reason."},{"issue":"8","key":"9713_CR19","doi-asserted-by":"publisher","first-page":"1125","DOI":"10.1007\/s10817-021-09602-2","volume":"65","author":"M Cristi\u00e1","year":"2021","unstructured":"Cristi\u00e1, M., Rossi, G.: An automatically verified prototype of the Tokeneer ID station specification. J. Autom. Reason. 65(8), 1125\u20131151 (2021)","journal-title":"J. Autom. Reason."},{"key":"9713_CR20","first-page":"24","volume":"53","author":"M Cristi\u00e1","year":"2021","unstructured":"Cristi\u00e1, M., Rossi, G.: $$\\{ log\\}$$: set formulas as programs. Rend. Ist. Mat. Univ. Trieste 53, 24 (2021). (Id\/No 23)","journal-title":"Rend. Ist. Mat. Univ. Trieste"},{"issue":"2","key":"9713_CR21","doi-asserted-by":"publisher","first-page":"468","DOI":"10.1017\/S1471068421000521","volume":"23","author":"M Cristi\u00e1","year":"2023","unstructured":"Cristi\u00e1, M., Rossi, G.: Integrating cardinality constraints into constraint logic programming with sets. Theory Pract. Log. Program. 23(2), 468\u2013502 (2023)","journal-title":"Theory Pract. Log. Program."},{"key":"9713_CR22","doi-asserted-by":"crossref","unstructured":"Cristi\u00e1, M., Rossi, G.: An automatically verified prototype of a landing gear system. In: Cantone, D., Pulvirenti, A. (eds.) From Computational Logic to Computational Biology - Essays Dedicated to Alfredo Ferro to Celebrate His Scientific Career, vol. 14070. Lecture Notes in Computer Science, pp. 56\u201381. Springer (2024)","DOI":"10.1007\/978-3-031-55248-9_3"},{"issue":"1","key":"9713_CR23","doi-asserted-by":"publisher","first-page":"3:1","DOI":"10.1145\/3625230","volume":"25","author":"M Cristi\u00e1","year":"2024","unstructured":"Cristi\u00e1, M., Rossi, G.: A decision procedure for a theory of finite sets with finite integer intervals. ACM Trans. Comput. Log. 25(1), 3:1-3:34 (2024)","journal-title":"ACM Trans. Comput. Log."},{"key":"9713_CR24","doi-asserted-by":"crossref","unstructured":"Cristi\u00e1, M., Rossi, G., Frydman, C.S.: $$\\{log\\}$$ as a test case generator for the Test Template Framework. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds), SEFM. Lecture Notes in Computer Science, vol. 8137, pp. 229\u2013243. Springer (2013)","DOI":"10.1007\/978-3-642-40561-7_16"},{"issue":"4\u20135","key":"9713_CR25","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1017\/S1471068415000290","volume":"15","author":"M Cristi\u00e1","year":"2015","unstructured":"Cristi\u00e1, M., Rossi, G., Frydman, C.S.: Adding partial functions to constraint logic programming with sets. Theory Pract. Log. Program. 15(4\u20135), 651\u2013665 (2015)","journal-title":"Theory Pract. Log. Program."},{"key":"9713_CR26","unstructured":"De Luca, G., Luna, C.: Towards a certified reference monitor of the Android 10 permission system. In: de\u2019Liguoro, U., Berardi, S., Altenkirch, T. (eds.) 26th International Conference on Types for Proofs and Programs, TYPES 2020, 2\u20135 March 2020, University of Turin, Italy. LIPIcs, vol. 188, pp. 3:1\u20133:18. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik (2020)"},{"key":"9713_CR27","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Efficient e-matching for SMT solvers. In: Pfenning, F. (ed.) Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, 17\u201320 July 2007, Proceedings. Lecture Notes in Computer Science, vol. 4603, pp. 183\u2013198. Springer (2007)","DOI":"10.1007\/978-3-540-73595-3_13"},{"issue":"3","key":"9713_CR28","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"issue":"5","key":"9713_CR29","doi-asserted-by":"publisher","first-page":"861","DOI":"10.1145\/365151.365169","volume":"22","author":"A Dovier","year":"2000","unstructured":"Dovier, A., Piazza, C., Pontelli, E., Rossi, G.: Sets and constraint logic programming. ACM Trans. Program. Lang. Syst. 22(5), 861\u2013931 (2000)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"6","key":"9713_CR30","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1017\/S1471068406002730","volume":"6","author":"A Dovier","year":"2006","unstructured":"Dovier, A., Pontelli, E., Rossi, G.: Set unification. Theory Pract. Log Program. 6(6), 645\u2013701 (2006)","journal-title":"Theory Pract. Log Program."},{"key":"9713_CR31","doi-asserted-by":"crossref","unstructured":"Dutertre, B., de\u00a0Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV. Lecture Notes in Computer Science, vol. 4144, pp. 81\u201394. Springer (2006)","DOI":"10.1007\/11817963_11"},{"key":"9713_CR32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_5","author":"YMY Feldman","year":"2019","unstructured":"Feldman, Y.M.Y., Padon, O., Immerman, N., Sagiv, M., Shoham, S.: Bounded quantifier instantiation for checking inductive invariants. Log. Methods Comput. Sci. (2019). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_5","journal-title":"Log. Methods Comput. Sci."},{"key":"9713_CR33","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem proving using lazy proof explication. In: Hunt Jr., W.A., Somenzi, F. (eds.) Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, 8\u201312 July 2003, Proceedings. Lecture Notes in Computer Science, vol. 2725, pp. 355\u2013367. Springer (2003)","DOI":"10.1007\/978-3-540-45069-6_34"},{"issue":"1\u20132","key":"9713_CR34","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/s10472-009-9153-6","volume":"55","author":"Y Ge","year":"2009","unstructured":"Ge, Y., Barrett, C.W., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. Ann. Math. Artif. Intell. 55(1\u20132), 101\u2013122 (2009)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9713_CR35","doi-asserted-by":"crossref","unstructured":"Ge, Y., de\u00a0Moura, L.M.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.), Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, 26 June\u20132 July 2009. Proceedings. Lecture Notes in Computer Science, vol. 5643, pp. 306\u2013320. Springer (2009)","DOI":"10.1007\/978-3-642-02658-4_25"},{"issue":"4","key":"9713_CR36","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s10817-006-9062-x","volume":"37","author":"S Givant","year":"2006","unstructured":"Givant, S.: The calculus of relations as a foundation for mathematics. J. Autom. Reason. 37(4), 277\u2013322 (2006)","journal-title":"J. Autom. Reason."},{"key":"9713_CR37","volume-title":"Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)"},{"issue":"2","key":"9713_CR38","doi-asserted-by":"publisher","first-page":"3:1","DOI":"10.19153\/cleiej.21.2.3","volume":"21","author":"C Luna","year":"2018","unstructured":"Luna, C., Betarte, G., Campo, J.D., Sanz, C., Cristi\u00e1, M., Gorostiaga, F.: A formal approach for the verification of the permission-based security model of Android. CLEI Electron. J. 21(2), 3:1-3:22 (2018)","journal-title":"CLEI Electron. J."},{"key":"9713_CR39","doi-asserted-by":"crossref","unstructured":"Mammar, A., Laleau, R.: Modeling a landing gear system in Event-B. In: Boniol, F., Wiels, V., Ameur, Y.A., Schewe, K.-D. (eds.) ABZ 2014: The Landing Gear Case Study\u2014Case Study Track, Held at the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, Toulouse, France, 2\u20136 June 2014. Proceedings. Communications in Computer and Information Science, vol. 433, pp. 80\u201394. Springer (2014)","DOI":"10.1007\/978-3-319-07512-9_6"},{"key":"9713_CR40","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1002\/malq.19960420105","volume":"42","author":"EG Omodeo","year":"1996","unstructured":"Omodeo, E.G., Parlamento, F., Policriti, A.: Decidability of $$\\exists ^{{*}}\\forall $$-sentences in membership theories. Math. Log. Q. 42, 41\u201358 (1996)","journal-title":"Math. Log. Q."},{"issue":"3","key":"9713_CR41","doi-asserted-by":"publisher","first-page":"896","DOI":"10.2178\/jsl\/1344862166","volume":"77","author":"EG Omodeo","year":"2012","unstructured":"Omodeo, E.G., Policriti, A.: The Bernays\u2013Sch\u00f6nfinkel\u2013Ramsey class for set theory: decidability. J. Symb. Log. 77(3), 896\u2013918 (2012)","journal-title":"J. Symb. Log."},{"issue":"1","key":"9713_CR42","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1002\/cpa.3160460104","volume":"46","author":"F Parlamento","year":"1993","unstructured":"Parlamento, F., Policriti, A.: Undecidability results for restricted universally quantified formulae of set theory. Commun. Pure Appl. Math. 46(1), 57\u201373 (1993)","journal-title":"Commun. Pure Appl. Math."},{"issue":"1","key":"9713_CR43","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1090\/S0002-9939-1988-0938682-2","volume":"103","author":"F Parlamento","year":"1988","unstructured":"Parlamento, F., Policriti, A.: The logically simplest form of the infinity axiom. Proc. Am. Math. Soc. 103(1), 274\u2013276 (1988)","journal-title":"Proc. Am. Math. Soc."},{"issue":"1","key":"9713_CR44","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1002\/malq.19920380110","volume":"38","author":"F Parlamento","year":"1992","unstructured":"Parlamento, F., Policriti, A.: The decision problem for restricted universal quantification in set theory and the axiom of foundation. Math. Log. Q. 38(1), 143\u2013156 (1992)","journal-title":"Math. Log. Q."},{"key":"9713_CR45","unstructured":"Rossi, G.: $$\\{log\\}$$ (2008). http:\/\/www.clpset.unipr.it\/setlog.Home.html. Last accessed 2022"},{"key":"9713_CR46","unstructured":"Schneider, S.: The B-method: An Introduction. Cornerstones of computing, Palgrave (2001)"},{"key":"9713_CR47","volume-title":"Using Z: Specification, Refinement, and Proof","author":"J Woodcock","year":"1996","unstructured":"Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice-Hall, Upper Saddle River (1996)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09713-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-024-09713-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09713-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,14]],"date-time":"2024-12-14T02:07:43Z","timestamp":1734142063000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-024-09713-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,24]]},"references-count":47,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2024,12]]}},"alternative-id":["9713"],"URL":"https:\/\/doi.org\/10.1007\/s10817-024-09713-6","relation":{"has-preprint":[{"id-type":"doi","id":"10.21203\/rs.3.rs-1936827\/v1","asserted-by":"object"}]},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,24]]},"assertion":[{"value":"6 August 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 September 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 October 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"23"}}