{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:19:24Z","timestamp":1750306764764,"version":"3.41.0"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2013,7,1]],"date-time":"2013-07-01T00:00:00Z","timestamp":1372636800000},"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. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2013,7]]},"abstract":"<jats:p>This article describes a multithreaded, portfolio-based approach to model checking, where multiple cores are exploited as the underlying computing framework to support concurrent execution of cooperative engines.<\/jats:p>\n          <jats:p>\n            We introduce a portfolio-based approach to model checking. Our portfolio is first driven by an approximate runtime predictor that provides a heuristic approximation to a\n            <jats:italic>perfect oracle<\/jats:italic>\n            and suggests which engines are more suitable for each verification instance. Scalability and robustness of the overall model-checking effort highly rely on a concurrent, multithreaded model of execution.\n          <\/jats:p>\n          <jats:p>Following similar approaches in related application fields, we dovetail data partitioning, focused on proving several properties in parallel, and engine partitioning, based on concurrent runs of different model-checking engines competing for completion of the same problem.<\/jats:p>\n          <jats:p>We investigate concurrency not only to effectively exploit several available engines, which operate independently, but also to show that a cooperative effort is possible. In this case, we adopt a straightforward, light-weight, model of inter-engine communication and data sharing.<\/jats:p>\n          <jats:p>We provide a detailed description of the ideas, algorithms, and experimental results obtained on the benchmarks from the Hardware Model Checking Competition suites (HWMCC'10 and HWMCC'11).<\/jats:p>","DOI":"10.1145\/2491477.2491480","type":"journal-article","created":{"date-parts":[[2013,7,25]],"date-time":"2013-07-25T19:12:41Z","timestamp":1374779561000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Thread-based multi-engine model checking for multicore platforms"],"prefix":"10.1145","volume":"18","author":[{"given":"Gianpiero","family":"Cabodi","sequence":"first","affiliation":[{"name":"Politecnico di Torino, Turin, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sergio","family":"Nocco","sequence":"additional","affiliation":[{"name":"Politecnico di Torino, Turin, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefano","family":"Quer","sequence":"additional","affiliation":[{"name":"Politecnico di Torino, Turin, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2013,7,29]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Lecture Notes Computer Science","volume":"4595","author":"Barnat J.","unstructured":"Barnat , J. , Brim , L. , and Rockai , P . 2007. Scalable Multi-core LTL model-checking. In model checking software . Lecture Notes Computer Science , vol. 4595 . Springer, Berlin Heidelberg, 187--203. Barnat, J., Brim, L., and Rockai, P. 2007. Scalable Multi-core LTL model-checking. In model checking software. Lecture Notes Computer Science, vol. 4595. Springer, Berlin Heidelberg, 187--203."},{"volume-title":"Proceedings of the 24th International Conference on Computer Design (ICCD'06)","author":"Baumgartner J.","key":"e_1_2_1_2_1","unstructured":"Baumgartner , J. , Mony , H. , Paruthi , V. , Kanzelman , R. , and Janssen , G . 2006. Scalable sequential equivalence checking across arbitrary design transformations . In Proceedings of the 24th International Conference on Computer Design (ICCD'06) . Baumgartner, J., Mony, H., Paruthi, V., Kanzelman, R., and Janssen, G. 2006. Scalable sequential equivalence checking across arbitrary design transformations. In Proceedings of the 24th International Conference on Computer Design (ICCD'06)."},{"key":"e_1_2_1_3_1","volume-title":"PicoSAT and PrecoSAT as SAT Race","author":"Biere A.","year":"2010","unstructured":"Biere , A. 2010. Lingeling , Plingeling , PicoSAT and PrecoSAT as SAT Race 2010 . Tech. rep., Johannes Kepler University , Linz, Austria. Aug. Biere, A. 2010. Lingeling, Plingeling, PicoSAT and PrecoSAT as SAT Race 2010. Tech. rep., Johannes Kepler University, Linz, Austria. Aug."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/309847.309942"},{"key":"e_1_2_1_5_1","unstructured":"Biere A. and Claessen K. L. 2010. The hardware model checking competition webpage. http:\/\/fmv.jku.at\/hwmcc10.  Biere A. and Claessen K. L. 2010. The hardware model checking competition webpage. http:\/\/fmv.jku.at\/hwmcc10."},{"key":"e_1_2_1_6_1","unstructured":"Biere A. and Claessen K. L. 2011. The hardware model checking competition webpage. http:\/\/fmv.jku.at\/hwmcc11.  Biere A. and Claessen K. L. 2011. The hardware model checking competition webpage. http:\/\/fmv.jku.at\/hwmcc11."},{"key":"e_1_2_1_7_1","unstructured":"Biere A. and Jussila T. 2007. The hardware model checking competition webpage. http:\/\/fmv.jku.at\/hwmcc07.  Biere A. and Jussila T. 2007. The hardware model checking competition webpage. http:\/\/fmv.jku.at\/hwmcc07."},{"key":"e_1_2_1_8_1","unstructured":"Biere A. and Jussila T. 2008. The hardware model checking competition webpage. http:\/\/fmv.jku.at\/hwmcc08.  Biere A. and Jussila T. 2008. The hardware model checking competition webpage. http:\/\/fmv.jku.at\/hwmcc08."},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design. Lecture Notes Computer Science","volume":"1954","author":"Bjesse P.","unstructured":"Bjesse , P. and Claessen , K . 2000. SAT-based verification without state space traversal . In Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design. Lecture Notes Computer Science , vol. 1954 . Springer, Berlin Heidelberg, 409--426. Bjesse, P. and Claessen, K. 2000. SAT-based verification without state space traversal. In Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design. Lecture Notes Computer Science, vol. 1954. Springer, Berlin Heidelberg, 409--426."},{"volume-title":"Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI'09)","author":"Bordeaux L.","key":"e_1_2_1_10_1","unstructured":"Bordeaux , L. , Hamadi , Y. , and Samulowitz , H . 2009. Experiments with massively parallel constraint solving . In Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI'09) . 443--448. Bordeaux, L., Hamadi, Y., and Samulowitz, H. 2009. Experiments with massively parallel constraint solving. In Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI'09). 443--448."},{"key":"e_1_2_1_11_1","unstructured":"Bradley A. 2010. IC3: SAT-based model checking without unrolling. http:\/\/ecee.colorado.edu\/&sim;bradleya\/ic3\/.  Bradley A. 2010. IC3: SAT-based model checking without unrolling. http:\/\/ecee.colorado.edu\/&sim;bradleya\/ic3\/."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_5"},{"volume-title":"Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD'08)","author":"Cabodi G.","key":"e_1_2_1_13_1","unstructured":"Cabodi , G. , Camurati , P. , Garcia , L. , Murciano , M. , Nocco , S. , and Quer , S . 2008a. Trading-off SAT search and variable quantifications for effective unbounded model checking . In Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD'08) . 205--212. Cabodi, G., Camurati, P., Garcia, L., Murciano, M., Nocco, S., and Quer, S. 2008a. Trading-off SAT search and variable quantifications for effective unbounded model checking. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD'08). 205--212."},{"volume-title":"Proceedings of the International Conference on Computer-Aided Design. ACM Press, 129--136","author":"Cabodi G.","key":"e_1_2_1_14_1","unstructured":"Cabodi , G. , Camurati , P. , and Murciano , M . 2008b. Automated abstraction by incremental refinement in interpolant-based model checking . In Proceedings of the International Conference on Computer-Aided Design. ACM Press, 129--136 . Cabodi, G., Camurati, P., and Murciano, M. 2008b. Automated abstraction by incremental refinement in interpolant-based model checking. In Proceedings of the International Conference on Computer-Aided Design. ACM Press, 129--136."},{"volume-title":"Proceedings of the IEEE International Symposium on Circuits and Systems (ISCAS'94)","author":"Cabodi G.","key":"e_1_2_1_15_1","unstructured":"Cabodi , G. , Camurati , P. , and Quer , S . 1994. Detecting hard faults with combined approximate forward\/backward symbolic techniques . In Proceedings of the IEEE International Symposium on Circuits and Systems (ISCAS'94) . 25--30. Cabodi, G., Camurati, P., and Quer, S. 1994. Detecting hard faults with combined approximate forward\/backward symbolic techniques. In Proceedings of the IEEE International Symposium on Circuits and Systems (ISCAS'94). 25--30."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2010.2041847"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1233501.1233661"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297666.1297669"},{"volume-title":"Proceedings of the Design Automation & Test in Europe Conference. IEEE Computer Society.","author":"Cabodi G.","key":"e_1_2_1_19_1","unstructured":"Cabodi , G. and Nocco , S . 2011. Optimized model checking of multiple properties . In Proceedings of the Design Automation & Test in Europe Conference. IEEE Computer Society. Cabodi, G. and Nocco, S. 2011. Optimized model checking of multiple properties. In Proceedings of the Design Automation & Test in Europe Conference. IEEE Computer Society."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2008.2009147"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0123-3"},{"volume-title":"Proceedings of the International Conference on Formal Methods in Computer-Aided Design. IEEE, 135--143","author":"Chockler H.","key":"e_1_2_1_22_1","unstructured":"Chockler , H. , Ivrii , A. , Matsliah , A. , Moran , S. , and Nevo , Z . 2011. Incremental formal verification of hardware . In Proceedings of the International Conference on Formal Methods in Computer-Aided Design. IEEE, 135--143 . Chockler, H., Ivrii, A., Matsliah, A., Moran, S., and Nevo, Z. 2011. Incremental formal verification of hardware. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design. IEEE, 135--143."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1048935.1050188"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82542-3"},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Feldman Y. Darshovitz N. and Hanna Z. 2005. Parallel multithreaded satisfiability solver: Design and implementation. Electron. Notes Theor. Comput. Sci. 128 3 Elsevier 75--90.  Feldman Y. Darshovitz N. and Hanna Z. 2005. Parallel multithreaded satisfiability solver: Design and implementation. Electron. Notes Theor. Comput. Sci. 128 3 Elsevier 75--90.","DOI":"10.1016\/j.entcs.2004.10.020"},{"key":"e_1_2_1_26_1","volume-title":"Principal and Practice of Constraint Programming. Lecture Notes Computer Science","volume":"6308","author":"Guo L.","unstructured":"Guo , L. , Hamadi , Y. , Jabbour , S. , and Sais , L . 2010. Diversification and intensification in parallel SAT solving . In Principal and Practice of Constraint Programming. Lecture Notes Computer Science , vol. 6308 , Springer, Berlin Heidelberg, 252--265. Guo, L., Hamadi, Y., Jabbour, S., and Sais, L. 2010. Diversification and intensification in parallel SAT solving. In Principal and Practice of Constraint Programming. Lecture Notes Computer Science, vol. 6308, Springer, Berlin Heidelberg, 252--265."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190070"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1020373206491"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1126\/science.275.5296.51"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2007.358108"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_2_1_32_1","volume-title":"ABC: A system for sequential synthesis and verification","author":"Mishchenko A.","year":"2005","unstructured":"Mishchenko , A. 2005 . ABC: A system for sequential synthesis and verification , http:\/\/www.eecs.berkeley.edu\/&sim;alanmi\/abc\/. Mishchenko, A. 2005. ABC: A system for sequential synthesis and verification, http:\/\/www.eecs.berkeley.edu\/&sim;alanmi\/abc\/."},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design. Lecture Notes Computer Science","volume":"3312","author":"Mony H.","unstructured":"Mony , H. , Baumgartner , J. , Paruthi , V. , Kanzelman , R. , and Kuehlmann , A . 2004. Scalable automated verification via expert-system guided transformations . In Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design. Lecture Notes Computer Science , vol. 3312 , Springer, Berlin Heidelberg, 159--173. Mony, H., Baumgartner, J., Paruthi, V., Kanzelman, R., and Kuehlmann, A. 2004. Scalable automated verification via expert-system guided transformations. In Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design. Lecture Notes Computer Science, vol. 3312, Springer, Berlin Heidelberg, 159--173."},{"key":"e_1_2_1_34_1","volume-title":"Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design, W. A. Hunt Jr. and S. D. Johnson, Eds. Lecture Notes Computer Science","volume":"1954","author":"Sheeran M.","unstructured":"Sheeran , M. , Singh , S. , and St\u00e5lmarck , G . 2000. Checking Safety Properties using induction and a SAT solver . In Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design, W. A. Hunt Jr. and S. D. Johnson, Eds. Lecture Notes Computer Science , vol. 1954 , Springer, Berlin Heidelberg, 108--125. Sheeran, M., Singh, S., and St\u00e5lmarck, G. 2000. Checking Safety Properties using induction and a SAT solver. In Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design, W. A. Hunt Jr. and S. D. Johnson, Eds. Lecture Notes Computer Science, vol. 1954, Springer, Berlin Heidelberg, 108--125."},{"volume-title":"Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT'01)","author":"Sinz C.","key":"e_1_2_1_35_1","unstructured":"Sinz , C. , Blochinger , W. , and Kuchlin , W . 2001. PaSAT - Parallel SAT-checking with lemma exchange: Implementatio and application . In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT'01) . Sinz, C., Blochinger, W., and Kuchlin, W. 2001. PaSAT - Parallel SAT-checking with lemma exchange: Implementatio and application. In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT'01)."},{"volume-title":"Proceedings of the International Workshop on Logic Synthesis.","author":"Sterin B.","key":"e_1_2_1_36_1","unstructured":"Sterin , B. , Een , N. , Mishchenko , A. , and Brayton , R. K . 2011. The benefit of concurrency in model checking . In Proceedings of the International Workshop on Logic Synthesis. Sterin, B., Een, N., Mishchenko, A., and Brayton, R. K. 2011. The benefit of concurrency in model checking. In Proceedings of the International Workshop on Logic Synthesis."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/240518.240639"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the 8th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC'09)","volume":"14","author":"Wieringa S.","unstructured":"Wieringa , S. , Niemenmaa , M. , and Heljanko , K . 2009. Tarmo: A framework for parallelized bounded model checking . In Proceedings of the 8th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC'09) , L. Brim and J. van der Pol, Eds. Electronic Proceedings in Theoretical Computer Science , vol. 14 . Elsevier, 62--76. Wieringa, S., Niemenmaa, M., and Heljanko, K. 2009. Tarmo: A framework for parallelized bounded model checking. In Proceedings of the 8th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC'09), L. Brim and J. van der Pol, Eds. Electronic Proceedings in Theoretical Computer Science, vol. 14. Elsevier, 62--76."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/263767.263784"}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2491477.2491480","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2491477.2491480","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:28:49Z","timestamp":1750231729000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2491477.2491480"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,7]]},"references-count":39,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2013,7]]}},"alternative-id":["10.1145\/2491477.2491480"],"URL":"https:\/\/doi.org\/10.1145\/2491477.2491480","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2013,7]]},"assertion":[{"value":"2011-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-07-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}