{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T05:29:57Z","timestamp":1769750997979,"version":"3.49.0"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319961415","type":"print"},{"value":"9783319961422","type":"electronic"}],"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:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-96142-2_3","type":"book-chapter","created":{"date-parts":[[2018,7,20]],"date-time":"2018-07-20T15:55:08Z","timestamp":1532102108000},"page":"20-27","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":41,"title":["The JKind Model Checker"],"prefix":"10.1007","author":[{"given":"Andrew","family":"Gacek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Backes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mike","family":"Whalen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lucas","family":"Wagner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Elaheh","family":"Ghassabani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,7,18]]},"reference":[{"key":"3_CR1","unstructured":"Cadence JasperGold Formal Verification Platform. https:\/\/www.cadence.com\/"},{"key":"3_CR2","unstructured":"Synopsys VC Formal Platform. https:\/\/www.synopsys.com"},{"key":"3_CR3","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":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-319-48869-1_14","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"D Beyer","year":"2016","unstructured":"Beyer, D., Dangl, M.: SMT-based software model checking: an experimental comparison of four algorithms. In: Blazy, S., Chechik, M. (eds.) VSTTE 2016. LNCS, vol. 9971, pp. 181\u2013198. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48869-1_14"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"622","DOI":"10.1007\/978-3-319-21690-4_42","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2015","unstructured":"Beyer, D., Dangl, M., Wendler, P.: Boosting k-Induction with continuously-refined invariants. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 622\u2013640. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_42"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Beyer, D., et al.: Correctness witnesses: exchanging verification results between verifiers. In: FSE, pp. 326\u2013337 (2016)","DOI":"10.1145\/2950290.2950351"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-662-48288-9_9","volume-title":"Static Analysis","author":"M Brain","year":"2015","unstructured":"Brain, M., Joshi, S., Kroening, D., Schrammel, P.: Safety verification and refutation by k-invariants and k-induction. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 145\u2013161. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48288-9_9"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"510","DOI":"10.1007\/978-3-319-41540-6_29","volume-title":"Computer Aided Verification","author":"A Champion","year":"2016","unstructured":"Champion, A., Mebsout, A., Sticksel, C., Tinelli, C.: The Kind 2 model checker. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 510\u2013517. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_29"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-642-54862-8_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2014","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 46\u201361. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_4"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-28891-3_13","volume-title":"NASA Formal Methods","author":"D Cofer","year":"2012","unstructured":"Cofer, D., Gacek, A., Miller, S., Whalen, M.W., LaValley, B., Sha, L.: Compositional verification of architectural models. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 126\u2013140. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28891-3_13"},{"key":"3_CR11","unstructured":"E\u00e9n, N., et al.: Efficient implementation of property directed reachability. In: FMCAD (2011)"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-319-57288-8_30","volume-title":"NASA Formal Methods","author":"AW Fifarek","year":"2017","unstructured":"Fifarek, A.W., Wagner, L.G., Hoffman, J.A., Rodes, B.D., Aiello, M.A., Davis, J.A.: SpeAR v2.0: formalized past LTL specification and analysis of requirements. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 420\u2013426. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-57288-8_30"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Ghassabani, E., et al.: Efficient generation of all minimal inductive validity cores. In: FMCAD (2017)","DOI":"10.23919\/FMCAD.2017.8102238"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Ghassabani, E., et al.: Efficient generation of inductive validity cores for safety properties. In: FSE (2016)","DOI":"10.1145\/2950290.2950346"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Ghassabani, E., et al.: Proof-based coverage metrics for formal verification. In: ASE (2017)","DOI":"10.1109\/ASE.2017.8115632"},{"key":"3_CR16","first-page":"67","volume":"119","author":"A Groce","year":"2005","unstructured":"Groce, A., Kroening, D.: Making the most of BMC counterexamples. Proc. BMC 2004 ENTCS 119, 67\u201381 (2005)","journal-title":"Proc. BMC 2004 ENTCS"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., et al.: The synchronous dataflow programming language Lustre. IEEE (1991)","DOI":"10.1109\/5.97300"},{"key":"3_CR18","unstructured":"Hanna, Z., et al.: Formal verification coverage metrics for circuit design properties (2015). https:\/\/www.google.com\/patents\/US20150135150"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-31612-8_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"K Hoder","year":"2012","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157\u2013171. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_13"},{"key":"3_CR20","unstructured":"Kahsai, T., Bourbouh, H.: Zustre product home page. https:\/\/github.com\/coco-team\/zustre"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Kahsai, T., Tinelli, C.: PKIND: a parallel k-induction based model checker. In: PDMC (2011)","DOI":"10.4204\/EPTCS.72.6"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-642-28891-3_35","volume-title":"NASA Formal Methods","author":"T Kahsai","year":"2012","unstructured":"Kahsai, T., Garoche, P.-L., Tinelli, C., Whalen, M.: Incremental verification with mode variable invariants in state machines. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 388\u2013402. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28891-3_35"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Murugesan, A., et al.: Compositional verification of a medical device system. In: HILT (2013)","DOI":"10.1145\/2527269.2527272"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-540-24730-2_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Ravi","year":"2004","unstructured":"Ravi, K., Somenzi, F.: Minimal assignments for bounded model checking. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 31\u201345. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_3"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Rocha, H., et al.: Model checking embedded C software using k-induction and invariants. In: SBESC (2015)","DOI":"10.1109\/SBESC.2015.24"},{"key":"3_CR26","unstructured":"RTCA DO-178C: Software Considerations in Airborne Systems and Equipment Certification (2011)"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Wagner, L., et al.: SIMPAL: a compositional reasoning framework for imperative programs. In: SPIN (2017)","DOI":"10.1145\/3092282.3092290"},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Whalen, M.W., et al.: Coverage metrics for requirements-based testing. In: ISSTA (2006)","DOI":"10.1145\/1146238.1146242"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96142-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T23:20:25Z","timestamp":1571613625000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96142-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319961415","9783319961422"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96142-2_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}