{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T04:20:13Z","timestamp":1742617213347,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540620341"},{"type":"electronic","value":"9783540496311"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-62034-6_36","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:32:12Z","timestamp":1330295532000},"page":"43-51","source":"Crossref","is-referenced-by-count":6,"title":["Mechanized formal methods: Progress and prospects"],"prefix":"10.1007","author":[{"given":"John","family":"Rushby","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"4_CR1","series-title":"volume 1102 of Lecture Notes in Computer Science","volume-title":"Computer-Aided Verification, CAV '96","year":"1996","unstructured":"Rajeev Alur and Thomas A. Henzinger, editors. Computer-Aided Verification, CAV '96, volume 1102 of Lecture Notes in Computer Science, New Brunswick, NJ, July\/August 1996. Springer-Verlag."},{"key":"4_CR2","series-title":"volume 939 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1007\/3-540-60045-0_63","volume-title":"Computer-Aided Verification, CAV '95","author":"\u00e1. T. Eir\u00edksson","year":"1995","unstructured":"\u00e1sgeir Th. Eir\u00edksson and Ken L. McMillan. Using formal verification\/analysis methods on the critical path in system design: A case study. In Pierre Wolper, editor, Computer-Aided Verification, CAV '95, volume 939 of Lecture Notes in Computer Science, pages 367\u2013380, Liege, Belgium, June 1995. Springer-Verlag."},{"issue":"3","key":"4_CR3","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R. E. Bryant","year":"1992","unstructured":"Randal E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293\u2013318, September 1992.","journal-title":"ACM Computing Surveys"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Randal E. Bryant. Bit-level analysis of an SRT divider circuit. In Proceedings of the 33rd Design Automation Conference, pages 661\u2013665, Las Vegas, NV, June 1996.","DOI":"10.1145\/240518.240643"},{"key":"4_CR5","series-title":"volume 1102 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/3-540-61474-5_62","volume-title":"Computer-Aided Verification, CAV '96","author":"E. M. Clarke","year":"1996","unstructured":"E. M. Clarke, S. M. German, and X. Zhao. Verifying the SRT division algorithm using theorem proving techniques. In Alur and Henzinger [1], pages 111\u2013122."},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, Manpreet Khaira, and Xudong Zhao. Word level symbolic model checking\u2014avoiding the Pentium FDIV error. In Proceedings of the 33rd Design Automation Conference, pages 645\u2013648, Las Veqas, NV, June 1996.","DOI":"10.1145\/240518.240640"},{"issue":"2","key":"4_CR7","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/BF01383968","volume":"6","author":"E. M. Clarke","year":"1995","unstructured":"Edmund M. Clarke, Orna Grumberg, Hiromi Haraishi, Somesh Jha, David E. Long, Kenneth L. McMillan, and Linda A. Ness. Verification of the Futurebus+ cache coherence protocol. Formal Methods in System Design, 6(2):217\u2013232, March 1995.","journal-title":"Formal Methods in System Design"},{"issue":"2","key":"4_CR8","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1109\/32.345825","volume":"21","author":"D. Craigen","year":"1995","unstructured":"Dan Craigen, Susan Gerhart, and Ted Ralston. Formal methods reality check: Industrial usage. IEEE Transactions on Software Engineering, 21(2):90\u201398, February 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"4_CR9","first-page":"538","volume-title":"Theorem proving: Not an esoteric diversion, but the unifying framework for industrial verification","author":"D. A. Cyrluk","year":"1995","unstructured":"David A. Cyrluk and Mandayam K. Srivas. Theorem proving: Not an esoteric diversion, but the unifying framework for industrial verification. In International Conference on Computer Design: VLSI in Computers and Processors (ICCD '95), pages 538\u2013544, Austin, TX, October 1995. IEEE Computer Society."},{"key":"4_CR10","first-page":"522","volume-title":"Protocol verification as a hardware design aid","author":"D. L. Dill","year":"1992","unstructured":"David L. Dill, Andreas J. Drexler, Alan J. Hu, and C. Han Yang. Protocol verification as a hardware design aid. In International Conference on Computer Design: VLSI in Computers and Processors, pages 522\u2013525. IEEE Computer Society, October 1992. Cambridge, MA."},{"key":"4_CR11","series-title":"volume 1051 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"662","DOI":"10.1007\/3-540-60973-3_113","volume-title":"Formal Methods Europe FME '96","author":"K. Havelund","year":"1996","unstructured":"Klaus Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. In Formal Methods Europe FME '96, volume 1051 of Lecture Notes in Computer Science, pages 662\u2013681, Oxford, UK, March 1996. Springer-Verlag."},{"key":"4_CR12","first-page":"79","volume-title":"Experiences and lessons from the analysis of TCAS II","author":"M. P. E. Heimdahl","year":"1996","unstructured":"Mats P. E. Heimdahl. Experiences and lessons from the analysis of TCAS II. In Steven J. Zeil, editor, International Symposium on Software Testing and Analysis (ISSTA), pages 79\u201383, San Diego, CA, January 1996. Association for Computing Machinery."},{"key":"4_CR13","unstructured":"Mats P. E. Heimdahl and Barbara J. Czerny. Using PVS to analyze hierarchical state-based requirements for completeness and consistency. In IEEE High-Assurance Systems Engineering Workshop (HASE '96), Niagara on the Lake, Canada, October 1996. To appear."},{"issue":"6","key":"4_CR14","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1109\/32.508311","volume":"22","author":"M. P. E. Heimdahl","year":"1996","unstructured":"Mats P. E. Heimdahl and Nancy G. Leveson. Completeness and consistency in hierarchical state-based requirements. IEEE Transactions on Software Engineering, 22(6):363\u2013377, June 1996.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"7","key":"4_CR15","doi-asserted-by":"crossref","first-page":"484","DOI":"10.1109\/32.538605","volume":"22","author":"D. Jackson","year":"1996","unstructured":"Daniel Jackson and Craig A. Damon. Elements of style: Analyzing a software design feature with a counterexample detector. IEEE Transactions on Software Engineering, 22(7):484\u2013495, July 1996.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"4_CR16","volume-title":"Prentice Hall International Series in Computer Science","author":"C. B. Jones","year":"1990","unstructured":"Cliff B. Jones. Systematic Software Development Using VDM. Prentice Hall International Series in Computer Science. Prentice Hall, Hemel Hempstead, UK, second edition, 1990.","edition":"second edition"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Robyn R. Lutz. Analyzing software requirements errors in safety-critical embedded systems. In IEEE International Symposium on Requirements Engineering, pages 126\u2013133, San Diego, CA, January 1993.","DOI":"10.1109\/ISRE.1993.324825"},{"key":"4_CR18","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. L. McMillan","year":"1993","unstructured":"Kenneth L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA, 1993."},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Paul S. Miner and James F. Leathrum, Jr. Verification of IEEE compliant subtractive division algorithms. In Srivas [34].","DOI":"10.1007\/BFb0031800"},{"key":"4_CR20","unstructured":"J S. Moore. ACL2 theorems about commercial microprocessors. In Srivas [34]."},{"key":"4_CR21","series-title":"volume 1102 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer-Aided Verification, CAV '96","author":"S. Owre","year":"1996","unstructured":"S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. PVS: Combining specification, proof checking, and model checking. In Alur and Henzinger [1], pages 411\u2013414."},{"issue":"2","key":"4_CR22","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, February 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Seungjoon Park and David L. Dill. An executable specification, analyzer and verifier for RMO (Relaxed Memory Order). In 7th ACM Symposium on Parallel Algorithms and Architectures, pages 34\u201351, July 1995.","DOI":"10.1145\/215399.215413"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Seungjoon Park and David L. Dill. Verification of the FLASH cache coherence protocol by aggregation of distributed transactions. In 8th ACM Symposium on Parallel Algorithms and Architectures, pages 288\u2013296, Padua, Italy, June 1996.","DOI":"10.1145\/237502.237573"},{"key":"4_CR25","series-title":"volume 915 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/3-540-59293-8_189","volume-title":"TAPSOFT '95: Theory and Practice of Software Development","author":"V. Pratt","year":"1995","unstructured":"Vaughan Pratt. Anatomy of the Pentium bug. In TAPSOFT '95: Theory and Practice of Software Development, volume 915 of Lecture Notes in Computer Science, pages 97\u2013107, Aarhus, Denmark, May 1995. Springer-Verlag."},{"key":"4_CR26","series-title":"volume 939 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/3-540-60045-0_42","volume-title":"Computer-Aided Verification, CAV '95","author":"S. Rajan","year":"1995","unstructured":"S. Rajan, N. Shankar, and M.K. Srivas. An integration of model-checking with automated proof checking. In Pierre Wolper, editor, Computer-Aided Verification, CAV '95, volume 939 of Lecture Notes in Computer Science, pages 84\u201397, Liege, Belgium, June 1995. Springer-Verlag."},{"key":"4_CR27","series-title":"volume 1102 of Lecture Notes in Computer Science","first-page":"123","volume-title":"Computer-Aided Verification, CAV '96","author":"H. Rue\\","year":"1996","unstructured":"H. Rue\\, N. Shankar, and M. K. Srivas. Modular verification of SRT division. In Alur and Henzinger [1], pages 123\u2013134."},{"key":"4_CR28","series-title":"volume 1102 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/3-540-61474-5_67","volume-title":"Computer-Aided Verification, CAV '96","author":"J. Rushby","year":"1996","unstructured":"John Rushby. Automated deduction and formal methods. In Alur and Henzinger [1], pages 169\u2013183."},{"key":"4_CR29","volume-title":"Calculating with requirements","author":"J. Rushby","year":"1997","unstructured":"John Rushby. Calculating with requirements. In 3rd IEEE International Symposium on Requirements Engineering, Annapolis, MD, January 1997. IEEE Computer Society. To appear."},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"N. Shankar. Computer-aided computing. In Bernhard M\u00f6ller, editor, Mathematics of Program Construction '95, volume 947 of Lecture Notes in Computer Science, pages 50\u201366. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60117-1_5"},{"key":"4_CR31","series-title":"volume 1135 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1007\/3-540-61648-9_32","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"N. Shankar","year":"1996","unstructured":"Natarajan Shankar. Unifying verification paradigms. In Bengt Jonsson and Joachim Parrow, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 1135 of Lecture Notes in Computer Science, pages 22\u201339, Uppsala, Sweden, September 1996. Springer-Verlag."},{"key":"4_CR32","series-title":"Prentice Hall International Series in Computer Science","volume-title":"The Z Notation: A Reference Manual","year":"1993","unstructured":"J. M. Spivey, editor. The Z Notation: A Reference Manual. Prentice Hall International Series in Computer Science. Prentice Hall, Hemel Hempstead, UK, second edition, 1993.","edition":"second edition"},{"key":"4_CR33","first-page":"77","volume-title":"Feasibility of model checking software requirements","author":"T. Sreemani","year":"1996","unstructured":"Tirumale Sreemani and Joanne M. Atlee. Feasibility of model checking software requirements. In COMPASS '96 (Proceedings of the Eleventh Annual Conference on Computer Assurance), pages 77\u201388, Gaithersburg, MD, June 1996. IEEE Washington Section."},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"M. Srivas, editor. Formal Methods in Computer-Aided Design (FMCAD '96), Palo Alto, CA, November 1996. To appear.","DOI":"10.1007\/BFb0031795"},{"key":"4_CR35","series-title":"Prentice Hall International Series in Computer Science","first-page":"125","volume-title":"Applications of Formal Methods","author":"M. K. Srivas","year":"1995","unstructured":"Mandayam K. Srivas and Steven P. Miller. Formal verification of the AAMP5 microprocessor. In Michael G. Hinchey and Jonathan P. Bowen, editors, Applications of Formal Methods, Prentice Hall International Series in Computer Science, chapter 7, pages 125\u2013180. Prentice Hall, Hemel Hempstead, UK, 1995."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-62034-6_36.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:27:43Z","timestamp":1742599663000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-62034-6_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540620341","9783540496311"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/3-540-62034-6_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}