{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,10]],"date-time":"2025-09-10T22:24:08Z","timestamp":1757543048409,"version":"3.37.3"},"reference-count":55,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2020,8,29]],"date-time":"2020-08-29T00:00:00Z","timestamp":1598659200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,8,29]],"date-time":"2020-08-29T00:00:00Z","timestamp":1598659200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100012352","name":"Universit\u00e0 degli Studi di Milano","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100012352","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2021,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We develop <jats:italic>quantifier elimination procedures<\/jats:italic> for fragments of higher order logic arising from the formalization of distributed systems (especially of fault-tolerant ones). Such procedures can be used in symbolic manipulations like the computation of pre\/post images and of projections. We show in particular that our procedures are quite effective in producing <jats:italic>counter abstractions<\/jats:italic> that can be model-checked using standard SMT technology. In fact, very often in the current literature verification tasks for distributed systems are accomplished via counter abstractions. Such abstractions can sometimes be justified via simulations and bisimulations. In this work, we supply logical foundations to this practice, by our technique for second order quantifier elimination. We <jats:italic>implemented<\/jats:italic> our procedure for a simplified (but still expressive) subfragment and we showed that our method is able to successfully handle verification benchmarks from various sources with interesting performances.\n<\/jats:p>","DOI":"10.1007\/s10817-020-09578-5","type":"journal-article","created":{"date-parts":[[2020,8,29]],"date-time":"2020-08-29T12:02:38Z","timestamp":1598702558000},"page":"425-460","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Higher-Order Quantifier Elimination, Counter Simulations and Fault-Tolerant Systems"],"prefix":"10.1007","volume":"65","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6449-6883","authenticated-orcid":false,"given":"Silvio","family":"Ghilardi","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7162-5997","authenticated-orcid":false,"given":"Elena","family":"Pagani","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,8,29]]},"reference":[{"key":"9578_CR1","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: Proceedings of LICS, pp. 313\u2013321 (1996)"},{"key":"9578_CR2","unstructured":"Abdulla, P.A., Delzanno, G., Henda, N.B., Rezine, A.: Regular model checking without transducers. In: TACAS, volume 4424 of LNCS, pp. 721\u2013736 (2007)"},{"key":"9578_CR3","unstructured":"Alberti, F., Ghilardi, S., Orsini, A., Pagani, E.: Counter abstractions in model checking of distributed broadcast algorithms: Some case studies. In: Proceedings of CILC, CEUR Proceedings, pp. 102\u2013117 (2016)"},{"key":"9578_CR4","doi-asserted-by":"crossref","unstructured":"Alberti, F., Ghilardi, S., Pagani, E.: Counting constraints in flat array fragments. In: Proceedings of the IJCAR, volume 9706 of Lecture Notes in Computer Science, pp. 65\u201381 (2016)","DOI":"10.1007\/978-3-319-40229-1_6"},{"key":"9578_CR5","doi-asserted-by":"crossref","unstructured":"Alberti, F., Ghilardi, S., Pagani, E.: Cardinality constraints for arrays (decidability results and applications). Formal Methods in System Design (2017)","DOI":"10.1007\/s10703-017-0279-6"},{"issue":"4","key":"9578_CR6","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/s10817-015-9323-7","volume":"54","author":"F Alberti","year":"2015","unstructured":"Alberti, F., Ghilardi, S., Sharygina, N.: Decision procedures for flat array properties. J. Autom. Reason. 54(4), 327\u2013352 (2015)","journal-title":"J. Autom. Reason."},{"key":"9578_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-015-9934-4","volume-title":"An introduction to mathematical logic and type theory: to truth through proof. Applied Logic Series","author":"PB Andrews","year":"2002","unstructured":"Andrews, P.B.: An introduction to mathematical logic and type theory: to truth through proof. Applied Logic Series, vol. 27, 2nd edn. Kluwer, Dordrecht (2002)","edition":"2"},{"key":"9578_CR8","unstructured":"Babaoglu, O., Toueg, S.: Non-blocking atomic commitment. In: Distributed Systems, 2nd edn., pp. 147\u2013168, Sape Mullender Ed., Addison-Wesley (1993)"},{"key":"9578_CR9","doi-asserted-by":"crossref","unstructured":"Ben-Or, M.: Another advantage of free choice: completely asynchronous agreement protocols. In: Proceedings of the PODC, pp. 27\u201330 (1983)","DOI":"10.1145\/800221.806707"},{"key":"9578_CR10","doi-asserted-by":"crossref","unstructured":"Biely, M., Charron-Bost, B., Gaillard, A., Hutle, M., Schiper, A., Widder, J.: Tolerating corrupted communication. In: Proceedings of the PODC, pp. 244\u2013253 (2007)","DOI":"10.1145\/1281100.1281136"},{"key":"9578_CR11","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., von Gleissenthall, K., Rybalchenko, A.: Cardinalities and universal quantifiers for verifying parameterized systems. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (2016)","DOI":"10.1145\/2908080.2908129"},{"issue":"4","key":"9578_CR12","doi-asserted-by":"publisher","first-page":"824","DOI":"10.1145\/4221.214134","volume":"32","author":"G Bracha","year":"1985","unstructured":"Bracha, G., Toueg, S.: Asynchronous consensus and broadcast protocols. JACM 32(4), 824\u2013840 (1985)","journal-title":"JACM"},{"key":"9578_CR13","doi-asserted-by":"crossref","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: CAV, pp. 334\u2013342 (2014)","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"9578_CR14","doi-asserted-by":"crossref","unstructured":"Charron-Bost, B., Debrat, H., Merz, S.: Formal verification of consensus algorithms tolerating malicious faults. In: Stabilization, Safety, and Security of Distributed Systems, LNCS. pp. 120\u2013134. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-24550-3_11"},{"issue":"1","key":"9578_CR15","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1016\/j.jalgor.2003.11.001","volume":"51","author":"B Charron-Bost","year":"2004","unstructured":"Charron-Bost, B., Schiper, A.: Uniform consensus is harder than consensus. J. Algorithms 51(1), 15\u201337 (2004)","journal-title":"J. Algorithms"},{"key":"9578_CR16","doi-asserted-by":"crossref","unstructured":"Charron-Bost, B., Schiper, A.: The heard-of model: computing in distributed systems with benign faults. In: Distributed Computing, pp. 49\u201371 (2009)","DOI":"10.1007\/s00446-009-0084-6"},{"key":"9578_CR17","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A.: Software model checking via IC3. In: CAV, pp. 277\u2013293 (2012)","DOI":"10.1007\/978-3-642-31424-7_23"},{"issue":"3","key":"9578_CR18","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1023\/A:1026276129010","volume":"23","author":"G Delzanno","year":"2003","unstructured":"Delzanno, G.: Constraint-based verification of parameterized cache coherence protocols. Form. Methods Syst. Design 23(3), 257\u2013301 (2003)","journal-title":"Form. Methods Syst. Design"},{"key":"9578_CR19","doi-asserted-by":"crossref","unstructured":"Delzanno, G., Esparza, J., Podelski, A.: Constraint-based analysis of broadcast protocols. In: Proceedings of CSL, volume 1683 of LNCS, pp. 50\u201366 (1999)","DOI":"10.1007\/3-540-48168-0_5"},{"key":"9578_CR20","volume-title":"Programming Languages","author":"EW Dijkstra","year":"1968","unstructured":"Dijkstra, E.W.: Cooperating sequential processes. In: Genuys, F. (ed.) Programming Languages. Academic Press, New York (1968)"},{"key":"9578_CR21","doi-asserted-by":"crossref","unstructured":"Dragoj, C., Henzinger, T., Veith, H., Widder, J., Zufferey, D.: A logic-based framework for verifying consensus algorithms. In: Proceedings of the VMCAI (2014)","DOI":"10.1007\/978-3-642-54013-4_10"},{"key":"9578_CR22","unstructured":"Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: Proceedings of LICS, pp. 352\u2013359. IEEE Computer Society (1999)"},{"key":"9578_CR23","unstructured":"Fisman, D., Kupferman, O., Lustig, Y.: On verifying fault tolerance of distributed protocols. In: Proceedings of the TACAS, 2008. Full paper at https:\/\/www.researchgate.net\/publication\/220852375_On_Verifying_Fault_Tolerance_of_Distributed_Protocols"},{"key":"9578_CR24","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL, pp. 191\u2013202 (2002)","DOI":"10.1145\/565816.503291"},{"key":"9578_CR25","unstructured":"Gabbay, D.M., Schmidt, R., Szalas, A.: Second Order Quantifier Elimination: Foundations, Computational Aspects and Applications. ACM Digital Library (2008)"},{"key":"9578_CR26","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Pagani, E.: Counter simulations via higher order quantifier elimination: a preliminary report. In: Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, PxTP 2017, Bras\u00edlia, Brazil, 23\u201324 Sept. 2017, pp. 39\u201353 (2017)","DOI":"10.4204\/EPTCS.262.5"},{"key":"9578_CR27","unstructured":"Ghilardi, S., Pagani, E.: Second order quantifier elimination: towards verification applications. In: Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017), Dresden, Germany, December 6\u20138, 2017, pp. 36\u201350 (2017)"},{"key":"9578_CR28","doi-asserted-by":"publisher","first-page":"2","DOI":"10.2168\/LMCS-6(4:10)2010","volume":"1","author":"S Ghilardi","year":"2010","unstructured":"Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by SMT solving: termination and Invariant Synthesis. Log. Methods Comput. Sci. 1, 2 (2010). https:\/\/doi.org\/10.2168\/LMCS-6(4:10)2010","journal-title":"Log. Methods Comput. Sci."},{"key":"9578_CR29","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Ranise, S.: MCMT: a model checker modulo theories. In: IJCAR, pp. 22\u201329 (2010)","DOI":"10.1007\/978-3-642-14203-1_3"},{"key":"9578_CR30","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/S0020-0190(00)00171-X","volume":"79","author":"R Guerraoui","year":"2001","unstructured":"Guerraoui, R.: On the hardness of failure-sensitive agreement problems. Inf. Process. Lett. 79, 99\u2013104 (2001)","journal-title":"Inf. Process. Lett."},{"key":"9578_CR31","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: CAV, pp. 343\u2013361 (2015)","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"9578_CR32","doi-asserted-by":"crossref","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: SAT, pp. 157\u2013171 (2012)","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"9578_CR33","doi-asserted-by":"crossref","unstructured":"Hoder, K., Bj\u00f8rner, N., de\u00a0Moura, L.: $$\\mu $$Z\u2014an efficient engine for fixed points with constraints. In: CAV, pp. 457\u2013462 (2011)","DOI":"10.1007\/978-3-642-22110-1_36"},{"key":"9578_CR34","doi-asserted-by":"crossref","unstructured":"John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In: Proceedings of International Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 201\u2013209 (2013, Aug)","DOI":"10.1109\/FMCAD.2013.6679411"},{"key":"9578_CR35","doi-asserted-by":"crossref","unstructured":"John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Towards modeling and model checking fault-tolerant distributed algorithms. In: Proceedings of the International SPIN Symposium on Model Checking of Software, volume 7976 of Lecture Notes in Computer Science, pp. 209\u2013226. Springer, Berlin (2013, July)","DOI":"10.1007\/978-3-642-39176-7_14"},{"key":"9578_CR36","doi-asserted-by":"crossref","unstructured":"Konnov, I.: ByMC: Byzantine Model Checker. http:\/\/forsyte.at\/software\/bymc\/, last visit: July 17 (2018)","DOI":"10.1007\/978-3-030-03424-5_22"},{"key":"9578_CR37","doi-asserted-by":"crossref","unstructured":"Konnov, I., Veith, H., Widder, J.: On the completeness of bounded model checking for threshold-based distributed algorithms: reachability. In: Proceedings of CONCUR, LNCS, pp. 125\u2013140 (2014)","DOI":"10.1007\/978-3-662-44584-6_10"},{"key":"9578_CR38","doi-asserted-by":"crossref","unstructured":"Konnov, I.V., Veith, H., Widder, J.: What you always wanted to know about model checking of fault-tolerant distributed algorithms. In: Perspectives of System Informatics\u201410th International Andrei Ershov Informatics Conference, PSI 2015, in Memory of Helmut Veith, Kazan and Innopolis, Russia, August 24\u201327, 2015, Revised Selected Papers, pp. 6\u201321 (2015)","DOI":"10.1007\/978-3-319-41579-6_2"},{"key":"9578_CR39","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/j.ic.2016.03.006","volume":"252","author":"IV Konnov","year":"2017","unstructured":"Konnov, I.V., Veith, H., Widder, J.: On the completeness of bounded model checking for threshold-based distributed algorithms: reachability. Inf. Comput. 252, 95\u2013109 (2017)","journal-title":"Inf. Comput."},{"key":"9578_CR40","unstructured":"Koopmann, P., Rudolph, S., Schmidt, R.A., Wernhard, C. (eds.): Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017), Dresden, Germany, December 6\u20138, 2017, volume 2013 of CEUR Workshop Proceedings. CEUR-WS.org (2017)"},{"key":"9578_CR41","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Interpolation and symbol elimination. In: Automated Deduction\u2014CADE-22. In: 22nd International Conference on Automated Deduction, Montreal, Canada, August 2\u20137, 2009. Proceedings, pp. 199\u2013213 (2009)","DOI":"10.1007\/978-3-642-02959-2_17"},{"issue":"3","key":"9578_CR42","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/s10817-006-9042-1","volume":"36","author":"V Kuncak","year":"2006","unstructured":"Kuncak, V., Nguyen, H.H., Rinard, M.: Deciding boolean algebra with Presburger arithmetic. J. Autom. Reas. 36(3), 213\u2013239 (2006)","journal-title":"J. Autom. Reas."},{"key":"9578_CR43","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Nguyen, H.H., Rinard, M.: An Algorithm for deciding BAPA: boolean algebra with Presburger arithmetic. In: Proceedings of CADE-20, volume 3632 of LNCS (July 2005)","DOI":"10.1007\/11532231_20"},{"key":"9578_CR44","unstructured":"Lambek, J., Scott, P.J.: Introduction to higher order categorical logic, volume\u00a07 of Cambridge Studies in Advanced Mathematics. Cambridge University Press, Cambridge, 1988. Reprint of the 1986 original"},{"key":"9578_CR45","volume-title":"Distributed Algorithms","author":"NA Lynch","year":"1996","unstructured":"Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann, Burlington (1996)"},{"key":"9578_CR46","doi-asserted-by":"crossref","unstructured":"Maric, O., Sprenger, C., Basin, D.A.: Cutoff bounds for consensus algorithms. In: Computer Aided Verification\u201429th International Conference, CAV 2017, Heidelberg, July 24\u201328, 2017, Proceedings, Part II, pp. 217\u2013237 (2017)","DOI":"10.1007\/978-3-319-63390-9_12"},{"key":"9578_CR47","doi-asserted-by":"crossref","unstructured":"Papamarcos, M.S., Patel, J.H.: A low-overhead coherence solution for multiprocessors with private cache memories. In: Proceedings of the ISCA (1984). https:\/\/dl.acm.org\/citation.cfm?id=808204","DOI":"10.1145\/800015.808204"},{"issue":"2","key":"9578_CR48","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1145\/322186.322188","volume":"27","author":"M Pease","year":"1980","unstructured":"Pease, M., Shostak, R., Lamport, L.: Reaching agreement in the presence of faults. JACM 27(2), 228\u2013234 (1980)","journal-title":"JACM"},{"key":"9578_CR49","volume-title":"\u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt","author":"M Presburger","year":"1929","unstructured":"Presburger, M.: \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. Kluwer, Warszawa (1929)"},{"key":"9578_CR50","doi-asserted-by":"crossref","unstructured":"Raynal, M.: Fault-tolerant Agreement in Synchronous Message-Passing Systems. Morgan & Claypool\u2014Synthesis Lectures on Distributed Computing Theory series (2010)","DOI":"10.2200\/S00294ED1V01Y201009DCT003"},{"key":"9578_CR51","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., Barrett, C.W.: Counterexample-guided quantifier instantiation for synthesis in SMT. In: Proceedings of the CAV, pp. 198\u2013216 (2015)","DOI":"10.1007\/978-3-319-21668-3_12"},{"key":"9578_CR52","unstructured":"Schweikhart, N.: Arithmetic, first-order logic, and counting quantifiers. In: ACM TOCL, pp. 1\u201335 (2004)"},{"key":"9578_CR53","volume-title":"Fundamentals of Parallel Computer Architecture Multichip and Multicore Systems","author":"Y Solihin","year":"2008","unstructured":"Solihin, Y.: Fundamentals of Parallel Computer Architecture Multichip and Multicore Systems. Solihin Publishing & Consulting LLC, Raleigh (2008)"},{"issue":"3","key":"9578_CR54","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/28869.28876","volume":"34","author":"TK Srikanth","year":"1987","unstructured":"Srikanth, T.K., Toueg, S.: Optimal clock synchronization. JACM 34(3), 626\u2013645 (1987)","journal-title":"JACM"},{"issue":"2","key":"9578_CR55","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/BF01667080","volume":"2","author":"TK Srikanth","year":"1987","unstructured":"Srikanth, T.K., Toueg, S.: Simulating authenticated broadcasts to derive simple fault-tolerant algorithms. Distrib. Comput. 2(2), 80\u201394 (1987)","journal-title":"Distrib. Comput."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09578-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-020-09578-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09578-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,29]],"date-time":"2021-08-29T00:02:03Z","timestamp":1630195323000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-020-09578-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,8,29]]},"references-count":55,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,3]]}},"alternative-id":["9578"],"URL":"https:\/\/doi.org\/10.1007\/s10817-020-09578-5","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2020,8,29]]},"assertion":[{"value":"3 January 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 August 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 August 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}