{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T05:41:00Z","timestamp":1742967660889,"version":"3.40.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319929699"},{"type":"electronic","value":"9783319929705"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-92970-5_12","type":"book-chapter","created":{"date-parts":[[2018,5,29]],"date-time":"2018-05-29T08:54:12Z","timestamp":1527584052000},"page":"189-204","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Online Enumeration of All Minimal Inductive Validity Cores"],"prefix":"10.1007","author":[{"given":"Jaroslav","family":"Bend\u00edk","sequence":"first","affiliation":[]},{"given":"Elaheh","family":"Ghassabani","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Whalen","sequence":"additional","affiliation":[]},{"given":"Ivana","family":"\u010cern\u00e1","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,5,30]]},"reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-319-17524-9_7","volume-title":"NASA Formal Methods","author":"J Backes","year":"2015","unstructured":"Backes, J., Cofer, D., Miller, S., Whalen, M.W.: Requirements analysis of a quad-redundant flight control system. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 82\u201396. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_7"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-319-41591-8_9","volume-title":"Software Engineering and Formal Methods","author":"J Bend\u00edk","year":"2016","unstructured":"Bend\u00edk, J., Bene\u0161, N., Barnat, J., \u010cern\u00e1, I.: Finding boundary elements in ordered sets with application to safety and requirements analysis. In: De Nicola, R., K\u00fchn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 121\u2013136. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41591-8_9"},{"key":"12_CR3","unstructured":"Bend\u00edk, J., Benes, N., Cern\u00e1, I., Barnat, J.: Tunable online MUS\/MSS enumeration. In: FSTTCS 2016, pp. 50:1\u201350:13 (2016)"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-540-39724-3_11","volume-title":"Correct Hardware Design and Verification Methods","author":"H Chockler","year":"2003","unstructured":"Chockler, H., Kupferman, O., Vardi, M.Y.: Coverage metrics for formal verification. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 111\u2013125. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-39724-3_11"},{"key":"12_CR5","unstructured":"Claessen, K., S\u00f6rensson, N.: A liveness checking algorithm that counts. In: FMCAD, pp. 52\u201359. IEEE (2012)"},{"key":"12_CR6","unstructured":"Een, N., et al.: Efficient implementation of property directed reachability. In FMCAD 2011 (2011)"},{"key":"12_CR7","unstructured":"Gacek, A., Backes, J., Whalen, M., Wagner, M., Ghassabani, E.: The Jkind model checker (2017). arXiv preprint arXiv:1712.01222"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Ghassabani, E., et al.: Efficient generation of inductive validity cores for safety properties. In: FSE 2016 (2016)","DOI":"10.1145\/2950290.2950346"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Ghassabani, E., Gacek, A., Whalen, M.W.: Efficient generation of all minimal inductive validity cores. In: FMCAD 2017 (2017)","DOI":"10.23919\/FMCAD.2017.8102238"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Ghassabani, E., Gacek, A., Whalen, M.W., Heimdahl, M., Lucas, W.: Proof-based coverage metrics for formal verification. In: ASE 2017 (2017)","DOI":"10.1109\/ASE.2017.8115632"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Hagen, G., Tinelli, C.: Scaling up the formal verification of lustre programs with SMT-based techniques. In: FMCAD 2008 (2008)","DOI":"10.1109\/FMCAD.2008.ECP.19"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., et al.: The synchronous dataflow programming language Lustre. In: Proceedings of the IEEE (1991)","DOI":"10.1109\/5.97300"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Li, W., Seshia, S.: A theory of mutations with applications to vacuity, coverage, and fault tolerance. In: FMCAD 2008, p. 25 (2008)","DOI":"10.1109\/FMCAD.2008.ECP.29"},{"issue":"2","key":"12_CR14","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1007\/s100090100062","volume":"4","author":"O Kupferman","year":"2003","unstructured":"Kupferman, O., Vardi, M.Y.: Vacuity detection in temporal model checking. STTT 4(2), 224\u2013233 (2003)","journal-title":"STTT"},{"issue":"2","key":"12_CR15","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/s10601-015-9183-0","volume":"21","author":"M Liffiton","year":"2016","unstructured":"Liffiton, M., et al.: Fast, flexible MUS enumeration. Constraints 21(2), 223\u2013250 (2016)","journal-title":"Constraints"},{"issue":"2","key":"12_CR16","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/s10601-015-9183-0","volume":"21","author":"MH Liffiton","year":"2016","unstructured":"Liffiton, M.H., Previti, A., Malik, A., Marques-Silva, J.: Fast, flexible MUS enumeration. Constraints 21(2), 223\u2013250 (2016)","journal-title":"Constraints"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Mebsout, A., Tinelli, C.: Proof certificates for SMT-based model checkers for infinite-state systems. In: FMCAD 2016 (2016)","DOI":"10.1109\/FMCAD.2016.7886669"},{"issue":"2","key":"12_CR18","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1145\/1646353.1646372","volume":"53","author":"SP Miller","year":"2010","unstructured":"Miller, S.P., Whalen, M.W., Cofer, D.D.: Software model checking takes off. Commun. ACM 53(2), 58\u201364 (2010)","journal-title":"Commun. ACM"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Murugesan, A., et al.: Compositional verification of a medical device system. In: HILT 2013 (2013)","DOI":"10.1145\/2527269.2527272"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Murugesan, A., et al.: Complete traceability for requirements in satisfaction arguments. In: RE 2016 (RE@Next! Track) (2016)","DOI":"10.1109\/RE.2016.35"},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 127\u2013144. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-40922-X_8"},{"key":"12_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-540-79707-4_7","volume-title":"Formal Methods for Industrial Critical Systems","author":"M Whalen","year":"2008","unstructured":"Whalen, M., Cofer, D., Miller, S., Krogh, B.H., Storm, W.: Integration of formal analysis into a model-based software development process. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol. 4916, pp. 68\u201384. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-79707-4_7"},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Whalen, M., Gay, G., You, D., Heimdahl, M., Staats, M.: Observable modified condition\/decision coverage. In: ICSE 2013. ACM (2013)","DOI":"10.1109\/ICSE.2013.6606556"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"You, D., Rayadurgam, S., Whalen, M., Heimdahl, M.: Efficient observability-based test generation by dynamic symbolic execution. In: ISSRE 2015 (2015)","DOI":"10.1109\/ISSRE.2015.7381816"},{"key":"12_CR25","unstructured":"Zhang, L., Malik, S.: Extracting small unsatisfiable cores from unsatisfiable boolean formula. In: SAT 2003 (2003)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-92970-5_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,18]],"date-time":"2019-10-18T15:23:45Z","timestamp":1571412225000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-92970-5_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319929699","9783319929705"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-92970-5_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}