{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T17:25:10Z","timestamp":1763227510174,"version":"3.37.3"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2021,11,1]],"date-time":"2021-11-01T00:00:00Z","timestamp":1635724800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,11,1]],"date-time":"2021-11-01T00:00:00Z","timestamp":1635724800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2021,11]]},"DOI":"10.1007\/s10703-022-00389-5","type":"journal-article","created":{"date-parts":[[2022,2,5]],"date-time":"2022-02-05T14:02:49Z","timestamp":1644069769000},"page":"375-398","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Incremental design-space model checking via reusable reachable state approximations"],"prefix":"10.1007","volume":"58","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7152-8115","authenticated-orcid":false,"given":"Rohit","family":"Dureja","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kristin Y.","family":"Rozier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,2,5]]},"reference":[{"issue":"4","key":"389_CR1","doi-asserted-by":"publisher","first-page":"1023","DOI":"10.2514\/1.26311","volume":"30","author":"C Bauer","year":"2007","unstructured":"Bauer C, Lagadec K, B\u00e8s C, Mongeau M (2007) Flight control system architecture optimization for fly-by-wire airliners. J Guid Control Dyn 30(4):1023\u20131029. https:\/\/doi.org\/10.2514\/1.26311","journal-title":"J Guid Control Dyn"},{"key":"389_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-41540-6_1","volume-title":"Computer aided verification","author":"M Gario","year":"2016","unstructured":"Gario M, Cimatti A, Mattarei C, Tonetta S, Rozier KY (2016) Model checking at scale: automated air traffic control design space exploration. In: Chaudhuri S, Farzan A (eds) Computer aided verification. Springer, Cham, pp 3\u201322. https:\/\/doi.org\/10.1007\/978-3-319-41540-6_1"},{"key":"389_CR3","doi-asserted-by":"publisher","unstructured":"Mattarei C, Cimatti A, Gario M, Tonetta S, Rozier KY (2015) Comparing different functional allocations in automated air traffic control design. In: Formal methods in computer-aided design. FMCAD Inc, Austin, pp 112\u2013119. https:\/\/doi.org\/10.5555\/2893529.2893551","DOI":"10.5555\/2893529.2893551"},{"key":"389_CR4","doi-asserted-by":"publisher","unstructured":"Bozzano M, Cimatti A, Pires AF, Jones D, Kimberly G, Petri T, Robinson R, Tonetta S (2015) Formal design and safety analysis of AIR6110 wheel brake system. In: Computer aided verification. Springer, Cham, pp 518\u2013535. https:\/\/doi.org\/10.1007\/978-3-319-21690-4_36","DOI":"10.1007\/978-3-319-21690-4_36"},{"key":"389_CR5","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1016\/j.scico.2014.04.005","volume":"96","author":"P James","year":"2014","unstructured":"James P, Moller F, Nga Nguyen H, Roggenbach M, Schneider S, Treharne H (2014) On modelling and verifying railway interlockings: tracking train lengths. Sci Comput Program 96:315\u2013336. https:\/\/doi.org\/10.1016\/j.scico.2014.04.005","journal-title":"Sci Comput Program"},{"key":"389_CR6","doi-asserted-by":"publisher","unstructured":"Moller F, Nguyen HN, Roggenbach M, Schneider S, Treharne H (2013) Defining and model checking abstractions of complex railway models using CSP$$\\vert $$$$\\vert $$B. In: Hardware and software: verification and testing. Springer, Berlin, pp 193\u2013208. https:\/\/doi.org\/10.1007\/978-3-642-39611-3_20","DOI":"10.1007\/978-3-642-39611-3_20"},{"key":"389_CR7","doi-asserted-by":"publisher","unstructured":"Dureja R, Rozier EWD, Rozier KY (2017) A case study in safety, security, and availability of wireless-enabled aircraft communication networks. In: Aviation technology, integration, and operations conference. AIAA, Denver, Colorado. https:\/\/doi.org\/10.2514\/6.2017-3112","DOI":"10.2514\/6.2017-3112"},{"issue":"7","key":"389_CR8","doi-asserted-by":"publisher","first-page":"322","DOI":"10.2514\/1.I010769","volume":"17","author":"R Dureja","year":"2020","unstructured":"Dureja R, Rozier KY (2020) Formal framework for safety, security, and availability of aircraft communication networks. J Aerosp Inf Syst 17(7):322\u2013335. https:\/\/doi.org\/10.2514\/1.I010769","journal-title":"J Aerosp Inf Syst"},{"key":"389_CR9","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, model checking, and abstract interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley AR (2011) SAT-based model checking without unrolling. In: Cousot R (ed) Verification, model checking, and abstract interpretation. Springer, Berlin, pp 70\u201387. https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7"},{"key":"389_CR10","doi-asserted-by":"publisher","unstructured":"Een N, Mishchenko A, Brayton R (2011) Efficient implementation of property directed reachability. In: Formal methods in computer-aided design. FMCAD Inc, Austin, pp 125\u2013134. https:\/\/doi.org\/10.5555\/2157654.2157675","DOI":"10.5555\/2157654.2157675"},{"key":"389_CR11","doi-asserted-by":"publisher","unstructured":"Yang B, Bryant RE, O\u2019Hallaron DR, Biere A, Coudert O, Janssen G, Ranjan RK, Somenzi F (1998) A performance study of BDD-based model checking. In: Hunt WA, Johnson SD (eds) Formal methods in computer-aided design. Springer, Berlin, pp 255\u2013289. https:\/\/doi.org\/10.1007\/3-540-49519-3_18","DOI":"10.1007\/3-540-49519-3_18"},{"key":"389_CR12","doi-asserted-by":"publisher","unstructured":"Beer I, Ben-David S, Eisner C, Landver A (1996) Rulebase: an industry-oriented formal verification tool. In: Design automation conference. Association for Computing Machinery, New York, pp 655\u2013660. https:\/\/doi.org\/10.1145\/240518.240642","DOI":"10.1145\/240518.240642"},{"issue":"3","key":"389_CR13","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/j.entcs.2006.12.021","volume":"174","author":"J Marques-Silva","year":"2007","unstructured":"Marques-Silva J (2007) Interpolant learning and reuse in sat-based model checking. Electron Notes Theor Comput Sci 174(3):31\u201343. https:\/\/doi.org\/10.1016\/j.entcs.2006.12.021","journal-title":"Electron Notes Theor Comput Sci"},{"issue":"5","key":"389_CR14","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1007\/s00165-017-0419-1","volume":"29","author":"P Schrammel","year":"2017","unstructured":"Schrammel P, Kroening D, Brain M, Martins R, Teige T, Bienm\u00fcller T (2017) Incremental bounded model checking for embedded software. Formal Aspects Comput 29(5):911\u2013931. https:\/\/doi.org\/10.1007\/s00165-017-0419-1","journal-title":"Formal Aspects Comput"},{"key":"389_CR15","doi-asserted-by":"publisher","unstructured":"Chockler H, Ivrii A, Matsliah A, Moran S, Nevo Z (2011) Incremental formal verification of hardware. In: Formal methods in computer-aided design. FMCAD Inc, Austin, pp 135\u2013143. https:\/\/doi.org\/10.5555\/2157654.2157676","DOI":"10.5555\/2157654.2157676"},{"key":"389_CR16","doi-asserted-by":"publisher","unstructured":"Yang G, Dwyer MB, Rothermel G (2009) Regression model checking. In: International conference on software maintenance. IEEE, New York, pp 115\u2013124. https:\/\/doi.org\/10.1109\/icsm.2009.5306334","DOI":"10.1109\/icsm.2009.5306334"},{"issue":"3","key":"389_CR17","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/s10703-006-0001-6","volume":"28","author":"H Chockler","year":"2006","unstructured":"Chockler H, KupfermanO Vardi MY (2006) Coverage metrics for temporal logic model checking. Formal Methods Syst Des 28(3):189\u2013212. https:\/\/doi.org\/10.1007\/s10703-006-0001-6","journal-title":"Formal Methods Syst Des"},{"key":"389_CR18","doi-asserted-by":"publisher","unstructured":"Classen A, Heymans P, Schobbens P-Y, Legay A, Raskin J-F (2010) Model checking lots of systems: efficient verification of temporal properties in software product lines. In: International conference on software engineering. Association for Computing Machinery, New York, pp 335\u2013344. https:\/\/doi.org\/10.1145\/1806799.1806850","DOI":"10.1145\/1806799.1806850"},{"key":"389_CR19","doi-asserted-by":"publisher","unstructured":"Classen A, Heymans P, Schobbens P-Y, Legay A (2011) Symbolic model checking of software product lines. In: International conference on software engineering. Association for Computing Machinery, New York, pp 321\u2013330. https:\/\/doi.org\/10.1145\/1985793.1985838","DOI":"10.1145\/1985793.1985838"},{"issue":"5","key":"389_CR20","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/s10009-012-0234-1","volume":"14","author":"A Classen","year":"2012","unstructured":"Classen A, Cordy M, Heymans P, Legay A, Schobbens P-Y (2012) Model checking software product lines with SNIP. Softw Tools Technol Transf 14(5):589\u2013612. https:\/\/doi.org\/10.1007\/s10009-012-0234-1","journal-title":"Softw Tools Technol Transf"},{"key":"389_CR21","doi-asserted-by":"publisher","unstructured":"Ben-David S, Sterin B, Atlee JM, Beidu S (2015) Symbolic model checking of product-line requirements using SAT-based methods. In: International conference on software engineering. IEEE Press, New York, pp 189\u2013199. https:\/\/doi.org\/10.5555\/2818754.2818780","DOI":"10.5555\/2818754.2818780"},{"issue":"8","key":"389_CR22","doi-asserted-by":"publisher","first-page":"1069","DOI":"10.1109\/TSE.2012.86","volume":"39","author":"A Classen","year":"2013","unstructured":"Classen A, Cordy M, Schobbens P-Y, Heymans P, Legay A, Raskin J-F (2013) Featured transition systems: foundations for verifying variability-intensive systems and their application to LTL model checking. IEEE Trans Softw Eng 39(8):1069\u20131089. https:\/\/doi.org\/10.1109\/TSE.2012.86","journal-title":"IEEE Trans Softw Eng"},{"key":"389_CR23","doi-asserted-by":"publisher","unstructured":"Dureja R, Rozier KY (2018) More scalable LTL model checking via discovering design-space dependencies (D$$^3$$). In: Tools and algorithms for the construction and analysis of systems. Springer, Cham, pp 309\u2013327. https:\/\/doi.org\/10.1007\/978-3-319-89960-2_17","DOI":"10.1007\/978-3-319-89960-2_17"},{"key":"389_CR24","doi-asserted-by":"publisher","unstructured":"Cimatti A, Griggio A, Mover S, Tonetta S (2013) Parameter synthesis with IC3. In: Formal methods in computer-aided design. FMCAD Inc, Austin, pp 165\u2013168. https:\/\/doi.org\/10.1109\/fmcad.2013.6679406","DOI":"10.1109\/fmcad.2013.6679406"},{"key":"389_CR25","doi-asserted-by":"publisher","unstructured":"Emerson EA, Kahlon V (2000) Reducing model checking of the many to the few. In: International conference on automated deduction. Springer, Berlin, pp 236\u2013254. https:\/\/doi.org\/10.1007\/10721959_19","DOI":"10.1007\/10721959_19"},{"key":"389_CR26","doi-asserted-by":"publisher","unstructured":"Goldberg E, G\u00fcdemann M, Kroening D, Mukherjee R (2018) Efficient verification of multi-property designs (the benefit of wrong assumptions). In: Design, automation test in Europe (DATE), pp 43\u201348. https:\/\/doi.org\/10.23919\/DATE.2018.8341977","DOI":"10.23919\/DATE.2018.8341977"},{"key":"389_CR27","doi-asserted-by":"publisher","unstructured":"Dureja R, Rozier KY (2017) FuseIC3: an algorithm for checking large design spaces. In: Formal methods in computer-aided design. FMCAD Inc, Austin, pp 164\u2013171. https:\/\/doi.org\/10.23919\/FMCAD.2017.8102255","DOI":"10.23919\/FMCAD.2017.8102255"},{"issue":"1","key":"389_CR28","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1145\/1327452.1327494","volume":"51","author":"A Andoni","year":"2008","unstructured":"Andoni A, Indyk P (2008) Near-optimal hashing algorithms for approximate nearest neighbor in high dimensions. Commun ACM 51(1):117\u2013122. https:\/\/doi.org\/10.1145\/1327452.1327494","journal-title":"Commun ACM"},{"key":"389_CR29","doi-asserted-by":"publisher","unstructured":"Biere A, Cimatti A, Clarke E, Zhu Y (1999) Symbolic model checking without BDDs. In: Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 193\u2013207. https:\/\/doi.org\/10.1007\/3-540-49059-0_14","DOI":"10.1007\/3-540-49059-0_14"},{"key":"389_CR30","doi-asserted-by":"publisher","unstructured":"McMillan KL (2003) Interpolation and sat-based model checking. In: Computer aided verification. Springer, Berlin, pp 1\u201313. https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"389_CR31","doi-asserted-by":"publisher","unstructured":"Vizel Y, Grumberg O (2009) Interpolation-sequence based model checking. In: Formal methods in computer-aided design. FMCAD Inc, Austin, pp 1\u20138. https:\/\/doi.org\/10.1109\/FMCAD.2009.5351148","DOI":"10.1109\/FMCAD.2009.5351148"},{"key":"389_CR32","doi-asserted-by":"publisher","unstructured":"Li J, Dureja R, Pu G, Rozier KY, Vardi MY (2018) SimpleCAR: an efficient bug-finding tool based on approximate reachability. In: Computer aided verification. Springer, Cham, pp 37\u201344. https:\/\/doi.org\/10.1007\/978-3-319-96142-2_5","DOI":"10.1007\/978-3-319-96142-2_5"},{"key":"389_CR33","doi-asserted-by":"publisher","unstructured":"Bradley AR (2012) Understanding IC3. In: Theory and applications of satisfiability testing. Springer, Berlin, pp 1\u201314. https:\/\/doi.org\/10.1007\/978-3-642-31612-8_1","DOI":"10.1007\/978-3-642-31612-8_1"},{"issue":"6","key":"389_CR34","doi-asserted-by":"publisher","first-page":"1026","DOI":"10.1109\/TCAD.2015.2481869","volume":"35","author":"A Griggio","year":"2016","unstructured":"Griggio A, Roveri M (2016) Comparing different variants of the IC3 algorithm for hardware model checking. IEEE Trans Comput Aided Des Integr Circuits Syst 35(6):1026\u20131039. https:\/\/doi.org\/10.1109\/TCAD.2015.2481869","journal-title":"IEEE Trans Comput Aided Des Integr Circuits Syst"},{"key":"389_CR35","doi-asserted-by":"publisher","unstructured":"Somenzi F, Bradley AR (2011) Ic3: where monolithic and incremental meet. In: Formal methods in computer-aided design. FMCAD Inc, Austin, pp 3\u20138. https:\/\/doi.org\/10.5555\/2157654.2157657","DOI":"10.5555\/2157654.2157657"},{"issue":"1","key":"389_CR36","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/3047307","volume":"50","author":"L Chi","year":"2017","unstructured":"Chi L, Zhu X (2017) Hashing techniques: a survey and taxonomy. ACM Comput Surv 50(1):11\u201311136. https:\/\/doi.org\/10.1145\/3047307","journal-title":"ACM Comput Surv"},{"issue":"3","key":"389_CR37","doi-asserted-by":"publisher","first-page":"630","DOI":"10.1006\/jcss.1999.1690","volume":"60","author":"AZ Broder","year":"2000","unstructured":"Broder AZ, Charikar M, Frieze AM, Mitzenmacher M (2000) Min-wise independent permutations. J Comput Syst Sci 60(3):630\u2013659. https:\/\/doi.org\/10.1006\/jcss.1999.1690","journal-title":"J Comput Syst Sci"},{"key":"389_CR38","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1017\/CBO9781139924801","volume-title":"Mining of massive datasets, Chap. 3","author":"A Rajaraman","year":"2011","unstructured":"Rajaraman A, Ullman JD (2011) Mining of massive datasets, Chap. 3. Cambridge University Press, New York, pp 55\u2013111. https:\/\/doi.org\/10.1017\/CBO9781139924801"},{"key":"389_CR39","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-017-0451-8","author":"G Cabodi","year":"2017","unstructured":"Cabodi G, Camurati PE, Loiacono C, Palena M, Pasini P, Patti D, Quer S (2017) To split or to group: from divide-and-conquer to sub-task sharing for verifying multiple properties in model checking. J Softw Tools Technol Transf. https:\/\/doi.org\/10.1007\/s10009-017-0451-8","journal-title":"J Softw Tools Technol Transf"},{"key":"389_CR40","doi-asserted-by":"publisher","unstructured":"Cabodi G, Nocco S (2011) Optimized model checking of multiple properties. In: Design, automation test in Europe. IEEE, New York, pp 1\u20134. https:\/\/doi.org\/10.1109\/DATE.2011.5763279","DOI":"10.1109\/DATE.2011.5763279"},{"key":"389_CR41","doi-asserted-by":"publisher","unstructured":"Cimatti A, Griggio A, Schaafsma BJ, Sebastiani R (2013) The MathSAT5 smt solver. In: Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 93\u2013107. https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"389_CR42","doi-asserted-by":"publisher","unstructured":"Dureja R, Baumgartner J, Ivrii A, Kanzelman R, Rozier KY (2019) Boosting verification scalability via structural grouping and semantic partitioning of properties. In: Formal methods in computer aided design. FMCAD Inc, Austin, pp 1\u20139. https:\/\/doi.org\/10.23919\/FMCAD.2019.8894265","DOI":"10.23919\/FMCAD.2019.8894265"},{"key":"389_CR43","doi-asserted-by":"publisher","unstructured":"Dureja R, Baumgartner J, Kanzelman R, Williams M, Rozier KY (2020) Accelerating parallel verification via complementary property partitioning and strategy exploration. In: Formal methods in computer aided design. FMCAD Inc, Austin, pp 16\u201325. https:\/\/doi.org\/10.34727\/2020\/isbn.978-3-85448-042-6_8","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_8"},{"key":"389_CR44","unstructured":"Claessen K, S\u00f6rensson N (2012) A liveness checking algorithm that counts. In: Formal methods in computer-aided design. FMCAD Inc, Austin, pp 52\u201359"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-022-00389-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-022-00389-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-022-00389-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,27]],"date-time":"2022-05-27T22:03:59Z","timestamp":1653689039000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-022-00389-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11]]},"references-count":44,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,11]]}},"alternative-id":["389"],"URL":"https:\/\/doi.org\/10.1007\/s10703-022-00389-5","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2021,11]]},"assertion":[{"value":"17 January 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 January 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 February 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}