{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T10:33:18Z","timestamp":1790073198060,"version":"4.0.1"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642288906","type":"print"},{"value":"9783642288913","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28891-3_35","type":"book-chapter","created":{"date-parts":[[2012,3,30]],"date-time":"2012-03-30T12:53:01Z","timestamp":1333111981000},"page":"388-402","source":"Crossref","is-referenced-by-count":10,"title":["Incremental Verification with Mode Variable Invariants in State Machines"],"prefix":"10.1007","author":[{"given":"Temesghen","family":"Kahsai","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pierre-Lo\u00efc","family":"Garoche","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mike","family":"Whalen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"12","key":"35_CR1","doi-asserted-by":"crossref","first-page":"1056","DOI":"10.1109\/TSE.2005.138","volume":"31","author":"C. Damas","year":"2005","unstructured":"Damas, C., Lambeau, B., Dupont, P., van Lamsweerde, A.: Generating annotated behavior models from end-user scenarios. IEEE Transactions on SE\u00a031(12), 1056\u20131073 (2005)","journal-title":"IEEE Transactions on SE"},{"key":"35_CR2","doi-asserted-by":"crossref","unstructured":"Damas, C., Lambeau, B., Roucoux, F., van Lamsweerde, A.: Analyzing critical process models through behavior model synthesis. In: ICSE 2009, pp. 441\u2013451. IEEE (2009)","DOI":"10.1109\/ICSE.2009.5070543"},{"key":"35_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/978-3-540-45069-6_2","volume-title":"Computer Aided Verification","author":"L. Moura de","year":"2003","unstructured":"de Moura, L., Rue\u00df, H., Sorea, M.: Bounded Model Checking and Induction: From Refutation to Verification. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 14\u201326. Springer, Heidelberg (2003)"},{"issue":"10","key":"35_CR4","doi-asserted-by":"crossref","first-page":"898","DOI":"10.1109\/TSE.2003.1237171","volume":"29","author":"A. Gurfinkel","year":"2003","unstructured":"Gurfinkel, A., Chechik, M., Devereux, B.: Temporal logic query checking: a tool for model exploration. IEEE Transactions on SE\u00a029(10), 898\u2013914 (2003)","journal-title":"IEEE Transactions on SE"},{"key":"35_CR5","first-page":"1","volume-title":"FMCAD 2008","author":"G. Hagen","year":"2008","unstructured":"Hagen, G., Tinelli, C.: Scaling up the formal verification of Lustre programs with SMT-based techniques. In: FMCAD 2008, pp. 1\u20139. IEEE Press, Piscataway (2008)"},{"issue":"9","key":"35_CR6","doi-asserted-by":"publisher","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N. Halbwachs","year":"1991","unstructured":"Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data-flow programming language Lustre. Proceedings of the IEEE\u00a079(9), 1305\u20131320 (1991)","journal-title":"Proceedings of the IEEE"},{"key":"35_CR7","doi-asserted-by":"crossref","unstructured":"Hangal, S., Narayanan, S., Chandra, N., Chakravorty, S.: IODINE: a tool to automatically infer dynamic invariants for hardware designs. In: DAC 2005, pp. 775\u2013778 (June 2005)","DOI":"10.1145\/1065579.1065786"},{"key":"35_CR8","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1145\/291252.288218","volume":"23","author":"R. Jeffords","year":"1998","unstructured":"Jeffords, R., Heitmeyer, C.: Automatic generation of state invariants from requirements specifications. SIGSOFT Softw. Eng. Notes\u00a023, 56\u201369 (1998)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"35_CR9","doi-asserted-by":"crossref","unstructured":"Jeffords, R., Heitmeyer, C.: An algorithm for strengthening state invariants generated from requirements specifications. In: RE 2001, pp. 182\u2013191 (2001)","DOI":"10.1109\/ISRE.2001.948558"},{"key":"35_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/978-3-642-20398-5_15","volume-title":"NASA Formal Methods","author":"T. Kahsai","year":"2011","unstructured":"Kahsai, T., Ge, Y., Tinelli, C.: Instantiation-Based Invariant Discovery. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 192\u2013206. Springer, Heidelberg (2011)"},{"key":"35_CR11","doi-asserted-by":"crossref","unstructured":"Kahsai, T., Tinelli, C.: PKIND: a parallel k-induction based model checker. In: PDMC 2011. EPTCS, vol.\u00a072, pp. 55\u201362 (2011)","DOI":"10.4204\/EPTCS.72.6"},{"key":"35_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/11678779_5","volume-title":"Hardware and Software, Verification and Testing","author":"Z. Khasidashvili","year":"2006","unstructured":"Khasidashvili, Z., Nadel, A., Palti, A., Hanna, Z.: Simultaneous SAT-Based Model Checking of Safety Properties. In: Ur, S., Bin, E., Wolfsthal, Y. (eds.) HVC 2005. LNCS, vol.\u00a03875, pp. 56\u201375. Springer, Heidelberg (2006)"},{"key":"35_CR13","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer (1995)","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"35_CR14","unstructured":"Sampson, M., Derevenko, V.: Interface definition document (IDD) for international space station (ISS) visiting vehicles (VVs). Technical report, NASA (2000)"},{"key":"35_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","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: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 108\u2013125. Springer, Heidelberg (2000)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28891-3_35.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,24]],"date-time":"2025-03-24T13:58:10Z","timestamp":1742824690000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28891-3_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288906","9783642288913"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28891-3_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}