{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T09:05:45Z","timestamp":1726045545343},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030315139"},{"type":"electronic","value":"9783030315146"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-030-31514-6_5","type":"book-chapter","created":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T23:03:06Z","timestamp":1569193386000},"page":"57-72","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Invisible Invariants Are Neither"],"prefix":"10.1007","author":[{"given":"Lenore D.","family":"Zuck","sequence":"first","affiliation":[]},{"given":"Kenneth L.","family":"McMillan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,9,23]]},"reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/3-540-36576-1_6","volume-title":"Foundations of Software Science and Computation Structures","author":"A Pnueli","year":"2003","unstructured":"Pnueli, A., Zuck, L.: Parameterized verification by probabilistic abstraction. In: Gordon, A.D. (ed.) FoSSaCS 2003. LNCS, vol. 2620, pp. 87\u2013102. Springer, Heidelberg (2003). \n                      https:\/\/doi.org\/10.1007\/3-540-36576-1_6"},{"issue":"3","key":"5_CR2","doi-asserted-by":"publisher","first-page":"853","DOI":"10.1016\/j.jcss.2011.08.003","volume":"78","author":"I Balaban","year":"2012","unstructured":"Balaban, I., Pnueli, A., Sa\u2019ar, Y., Zuck, L.D.: Verification of multi-linked heaps. J. Comput. Syst. Sci. 78(3), 853\u2013876 (2012)","journal-title":"J. Comput. Syst. Sci."},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-540-30579-8_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"I Balaban","year":"2005","unstructured":"Balaban, I., Pnueli, A., Zuck, L.D.: Shape analysis by predicate abstraction. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 164\u2013180. Springer, Heidelberg (2005). \n                      https:\/\/doi.org\/10.1007\/978-3-540-30579-8_12"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-540-69738-1_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"I Balaban","year":"2007","unstructured":"Balaban, I., Pnueli, A., Zuck, L.D.: Shape analysis of single-parent heaps. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 91\u2013105. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-69738-1_7"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/11888116_26","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2006","author":"Y Fang","year":"2006","unstructured":"Fang, Y., McMillan, K.L., Pnueli, A., Zuck, L.D.: Liveness by invisible invariants. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 356\u2013371. Springer, Heidelberg (2006). \n                      https:\/\/doi.org\/10.1007\/11888116_26"},{"key":"5_CR6","volume-title":"Fact Fiction and Forecast","author":"N Goodman","year":"1983","unstructured":"Goodman, N.: Fact Fiction and Forecast, 4th edn. Harvard University Press, Cambridge (1983)","edition":"4"},{"key":"5_CR7","volume-title":"Treatise of Human Nature","author":"D Hume","year":"1888","unstructured":"Hume, D.: Treatise of Human Nature. Clarendon Press, Oxford (1888). Edited by L. A Selby Bigge. Originally published 1739\u20131740"},{"key":"5_CR8","unstructured":"Lahiri, S.K.: Ubounded system verification using decision procedure and predicate abstraction. Ph.D. thesis, Carnegie Mellon University (2004)"},{"issue":"2","key":"5_CR9","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"SE-3","author":"L. Lamport","year":"1977","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. SE-3, 2:125\u2013143, 3 (1977)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"5_CR10","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995). \n                      https:\/\/doi.org\/10.1007\/978-1-4612-4222-2"},{"key":"5_CR11","unstructured":"Mitchell, T.M.: The need for biases in learning generalizations, Technical report (1980)"},{"issue":"5","key":"5_CR12","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1145\/360051.360224","volume":"19","author":"Susan Owicki","year":"1976","unstructured":"Owicki, S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Commun. ACM 19(5), 279\u2013285, 5 (1976)","journal-title":"Communications of the ACM"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Pnueli","year":"2001","unstructured":"Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 82\u201397. Springer, Heidelberg (2001). \n                      https:\/\/doi.org\/10.1007\/3-540-45319-9_7"},{"key":"5_CR14","unstructured":"Pnueli, A., Zuck, L.D.: Probabilistic verification by tableaux. In: Proceedings of the Symposium on Logic in Computer Science (LICS 1986), Cambridge, Massachusetts, USA, 16\u201318 June 1986, pp. 322\u2013331 (1986)"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-540-24622-0_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T Reps","year":"2004","unstructured":"Reps, T., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 252\u2013266. Springer, Heidelberg (2004). \n                      https:\/\/doi.org\/10.1007\/978-3-540-24622-0_21"},{"key":"5_CR16","volume-title":"Artificial Intelligence: A Modern Approach","author":"SJ Russell","year":"2014","unstructured":"Russell, S.J., Norvig, P.: Artificial Intelligence: A Modern Approach, 3rd edn. Pearson Education Limited, London (2014)","edition":"3"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/3-540-47813-2_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L Zuck","year":"2002","unstructured":"Zuck, L., Pnueli, A., Kesten, Y.: Automatic verification of probabilistic free choice. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol. 2294, pp. 208\u2013224. Springer, Heidelberg (2002). \n                      https:\/\/doi.org\/10.1007\/3-540-47813-2_15"}],"container-title":["Lecture Notes in Computer Science","From Reactive Systems to Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-31514-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T23:26:48Z","timestamp":1569194808000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-31514-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030315139","9783030315146"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-31514-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"23 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}