{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T21:18:32Z","timestamp":1725743912933},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642392764"},{"type":"electronic","value":"9783642392771"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39277-1_6","type":"book-chapter","created":{"date-parts":[[2013,8,3]],"date-time":"2013-08-03T02:46:58Z","timestamp":1375498018000},"page":"71-86","source":"Crossref","is-referenced-by-count":1,"title":["Abstract Model Checking with SOFL Hierarchy"],"prefix":"10.1007","author":[{"given":"Cong","family":"Tian","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shaoying","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J.P. Quielle","year":"1982","unstructured":"Quielle, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol.\u00a0137, pp. 337\u2013351. Springer, Heidelberg (1982)"},{"key":"6_CR3","unstructured":"Clarke, E.M., Grumber, O., Peled, D.: Model Checking. MIT Press (2000)"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv.\u00a041(4) (2009)","DOI":"10.1145\/1592434.1592438"},{"issue":"5-6","key":"6_CR5","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. Software Tools for Technology Transfer\u00a09(5-6), 505\u2013525 (2007)","journal-title":"Software Tools for Technology Transfer"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C., Robby, L.S., Zheng, H.: Bandera: Extracting finite-state models from Java source code. In: ICSE 2000: Software Engineering, pp. 439\u2013448 (2000)","DOI":"10.1145\/337180.337234"},{"issue":"4","key":"6_CR7","first-page":"72","volume":"2","author":"K. Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking Java programs using Java Pathfinder. Software Tools for Technology Transfer (STTT)\u00a02(4), 72\u201384 (2000)","journal-title":"Software Tools for Technology Transfer (STTT)"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"issue":"7","key":"6_CR9","doi-asserted-by":"publisher","first-page":"1113","DOI":"10.1109\/TCAD.2004.829807","volume":"23","author":"E.M. Clarke","year":"2004","unstructured":"Clarke, E.M., Gupta, A., Strichman, O.: SAT Based Counterexample-Guided Abstraction-Refinement. IEEE Trans. Computer Aided Design\u00a023(7), 1113\u20131123 (2004)","journal-title":"IEEE Trans. Computer Aided Design"},{"issue":"5","key":"6_CR10","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E. Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement for Symbolic Model Checking. J. ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/3-540-48683-6_38","volume-title":"Computer Aided Verification","author":"H. Sa\u00efdi","year":"1999","unstructured":"Sa\u00efdi, H., Shankar, N.: Abstract and model check while you prove. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 443\u2013454. Springer, Heidelberg (1999)"},{"key":"6_CR12","unstructured":"Dwyer, M.B., Hatcliff, J.: Slicing Software for Model Construction. In: PEPM 1999, pp. 105\u2013118 (1999)"},{"issue":"2","key":"6_CR13","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1006\/inco.1994.1035","volume":"110","author":"P. Godefroid","year":"1994","unstructured":"Godefroid, P., Wolper, P.: A Partial Approach to Model Checking. Inf. Comput.\u00a0110(2), 305\u2013326 (1994)","journal-title":"Inf. Comput."},{"key":"6_CR14","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic Model Checking: 1020 States and Beyond. In: LICS 1990, pp. 428\u2013439 (1990)"},{"key":"6_CR15","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A. Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Advances in Computers\u00a058, 118\u2013149 (2003)","journal-title":"Advances in Computers"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/978-3-642-22685-4_36","volume-title":"Computing and Combinatorics","author":"C. Tian","year":"2011","unstructured":"Tian, C., Duan, Z.: Making Abstraction-Refinement Efficient in Model Checking. In: Fu, B., Du, D.-Z. (eds.) COCOON 2011. LNCS, vol.\u00a06842, pp. 402\u2013413. Springer, Heidelberg (2011)"},{"issue":"1","key":"6_CR17","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1109\/TC.2009.105","volume":"59","author":"F. He","year":"2010","unstructured":"He, F., Song, X., Hung, W.N.N., Gu, M., Sun, J.: Integrating Evolutionary Computation with Abstraction Refinement for Model Checking. IEEE Trans. Computers\u00a059(1), 116\u2013126 (2010)","journal-title":"IEEE Trans. Computers"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/11576280_29","volume-title":"Formal Methods and Software Engineering","author":"S. Liu","year":"2005","unstructured":"Liu, S., Nagoya, F., Chen, Y., Goya, M., McDermid, J.A.: An Automated Approach to Specification-Based Program Inspection. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol.\u00a03785, pp. 421\u2013434. Springer, Heidelberg (2005)"},{"key":"6_CR19","unstructured":"Liu, S.: Formal Engineering for Industrial Software Development Using the SOFL Method. Springer, Berlin, ISBN 3-540-20602-7"},{"issue":"4","key":"6_CR20","doi-asserted-by":"publisher","first-page":"667","DOI":"10.1109\/TR.2010.2085571","volume":"59","author":"S. Liu","year":"2010","unstructured":"Liu, S., McDermid, J.A., Chen, Y.: A Rigorous Method for Inspection of Model-Based Formal Specifications. IEEE Transactions on Reliability\u00a059(4), 667\u2013684 (2010)","journal-title":"IEEE Transactions on Reliability"},{"issue":"5","key":"6_CR21","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The Model Checker Spin. IEEE Trans. on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. on Software Engineering"},{"key":"6_CR22","first-page":"46","volume-title":"Proceedings of the 18th IEEE Symposium on Foundations of Computer Science","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46\u201367. IEEE, New York (1977)"},{"key":"6_CR23","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1002\/malq.19630090502","volume":"9","author":"S.A. Kripke","year":"1963","unstructured":"Kripke, S.A.: Semantical analysis of modal logic I: Normal propositional calculi. Z. Math. Logik Grund. Math.\u00a09, 67\u201396 (1963)","journal-title":"Z. Math. Logik Grund. Math."},{"issue":"7","key":"6_CR24","doi-asserted-by":"publisher","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","volume":"27","author":"V. D\u2019Silva","year":"2008","unstructured":"D\u2019Silva, V., Kroening, D., Weissenbacher, G.: A Survey of Automated Techniques for Formal Software Verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a027(7), 1165\u20131178 (2008), doi:10.1109\/TCAD.2008.923410","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"}],"container-title":["Lecture Notes in Computer Science","Structured Object-Oriented Formal Language and Method"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39277-1_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T10:29:46Z","timestamp":1558002586000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39277-1_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642392764","9783642392771"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39277-1_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}