{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,25]],"date-time":"2026-10-25T21:47:45Z","timestamp":1792964865975,"version":"4.5.0"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642317583","type":"print"},{"value":"9783642317590","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31759-0_7","type":"book-chapter","created":{"date-parts":[[2012,7,19]],"date-time":"2012-07-19T00:59:50Z","timestamp":1342659590000},"page":"62-79","source":"Crossref","is-referenced-by-count":1,"title":["A Compositional Minimization Approach for Large Asynchronous Design Verification"],"prefix":"10.1007","author":[{"given":"Hao","family":"Zheng","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Emmanuel","family":"Rodriguez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yingying","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Chris","family":"Myers","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"548","DOI":"10.1007\/11513988_52","volume-title":"Computer Aided Verification","author":"R. Alur","year":"2005","unstructured":"Alur, R., Madhusudan, P., Nam, W.: Symbolic Compositional Verification by Learning Assumptions. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 548\u2013562. Springer, Heidelberg (2005)"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/3-540-49213-5_4","volume-title":"Compositionality: The Significant Difference","author":"S. Berezin","year":"1998","unstructured":"Berezin, S., Campos, S., Clarke, E.M.: Compositional Reasoning in Model Checking. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol.\u00a01536, pp. 81\u2013102. Springer, Heidelberg (1998)"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-540-70545-1_14","volume-title":"Computer Aided Verification","author":"M. Gheorghiu Bobaru","year":"2008","unstructured":"Gheorghiu Bobaru, M., P\u0103s\u0103reanu, C.S., Giannakopoulou, D.: Automated Assume-Guarantee Reasoning by Abstraction Refinement. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 135\u2013148. Springer, Heidelberg (2008)"},{"key":"7_CR4","unstructured":"Bustan, D., Grumberg, O.: Modular minimization of deterministic finite-state machines. In: Proceedings the 6th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2001 (July 2001)"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"534","DOI":"10.1007\/11513988_51","volume-title":"Computer Aided Verification","author":"S. Chaki","year":"2005","unstructured":"Chaki, S., Clarke, E., Sinha, N., Thati, P.: Automated Assume-Guarantee Reasoning for Simulation Conformance. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 534\u2013547. Springer, Heidelberg (2005)"},{"issue":"4","key":"7_CR6","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1145\/235321.235323","volume":"5","author":"S. Cheung","year":"1996","unstructured":"Cheung, S., Kramer, J.: Context constraints for compositional reachability analysis. ACM Transations on Software Engineering and Methodology\u00a05(4), 334\u2013377 (1996)","journal-title":"ACM Transations on Software Engineering and Methodology"},{"issue":"1","key":"7_CR7","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1145\/295558.295570","volume":"8","author":"S. Cheung","year":"1999","unstructured":"Cheung, S., Kramer, J.: Checking safety properties using compositional reachability analysis. ACM Trans. Softw. Eng. Methodol.\u00a08(1), 49\u201378 (1999)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"7_CR8","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1109\/LICS.1989.39190","volume-title":"Proceedings of the 4th Annual Symposium on Logic in Computer Science","author":"E. Clarke","year":"1989","unstructured":"Clarke, E., Long, D., McMillan, K.: Compositional model checking. In: Proceedings of the 4th Annual Symposium on Logic in Computer Science, pp. 353\u2013362. IEEE Press, Piscataway (1989)"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-36577-X_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.M. Cobleigh","year":"2003","unstructured":"Cobleigh, J.M., Giannakopoulou, D., P\u0103s\u0103reanu, C.S.: Learning Assumptions for Compositional Verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 331\u2013346. Springer, Heidelberg (2003)"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Dill, D.: Trace Theory for Automatic Hierarchical Verification of Speed Independent Circuits. PhD thesis, Carnegie Mellon University (1988)","DOI":"10.7551\/mitpress\/6874.001.0001"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., P\u01cesare\u01cenu, C.S., Barringer, H.: Component verification with automatically generated assumptions. Automated Software Engineering, 297\u2013320 (2005)","DOI":"10.1007\/s10515-005-2641-y"},{"issue":"5","key":"7_CR12","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1007\/BF01211911","volume":"8","author":"S. Graf","year":"1996","unstructured":"Graf, S., Steffen, B., Luttgen, G.: Compositional minimization of finite state systems using interface specifications. Formal Aspects of Computation\u00a08(5), 607\u2013616 (1996)","journal-title":"Formal Aspects of Computation"},{"issue":"3","key":"7_CR13","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"Grumberg, O., Long, D.: Model checking and modular verification. ACM Transactions on Programming Languages and Systems\u00a016(3), 843\u2013871 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/BFb0028765","volume-title":"Computer Aided Verification","author":"T. Henzinger","year":"1998","unstructured":"Henzinger, T., Qadeer, S., Rajamani, S.: You Assume, we Guarantee: Methodology and Case Studies. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 440\u2013451. Springer, Heidelberg (1998)"},{"key":"7_CR15","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/978-0-387-34878-0_13","volume-title":"Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques VII","author":"G.J. Holzmann","year":"1995","unstructured":"Holzmann, G.J., Peled, D.: An improvement in formal verification. In: Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques VII, pp. 197\u2013211. Chapman & Hall, Ltd., London (1995)"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/BFb0035392","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Krimm","year":"1997","unstructured":"Krimm, J., Mounier, L.: Compositional State Space Generation from Lotos Programs. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol.\u00a01217, pp. 239\u2013258. Springer, Heidelberg (1997)"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Martin, A.J.: Self-timed fifo: An exercise in compiling programs into vlsi circuits. Technical Report 1986.5211-tr-86, California Institute of Technology (1986)","DOI":"10.21236\/ADA442970"},{"key":"7_CR18","unstructured":"Mcmillan, K.L.: A methodology for hardware verification using compositional model checking. Technical report, Cadence Berkeley Labs (1999)"},{"key":"7_CR19","unstructured":"Myers, C.J.: Computer-Aided Synthesis and Verification of Gate-Level Timed Circuits. PhD thesis, Stanford University (1995)"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/11901914_15","volume-title":"Automated Technology for Verification and Analysis","author":"W. Nam","year":"2006","unstructured":"Nam, W., Alur, R.: Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol.\u00a04218, pp. 170\u2013185. Springer, Heidelberg (2006)"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Stevens, K., Ginosar, R., Rotem, S.: Relative timing. In: Proc. International Symposium on Advanced Research in Asynchronous Circuits and Systems, pp. 208\u2013218 (1999)","DOI":"10.1109\/ASYNC.1999.761535"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Thacker, R.A., Jones, K.R., Myers, C.J., Zheng, H.: Automatic abstraction for verification of cyber-physical systems. In: Proceedings of the 1st ACM\/IEEE International Conference on Cyber-Physical Systems, ICCPS 2010, pp. 12\u201321 (2010)","DOI":"10.1145\/1795194.1795197"},{"issue":"3","key":"7_CR23","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1109\/TCAD.2009.2012531","volume":"28","author":"H. Yao","year":"2009","unstructured":"Yao, H., Zheng, H.: Automated interface refinement for compositional verification. IEEE Transaction on Computer-Aided Design of Integrated Circuits and Systems\u00a028(3), 433\u2013446 (2009)","journal-title":"IEEE Transaction on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"7_CR24","unstructured":"Yoneda, T., Yoshikawa, T.: Using partial orders for trace theoretic verification of asynchronous circuits. In: Proc. International Symposium on Advanced Research in Asynchronous Circuits and Systems. IEEE Computer Society Press (March 1996)"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Zheng, H.: Compositional reachability analysis for efficient modular verification of asynchronous designs. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a029(3) (March 2010)","DOI":"10.1109\/TCAD.2009.2035544"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Zheng, H., Ahrens, J., Xia, T.: A compositional method with failure-preserving abstractions for asynchronous design verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a027 (2008)","DOI":"10.1109\/TCAD.2008.923104"},{"issue":"9","key":"7_CR27","doi-asserted-by":"publisher","first-page":"1138","DOI":"10.1109\/TCAD.2003.816214","volume":"22","author":"H. Zheng","year":"2003","unstructured":"Zheng, H., Mercer, E., Myers, C.: Modular verification of timed circuits using automatic abstraction. IEEE Transactions on Computer-Aided Design\u00a022(9), 1138\u20131153 (2003)","journal-title":"IEEE Transactions on Computer-Aided Design"},{"issue":"3","key":"7_CR28","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1109\/TCAD.2005.854638","volume":"25","author":"H. Zheng","year":"2006","unstructured":"Zheng, H., Myers, C., Walter, D., Little, S., Yoneda, T.: Verification of timed circuits with failure directed abstractions. IEEE Transactions on Computer-Aided Design\u00a025(3), 403\u2013412 (2006)","journal-title":"IEEE Transactions on Computer-Aided Design"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31759-0_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,4]],"date-time":"2025-04-04T21:08:24Z","timestamp":1743800904000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31759-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642317583","9783642317590"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31759-0_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}