{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T14:12:01Z","timestamp":1773843121528,"version":"3.50.1"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2017,3,2]],"date-time":"2017-03-02T00:00:00Z","timestamp":1488412800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2018,6]]},"DOI":"10.1007\/s10009-017-0451-8","type":"journal-article","created":{"date-parts":[[2017,3,2]],"date-time":"2017-03-02T15:49:38Z","timestamp":1488469778000},"page":"313-325","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["To split or to group: from divide-and-conquer to sub-task sharing for verifying multiple properties in model checking"],"prefix":"10.1007","volume":"20","author":[{"given":"G.","family":"Cabodi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P. E.","family":"Camurati","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C.","family":"Loiacono","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Palena","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.","family":"Pasini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"D.","family":"Patti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.","family":"Quer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,3,2]]},"reference":[{"key":"451_CR1","unstructured":"Biere, A.: The AIGER And-Inverter Graph (AIG) format. http:\/\/fmv.jku.at\/aiger\/ . Accessed 23 Feb 2017"},{"issue":"2","key":"451_CR2","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1023\/A:1008779610539","volume":"18","author":"I Beer","year":"2001","unstructured":"Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in temporal model checking. Form. Methods Syst. Des. 18(2), 141\u2013163 (2001). doi: 10.1023\/A:1008779610539","journal-title":"Form. Methods Syst. Des."},{"key":"451_CR3","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proceedings of 36th Design Automation Conference, pp. 317\u2013320. IEEE Computer Society, New Orleans (1999)","DOI":"10.1145\/309847.309942"},{"key":"451_CR4","doi-asserted-by":"crossref","unstructured":"Biere, A., Claessen, K.L., Jussila, T.: The hardware model checking competition web page. Accessed 23 Feb 2017","DOI":"10.23919\/FMCAD.2017.8102233"},{"key":"451_CR5","doi-asserted-by":"publisher","unstructured":"Bradley, A.R.: SAT-Based Model Checking Without Unrolling, LNCS, vol. 6538, pp. 70\u201387. Springer, Berlin (2011). doi: 10.1007\/978-3-642-18275-4_7","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"451_CR6","doi-asserted-by":"crossref","unstructured":"Bradley, A.R.: Sat-based model checking without unrolling. In: VMCAI, Austin, Texas, pp. 70\u201387 (2011)","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"451_CR7","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"ABC: An Academic Industrial-Strength Verification Tool","author":"RK Brayton","year":"2010","unstructured":"Brayton, R.K., Mishchenko, A.: ABC: An Academic Industrial-Strength Verification Tool, pp. 24\u201340. Springer, Berlin (2010). doi: 10.1007\/978-3-642-14295-6_5"},{"issue":"8","key":"451_CR8","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C\u201335","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C\u201335(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"451_CR9","unstructured":"Cabodi, G.: DIFTS 2014: International workshop on design and implementation of formal tools and systems. http:\/\/fmgroup.polito.it\/cabodi\/difts2014\/ . Accessed 23 Feb 2017"},{"key":"451_CR10","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1002\/spe.2321","volume":"46","author":"G Cabodi","year":"2016","unstructured":"Cabodi, G., Camurati, P., Quer, S.: A Graph-labeling approach for efficient cone-of-influence computation in model-checking problems with multiple properties. Softw. Pract. Exp. 46, 493\u2013511 (2016). doi: 10.1002\/spe.2321","journal-title":"Softw. Pract. Exp."},{"key":"451_CR11","first-page":"135","volume":"9","author":"G Cabodi","year":"2016","unstructured":"Cabodi, G., Loiacono, C., Palena, M., Pasini, P., Patti, D., Quer, S., Vendraminetto, D., Biere, A., Heljanko, K.: Hardware model checking competition 2014: an analysis and comparison of model checkers and benchmarks. Int. J. Satisf. Boolean Model. Comput. (JSAT) 9, 135\u2013172 (2016)","journal-title":"Int. J. Satisf. Boolean Model. Comput. (JSAT)"},{"key":"451_CR12","doi-asserted-by":"publisher","unstructured":"Cabodi, G., Nocco, S.: Optimized model checking of multiple properties. In: Proceedings of Design Automation and Test in Europe Conference, pp. 1\u20134. IEEE Computer Society, Grenoble (2011). doi: 10.1109\/DATE.2011.5763279","DOI":"10.1109\/DATE.2011.5763279"},{"key":"451_CR13","unstructured":"Cabodi, G., Nocco, S., Quer, S.: Formal Method Group\u2019s home page. http:\/\/fmgroup.polito.it\/ . Accessed 23 Feb 2017"},{"issue":"2","key":"451_CR14","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/s10703-011-0123-3","volume":"39","author":"G Cabodi","year":"2011","unstructured":"Cabodi, G., Nocco, S., Quer, S.: Benchmarking a model checker for algorithmic improvements and tuning for performance. Form. Methods Syst. Des. 39(2), 205\u2013227 (2011). doi: 10.1007\/s10703-011-0123-3","journal-title":"Form. Methods Syst. Des."},{"issue":"11","key":"451_CR15","doi-asserted-by":"publisher","first-page":"1499","DOI":"10.1109\/TVLSI.2008.2001134","volume":"16","author":"J Campos","year":"2008","unstructured":"Campos, J., Al-Asaad, H.: A novel mutation-based validation paradigm for high-level hardware descriptions. IEEE Trans. Very Large Scale Integr. (VLSI) Syst. 16(11), 1499\u20131512 (2008). doi: 10.1109\/TVLSI.2008.2001134","journal-title":"IEEE Trans. Very Large Scale Integr. (VLSI) Syst."},{"key":"451_CR16","unstructured":"Camurati, P., Loiacono, C., Pasini, P., Patti, D., Quer, S.: To split or to Group: from divide-and-conquer to sub-task sharing in verifying multiple properties. In: International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS), Lausanne, Switzerland (2014)"},{"key":"451_CR17","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"The nuXmv Symbolic Model Checker","author":"R Cavada","year":"2014","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv Symbolic Model Checker, pp. 334\u2013342. Springer, Cham (2014). doi: 10.1007\/978-3-319-08867-9_22"},{"key":"451_CR18","doi-asserted-by":"publisher","unstructured":"Chen, M., Mishra, P.: Functional test generation using efficient property clustering and learning techniques. IEEE Trans. Comput. Aided Des. 29(3), 396\u2013404 (2010). doi: 10.1109\/TCAD.2010.2041846","DOI":"10.1109\/TCAD.2010.2041846"},{"key":"451_CR19","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/3-540-44585-4_7","volume-title":"A Practical Approach to Coverage in Model Checking, LNCS","author":"H Chockler","year":"2001","unstructured":"Chockler, H., Kupferman, O., Kurshan, R.P., Vardi, M.Y.: A Practical Approach to Coverage in Model Checking, LNCS, vol. 2102, pp. 66\u201378. Springer, Paris (2001). doi: 10.1007\/3-540-44585-4_7"},{"issue":"3","key":"451_CR20","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/s10703-006-0001-6","volume":"28","author":"H Chockler","year":"2006","unstructured":"Chockler, H., Kupferman, O., Vardi, M.Y.: Coverage metrics for temporal logic model checking. Form. Methods Syst. Des. 28(3), 189\u2013212 (2006). doi: 10.1007\/s10703-006-0001-6","journal-title":"Form. Methods Syst. Des."},{"key":"451_CR21","doi-asserted-by":"publisher","unstructured":"Fraer, R., Ikram, S., Kamhi, G., Leonard, T., Mokkedem, A.: Accelerated verification of RTL assertions based on satisfiability solvers. In: Proceedings of High-Level Design Validation and Test Workshop, pp. 107\u2013110 (2002). doi: 10.1109\/HLDVT.2002.1224437","DOI":"10.1109\/HLDVT.2002.1224437"},{"key":"451_CR22","doi-asserted-by":"publisher","unstructured":"Hoskote, Y., Kam, T., Ho, P.H., Zhao, X.: Coverage estimation for symbolic model checking. In: Proceedings of 36th Design Automation Conference, pp. 300\u2013305. ACM, New York (1999). doi: 10.1145\/309847.309936","DOI":"10.1145\/309847.309936"},{"key":"451_CR23","doi-asserted-by":"publisher","unstructured":"Baumgartner, J., Loiacono, C., Palena, M., Pasini, P., Patti, D., Quer, S., Ricossa, S., Vendraminetto, D.: Fast cone-of-influence computation and estimation in problems with multiple properties. In: Proceedings of Design Automation and Test in Europe Conference, pp. 803\u2013806. IEEE Computer Society, Grenoble (2013). doi: 10.7873\/DATE.2013.170","DOI":"10.7873\/DATE.2013.170"},{"key":"451_CR24","doi-asserted-by":"publisher","unstructured":"Jayakumar, N., Purandare, M., Somenzi, F.: Dos and don\u2019ts of CTL state coverage estimation. In: Proceedings of the 40th Annual Design Automation Conference, DAC \u201903, pp. 292\u2013295. ACM, New York (2003). doi: 10.1145\/775832.775908","DOI":"10.1145\/775832.775908"},{"key":"451_CR25","doi-asserted-by":"publisher","unstructured":"Katzir, L., Liberty, E., Somekh, O.: Estimating sizes of social networks via biased sampling. In: Proceedings of the 20th International Conference on World Wide Web, WWW \u201911, pp. 597\u2013606. ACM, New York (2011). doi: 10.1145\/1963405.1963489","DOI":"10.1145\/1963405.1963489"},{"key":"451_CR26","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/11678779_5","volume-title":"Simultaneous SAT-Based Model Checking of Safety Properties","author":"Z Khasidashvili","year":"2006","unstructured":"Khasidashvili, Z., Nadel, A., Palti, A., Hanna, Z.: Simultaneous SAT-Based Model Checking of Safety Properties, pp. 56\u201375. Springer, Berlin (2006). doi: 10.1007\/11678779_5"},{"key":"451_CR27","unstructured":"Kurant, M., Butt, C.T., Markopoulou, A.: Graph size estimate. In: CoRR(2012). arXiv:1210.0460"},{"key":"451_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Proceedings of Computer Aided Verification, LNCS","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) Proceedings of Computer Aided Verification, LNCS, vol. 2725, pp. 1\u201313. Springer, Boulder (2003). doi: 10.1007\/978-3-540-45069-6_1"},{"key":"451_CR29","doi-asserted-by":"crossref","unstructured":"Offutt, A.J., Untch, R.H.: Mutation 2000: Uniting the orthogonal. In: Mutation 2000: Mutation Testing in the Twentieth and the Twenty First Centuries, pp. 45\u201355. San Jose, CA, USA (2000)","DOI":"10.1007\/978-1-4757-5939-6_7"},{"key":"451_CR30","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/3-540-45657-0_39","volume-title":"Vacuum Cleaning CTL Formulae, LNCS","author":"M Purandare","year":"2002","unstructured":"Purandare, M., Somenzi, F.: Vacuum Cleaning CTL Formulae, LNCS, vol. 2102, pp. 485\u2013499. Springer, Copenhagen (2002). doi: 10.1007\/3-540-45657-0_39"},{"key":"451_CR31","doi-asserted-by":"publisher","unstructured":"Qin, X., Chen, M., Mishra, P.: Synchronized generation of directed tests using satisfiability solving. In: Proceedings of International Conference on VLSI Design, VLSID \u201910, pp. 351\u2013356. IEEE Computer Society, Washington (2010). doi: 10.1109\/VLSI.Design.2010.47","DOI":"10.1109\/VLSI.Design.2010.47"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-017-0451-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-017-0451-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-017-0451-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,19]],"date-time":"2019-09-19T07:33:12Z","timestamp":1568878392000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-017-0451-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,3,2]]},"references-count":31,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2018,6]]}},"alternative-id":["451"],"URL":"https:\/\/doi.org\/10.1007\/s10009-017-0451-8","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,3,2]]}}}