{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T23:10:10Z","timestamp":1737501010806,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540766483"},{"type":"electronic","value":"9783540766506"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-76650-6_12","type":"book-chapter","created":{"date-parts":[[2007,10,26]],"date-time":"2007-10-26T07:12:49Z","timestamp":1193382769000},"page":"191-211","source":"Crossref","is-referenced-by-count":2,"title":["Model Checking with SAT-Based Characterization of ACTL Formulas"],"prefix":"10.1007","author":[{"given":"Wenhui","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","volume-title":"Bounded Model Checking. Advances in Computers 58","author":"A. Biere","year":"2003","unstructured":"Biere, A., Cimmatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded Model Checking. Advances in Computers 58. Academic Press, London (2003)"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimmatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, J.: Symbolic model checking: 1020 states and beyond. In: LICS 1990, pp. 428\u2013439 (1990)","DOI":"10.1109\/LICS.1990.113767"},{"issue":"8","key":"12_CR4","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. Bryant","year":"1986","unstructured":"Bryant, R.: Graph based algorithms for boolean function manipulation. IEEE Transaction on Computers\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Transaction on Computers"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Bryant, R.: Binary decision diagrams and beyond: enabling technologies for formal verification. In: CAD 1995, pp. 236\u2013243 (1995)","DOI":"10.1109\/ICCAD.1995.480018"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1981","unstructured":"Clarke, E.M., Emerson, E.A.: Synthesis of synchronization skeletons for branching time temporal logic. In: Kozen, D. (ed.) Logics of Programs. LNCS, vol.\u00a0131, Springer, Heidelberg (1981)"},{"issue":"2","key":"12_CR7","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Jha, S., Lu, Y., Veith, H.: Tree-Like Counterexamples in Model Checking. In: LICS 2002, pp. 19\u201329 (2002)","DOI":"10.1109\/LICS.2002.1029814"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Das, S., Dill, D.L.: Successive Approximation of Abstract Transition Relations. In: LICS 2001, pp. 51\u201360 (2001)","DOI":"10.1109\/LICS.2001.932482"},{"issue":"3","key":"12_CR10","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E.A. Emerson","year":"1982","unstructured":"Emerson, E.A., Clarke, E.M.: Using Branching-time Temporal Logics to Synthesize Synchronization Skeletons. Science of Computer Programming\u00a02(3), 241\u2013266 (1982)","journal-title":"Science of Computer Programming"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","first-page":"442","volume-title":"Software Engineering Education in the Modern Age","author":"M.F. Frias","year":"2006","unstructured":"Frias, M.F., Galeotti, J.P., Pombo, C.L., Aguirre, N.: DynAlloy: upgrading alloy with actions. In: Inverardi, P., Jazayeri, M. (eds.) ICSE 2005. LNCS, vol.\u00a04309, pp. 442\u2013451. Springer, Heidelberg (2006)"},{"issue":"4","key":"12_CR12","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1145\/1101815.1101819","volume":"14","author":"M.F. Frias","year":"2005","unstructured":"Frias, M.F., Pombo, C.L., Baum, G.A., Aguirre, N., Maibaum, T.S.E.: Reasoning about static and dynamic properties in alloy: A purely relational approach. ACM Trans. Softw. Eng. Methodol.\u00a014(4), 478\u2013526 (2005)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/3-540-36384-X_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Kroening","year":"2002","unstructured":"Kroening, D., Strichman, O.: Efficient Computation of Recurrence Diameters. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 298\u2013309. Springer, Heidelberg (2002)"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"CAV 2003","author":"R. Jhala","year":"2003","unstructured":"Jhala, R., McMillan, K.L.: McMillan. Interpolation and SAT-Based Model Checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"12_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: DAC 2001 (2001)","DOI":"10.1145\/378239.379017"},{"volume-title":"Software Reliability Methods","year":"2001","key":"12_CR17","unstructured":"Peled, D.A.: Software Reliability Methods. Springer, Heidelberg (2001)"},{"key":"12_CR18","first-page":"135","volume":"51","author":"W. Penczek","year":"2002","unstructured":"Penczek, W., Wozna, B., Zbrzezny, A.: Bounded Model Checking for the Universal Fragment of CTL. Fundamenta Informaticae\u00a051, 135\u2013156 (2002)","journal-title":"Fundamenta Informaticae"},{"issue":"2","key":"12_CR19","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/s10009-004-0183-4","volume":"7","author":"M.R. Prasad","year":"2005","unstructured":"Prasad, M.R., Biere, A., Gupta, A.: A survey of recent advances in SAT-based formal verification. STTT\u00a07(2), 156\u2013173 (2005)","journal-title":"STTT"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/978-3-540-45069-6_28","volume-title":"CAV 2003","author":"S. Shoham","year":"2003","unstructured":"Shoham, S., Grumberg, O.: A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 275\u2013287. Springer, Heidelberg (2003)"},{"key":"12_CR21","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., lmarck, G.S.: 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)"},{"key":"12_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"753","DOI":"10.1007\/3-540-58156-1_54","volume-title":"CADE-12","author":"J. Zhang","year":"1994","unstructured":"Zhang, J.: Problems on the generation of finite models. In: Bundy, A. (ed.) CADE-12. LNCS, vol.\u00a0814, pp. 753\u2013757. Springer, Heidelberg (1994)"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-540-70952-7_18","volume-title":"Formal Methods: Applications and Technology","author":"W. Zhang","year":"2007","unstructured":"Zhang, W.: SAT-based verification of LTL formulas. In: Brim, L., Haverkort, B., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol.\u00a04346, pp. 277\u2013292. Springer, Heidelberg (2007)"},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","volume-title":"EUROCAST 2007","author":"W. Zhang","year":"2007","unstructured":"Zhang, W.: Verification of ACTL properties by bounded model checking. In: Moreno Diaz, R., Pichler, F., Quesada Arencibia, A. (eds.) EUROCAST 2007. LNCS, vol.\u00a04739, Springer, Heidelberg (2007)"},{"key":"12_CR25","series-title":"Lecture Notes in Artificial Intelligence","first-page":"108","volume-title":"PRICAI 2002","author":"W. Zhang","year":"2002","unstructured":"Zhang, W., Huang, Z., Zhang, J.: Parallel Execution of Stochastic Search Procedures on Reduced SAT Instances. In: Ishizuka, M., Sattar, A. (eds.) PRICAI 2002. LNCS (LNAI), vol.\u00a02417, pp. 108\u2013117. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-76650-6_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T22:42:30Z","timestamp":1737499350000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-76650-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540766483","9783540766506"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-76650-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}