{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T05:20:40Z","timestamp":1737609640603,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540671022"},{"type":"electronic","value":"9783540465621"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46562-6_41","type":"book-chapter","created":{"date-parts":[[2007,11,14]],"date-time":"2007-11-14T00:12:56Z","timestamp":1194999176000},"page":"460-469","source":"Crossref","is-referenced-by-count":0,"title":["Experiences with the Application of Symbolic Model Checking to the Analysis of Software Specifications"],"prefix":"10.1007","author":[{"given":"Richard J.","family":"Anderson","sequence":"first","affiliation":[]},{"given":"Paul","family":"Beame","sequence":"additional","affiliation":[]},{"given":"William","family":"Chan","sequence":"additional","affiliation":[]},{"given":"David","family":"Notkin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2000,1,28]]},"reference":[{"issue":"1","key":"41_CR1","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/32.210305","volume":"19","author":"J. M. Atlee","year":"1993","unstructured":"J. M. Atlee and J. Gannon. State-based model checking of event-driven system requirements. IEEE Transactions on Software Engineering, 19(1):24\u201340, January 1993.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"6","key":"41_CR2","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 35(6):677\u2013691, August 1986.","journal-title":"IEEE Transactions on Computers"},{"issue":"2","key":"41_CR3","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1109\/12.73590","volume":"40","author":"R. E. Bryant","year":"1991","unstructured":"R. E. Bryant. On the complexity of VLSI implementations and graph representation of boolean functions with applications to integer multiplication. IEEE Transactions on Computers, 40(2):205\u2013213, February 1991.","journal-title":"IEEE Transactions on Computers"},{"issue":"4","key":"41_CR4","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"J. R. Burch","year":"1994","unstructured":"J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits, 13(4):401\u2013424, April 1994.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits"},{"issue":"7","key":"41_CR5","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1109\/32.708566","volume":"24","author":"W. Chan","year":"1998","unstructured":"W. Chan, R. J. Anderson, P. Beame, S. Burns, F. Modugno, D. Notkin, and J. D. Reese. Model checking large software specifications. IEEE Transactions on Software Engineering, 24(7):498\u2013520, July 1998.","journal-title":"IEEE Transactions on Software Engineering"},{"doi-asserted-by":"crossref","unstructured":"W. Chan, R. J. Anderson, P. Beame, D. H. Jones, D. Notkin, and W. E. Warner. Decoupling synchronization from logic for efficient symbolic model checking of statecharts. In Proceedings of the 1999 International Conference on Software Engineering: ICSE 99, Los Angeles, USA, May 1999. To appear.","key":"41_CR6","DOI":"10.1145\/302405.302460"},{"key":"41_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"316","DOI":"10.1007\/3-540-63166-6_32","volume-title":"Computer Aided Verification, 9th International Conference, CAV\u201997 Proceedings","author":"W. Chan","year":"1997","unstructured":"W. Chan, R. J. Anderson, P. Beame, and D. Notkin. Combining constraint solving and symbolic model checking for a class of systems with non-linear constraints. In O. Grumberg, editor, Computer Aided Verification, 9th International Conference, CAV\u201997 Proceedings, volume 1254 of Lecture Notes in Computer Science, pages 316\u2013327, Haifa, Israel, June 1997. Springer-Verlag."},{"doi-asserted-by":"crossref","unstructured":"W. Chan, R. J. Anderson, P. Beame, and D. Notkin. Improving efficiency of symbolic model checking for state-based system requirements. In M. Young, editor, ISSTA 98: Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 102\u2013112, Clearwater Beach, Florida, USA, March 1998. Published as Software Engineering Notes, 23(2).","key":"41_CR8","DOI":"10.1145\/271771.271798"},{"issue":"2","key":"41_CR9","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, April 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"unstructured":"J. Crow and B. L. Di Vito. Formalizing space shuttle software requirements. In Proceedings of the ACM SIGSOFT Workshop on Formal Methods in Software Practice, pages 40\u201348, January 1996.","key":"41_CR10"},{"issue":"3","key":"41_CR11","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(3):231\u2013274, June 1987.","journal-title":"Science of Computer Programming"},{"issue":"4","key":"41_CR12","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/235321.235322","volume":"5","author":"D. Harel","year":"1996","unstructured":"D. Harel and A. Naamad. The STATEMATE semantics of statecharts. ACM Transactions on Software Engineering and Methodology, 5(4):293\u2013333, October 1996.","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"unstructured":"D. Harel, A. Pnueli, J. P. Schmidt, and R. Sherman. On the formal semantics of statecharts (extended abstract). In Proceedings: Symposium on Logic in Computer Science, pages 54\u201364, Ithaca, New York, USA, June 1987. IEEE.","key":"41_CR13"},{"doi-asserted-by":"crossref","unstructured":"J. Helbig and P. Kelb. An OBDD-representation of statecharts. In Proceedings: The European Design and Test Conference. EDAC, The European Conference on Design Automation. ETC, European Test Conference. EUROASIC, The European Event in ASIC Design, pages 142\u2013149, Paris, France, February\/March 1994. IEEE.","key":"41_CR14","DOI":"10.1109\/EDTC.1994.326884"},{"issue":"3","key":"41_CR15","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1109\/32.75414","volume":"17","author":"M. S. Jaffe","year":"1991","unstructured":"M. S. Jaffe, N. G. Leveson, M. P. E. Heimdahl, and B. E. Melhart. Software requirements analysis for real-time process-control systems. IEEE Transactions on Software Engineering, 17(3):241\u2013258, March 1991.","journal-title":"IEEE Transactions on Software Engineering"},{"doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","key":"41_CR16","DOI":"10.1007\/978-1-4615-3190-6"},{"doi-asserted-by":"crossref","unstructured":"C._R. Nobe and W. E. Warner. Lessons learned from a trial application of requirements modeling using statecharts. In Proceedings of the 2nd International Conference on Requirements Engineering, pages 86\u201393, Colorado Springs, USA, April 1996. IEEE.","key":"41_CR17","DOI":"10.1109\/ICRE.1996.491433"},{"key":"41_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1007\/3-540-54415-1_49","volume-title":"Theoretical Aspects of Computer Software, International Conference TACS\u201991","author":"A. Pnueli","year":"1991","unstructured":"A. Pnueli and M. Shalev. What is in a step: On the semantics of statecharts. In T. Ito and A. R. Meyer, editors, Theoretical Aspects of Computer Software, International Conference TACS\u201991, volume 526 of Lecture Notes in Computer Science, pages 244\u2013264, Sendai, Japan, September 1991. Springer-Verlag."},{"issue":"2\/3","key":"41_CR19","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/S0167-6423(96)00020-2","volume":"28","author":"J. M. Wing","year":"1997","unstructured":"J. M. Wing and M. Vaziri-Farahani. A case study in model checking software systems. Science of Computer Programming, 28(2\/3):273\u2013299, April 1997.","journal-title":"Science of Computer Programming"}],"container-title":["Lecture Notes in Computer Science","Perspectives of System Informatics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46562-6_41","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T09:04:30Z","timestamp":1737536670000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46562-6_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540671022","9783540465621"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-46562-6_41","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}