{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:28:12Z","timestamp":1784845692683,"version":"3.55.0"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2024,10,29]],"date-time":"2024-10-29T00:00:00Z","timestamp":1730160000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2024,10,31]]},"abstract":"<jats:p>This article addresses the problem of checking invariant properties for a large class of symbolic transition systems defined by a combination of SMT theories and quantifiers. State variables can be functions from an uninterpreted sort (finite but unbounded) to an interpreted sort, such as the integers under the theory of linear arithmetic. This formalism is very expressive and can be used for modeling parameterized systems, array-manipulating programs, and more. We propose two algorithms for finding universal inductive invariants for such systems. The first algorithm combines an IC3-style loop with a form of implicit predicate abstraction to construct an invariant in an incremental manner. The second algorithm constructs an under-approximation of the original problem and searches for a formula which is an inductive invariant for this case; then, the invariant is generalized to the original case and checked with a portfolio of techniques. We have implemented the two algorithms and conducted an extensive experimental evaluation, considering various benchmarks and different tools from the literature. As far as we know, our method is the first capable of handling in a large class of systems in a uniform way. The experiment shows that both algorithms are competitive with the state of the art.<\/jats:p>","DOI":"10.1145\/3686153","type":"journal-article","created":{"date-parts":[[2024,8,3]],"date-time":"2024-08-03T10:32:03Z","timestamp":1722681123000},"page":"1-37","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Invariant Checking for SMT-Based Systems with Quantifiers"],"prefix":"10.1145","volume":"25","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2856-5236","authenticated-orcid":false,"given":"Gianluca","family":"Redondi","sequence":"first","affiliation":[{"name":"Fondazione Bruno Kessler and Universit\u00e1 di Trento, Trento, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1315-6990","authenticated-orcid":false,"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[{"name":"Fondazione Bruno Kessler, Trento, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3311-0893","authenticated-orcid":false,"given":"Alberto","family":"Griggio","sequence":"additional","affiliation":[{"name":"Fondazione Bruno Kessler, Trento, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4389-7471","authenticated-orcid":false,"given":"Kenneth L.","family":"Mcmillan","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, Austin, TX, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,10,29]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190087"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61467-6_16"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.5555\/2886151"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2021.3118448"},{"key":"e_1_3_3_8_2","first-page":"47","article-title":"MCMT in the Land of Parametrized Timed Automata","author":"Carioni Alessandro","year":"2012","unstructured":"Alessandro Carioni, Silvio Ghilardi, and Silvio Ranise. 2012. MCMT in the Land of Parametrized Timed Automata. In VERIFY-2010. Proceedings of the 6th International Verification Workshop (VERIFY \u201910). Markus Aderhold, Serge Autexier, and Heiko Mantel (Eds.), EPiC Series in Computing, Vol. 3, EasyChair, 47\u201364. 2398\u20137340","journal-title":"VERIFY-2010. Proceedings of the 6th International Verification Workshop (VERIFY \u201910)"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30494-4_27"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0257-4"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_8"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-19992-9_10"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/1838552.1838559"},{"key":"e_1_3_3_15_2","unstructured":"Alessandro Cimatti Alberto Griggio and Stefano Tonetta. 2021b. The VMT-lib Language and Tools. arXiv:2109.12821. Retrieved from https:\/\/arxiv.org\/abs\/2109.12821"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-95582-7_37"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_55"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679392"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_16"},{"issue":"3","key":"e_1_3_3_23_2","first-page":"1","article-title":"Bounded Quantifier Instantiation for Checking Inductive Invariants","volume":"15","author":"Feldman Yotam M. Y.","year":"2019","unstructured":"Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, and Sharon Shoham. 2019. Bounded Quantifier Instantiation for Checking Inductive Invariants. Logical Methods in Computer Science 15, 3 (2019), 1\u201347.","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-009-9153-6"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_6"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-6(4:10)2010"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-76384-8_9"},{"key":"e_1_3_3_28_2","first-page":"112","volume-title":"Proceedings of the International Conference on Formal Methods in Computer Aided Design (FMCAD \u201921)","author":"Goel Aman","year":"2021","unstructured":"Aman Goel and Karem A. Sakallah. 2021. Towards an Automatic Proof of Lamport's Paxos. In Proceedings of the International Conference on Formal Methods in Computer Aided Design (FMCAD \u201921). IEEE, 112\u2013122."},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950330"},{"key":"e_1_3_3_30_2","first-page":"115","volume-title":"Proceedings of the 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI \u201921)","author":"Hance Travis","year":"2021","unstructured":"Travis Hance, Marijn Heule, Ruben Martins, and Bryan Parno. 2021. Finding Invariants of Distributed Systems: It's a Small (Enough) World After All. In Proceedings of the 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI \u201921). USENIX Association, 115\u2013131."},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.5555\/2682923.2682947"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_40"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386018"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"e_1_3_3_35_2","volume-title":"Automated Verification of Infinite State Systems","author":"Krstic Sava","year":"2005","unstructured":"Sava Krstic. 2005. Parametrized System Verification with Guard Strengthening and Parameter Abstraction. In Automated Verification of Infinite State Systems."},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_5"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/1297658.1297662"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_39"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/3232164"},{"key":"e_1_3_3_40_2","first-page":"15","article-title":"I4: Incremental Inference of Inductive Invariants for Verification of Distributed Protocols","author":"Ma Haojun","year":"2019","unstructured":"Haojun Ma, Aman Goel, Jean-Baptiste Jeannin, Manos Kapritsos, Baris Kasikci, and Karem A. Sakallah. 2019. I4: Incremental Inference of Inductive Invariants for Verification of Distributed Protocols. In Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP \u201919). 15 pages.","journal-title":"Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP \u201919)"},{"key":"e_1_3_3_41_2","doi-asserted-by":"crossref","unstructured":"Makai Mann Ahmed Irfan Alberto Griggio Oded Padon and Clark W. Barrett. 2021. Counterexample-guided prophecy for model checking modulo the theory of arrays. arXiv:2101.06825.","DOI":"10.26226\/morressier.604907f41a80aac83ca25ced"},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_11"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8603010"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837640"},{"key":"e_1_3_3_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/2980983.2908118"},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498712"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45319-9_7"},{"key":"e_1_3_3_49_2","volume-title":"Proceedings of the International Conference on Computer Aided Verification (CAV \u201917)","author":"Reynolds Andrew","year":"2017","unstructured":"Andrew Reynolds. 2017. Quantifier Instantiation Beyond E-Matching. In Proceedings of the International Conference on Computer Aided Verification (CAV \u201917). Martin Brain and Liana Hadarean (Eds.)."},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.14"},{"key":"e_1_3_3_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_7"},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-24950-1_15"},{"key":"e_1_3_3_53_2","article-title":"DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols","author":"Yao Jianan","year":"2021","unstructured":"Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, and Gabriel Ryan. 2021. DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21).","journal-title":"Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21)"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3686153","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3686153","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:17:50Z","timestamp":1750295870000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3686153"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,29]]},"references-count":52,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2024,10,31]]}},"alternative-id":["10.1145\/3686153"],"URL":"https:\/\/doi.org\/10.1145\/3686153","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,29]]},"assertion":[{"value":"2023-11-13","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-07-24","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-29","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}