{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:44:53Z","timestamp":1754487893707},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540631668"},{"type":"electronic","value":"9783540691952"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63166-6_5","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:14:20Z","timestamp":1330280060000},"page":"12-23","source":"Crossref","is-referenced-by-count":14,"title":["Automatic abstraction techniques for propositional \u03bc-calculus model checking"],"prefix":"10.1007","author":[{"given":"Abelardo","family":"Pardo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gary D.","family":"Hachtel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"5_CR1","series-title":"LNCS 697","volume-title":"An iterative approach to language containment","author":"F. Balarin","year":"1993","unstructured":"F. Balarin and A. L. Sangiovanni-Vincentelli. An iterative approach to language containment. In C. Courcoubetis, editor, Fifth Conference on Computer Aided Verification (CAV '93). Springer-Verlag, Berlin, 1993. LNCS 697."},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"R. K. Brayton et al. VIS: A system for verification and synthesis. In T. Henzinger and R. Alur, editors, Eigth Conference on Computer Aided Verification (CAV'96), pages 428\u2013432. Springer-Verlag, Rutgers University, 1996. LNCS 1102.","DOI":"10.1007\/3-540-61474-5_95"},{"issue":"8","key":"5_CR3","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677\u2013691, Aug. 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. M. Clarke, and D. E. Long. Representing circuits more efficiently in symbolic model checking. In Proceedings of the Design Automation Conference, pages 403\u2013407, San Francisco, CA, June 1991.","DOI":"10.1145\/127601.127702"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill. Sequential circuit verification using symbolic model checking. In Proceedings of the Design Automation Conference, pages 46\u201351, June 1990.","DOI":"10.1145\/123186.123223"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"H. Cho, G. D. Hachtel, E. Macii, B. Plessier, and F. Somenzi. Algorithms for approximate FSM traversal based on state space decomposition. In Proceedings of the Design Automation Conference, pages 25\u201330, Dallas, TX, June 1993.","DOI":"10.1145\/157485.164555"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by constructions or approximation of fixpoints. In Proceedings of the ACM Symposium on the Principles of Programming Languages, pages 238\u2013250, 1977.","DOI":"10.1145\/512950.512973"},{"key":"5_CR8","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/0304-3975(94)90269-0","volume":"126","author":"M. Dam","year":"1994","unstructured":"M. Dam. CTL* and ECTL* as fragments of the modal \u03bc-calculus. Theoretical Computer Science, 126: 77\u201397, 1994.","journal-title":"Theoretical Computer Science"},{"key":"5_CR9","unstructured":"E. A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional mu-calculus. In Proceedings of the First Annual Symposium of Logic in Computer Science, pages 267\u2013278, June 1986."},{"key":"5_CR10","series-title":"LNCS 818","first-page":"299","volume-title":"Efficient model checking by automated ordering of transition relation parititons","author":"D. Geist","year":"1994","unstructured":"D. Geist and I. Beer. Efficient model checking by automated ordering of transition relation parititons. In D. L. Dill, editor, Sixth Conference on Computer Aided Verification (CAV'94), pages 299\u2013310, Berlin, 1994. Springer-Verlag. LNCS 818."},{"key":"5_CR11","unstructured":"P. Kelb, D. Dams, and R. Gerth. Practical symbolic model checking of the full \u03bc-calculus using compositional abstractions. Technical Report 95-31, Department of Computing Science, Eindhoven University of Technology, 1995."},{"key":"5_CR12","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"D. Kozen. Results on the propositional \u03bc-calculus. Theoretical Computer Science, 27:333\u2013354, 1983.","journal-title":"Theoretical Computer Science"},{"key":"5_CR13","volume-title":"Computer-Aided Verification of Coordinating Processes","author":"R. P. Kurshan","year":"1994","unstructured":"R. P. Kurshan. Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton, NJ, 1994."},{"key":"5_CR14","unstructured":"W. Lee, A. Pardo, J. Jang, G. Hachtel, and F. Somenzi. Tearing based abstraction for CTL model checking. In Proceedings of the IEEE International Conference on Computer Aided Design, pages 76\u201381, 1996."},{"key":"5_CR15","unstructured":"D. E. Long. Model Checking, Abstraction, and Compositional Verification. PhD thesis, Carnegie-Mellon University, July 1993."},{"key":"5_CR16","volume-title":"Symbolic Model Checking","author":"K. L. McMillan","year":"1994","unstructured":"K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA, 1994."},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"C. Pixley, S.-W. Jeong, and G. D. Hachtel. Exact calculation of synchronization sequences based on binary decision diagrams. In Proceedings of the Design Automation Conference, pages 620\u2013623, Anaheim, CA, June 1992.","DOI":"10.1109\/DAC.1992.227811"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63166-6_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:16:49Z","timestamp":1605629809000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63166-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631668","9783540691952"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-63166-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}