{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:34:00Z","timestamp":1754483640368},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1996,3,1]],"date-time":"1996-03-01T00:00:00Z","timestamp":825638400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1996,3]]},"DOI":"10.1007\/bf00122419","type":"journal-article","created":{"date-parts":[[2004,10,31]],"date-time":"2004-10-31T08:51:17Z","timestamp":1099212677000},"page":"153-188","source":"Crossref","is-referenced-by-count":18,"title":["Applying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods"],"prefix":"10.1007","volume":"8","author":[{"given":"Mandayam K.","family":"Srivas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steven P.","family":"Miller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","unstructured":"D. Best, C. Kress, N. Mykris, J. Russel, and W. Smith, ?An advanced-architecture cmos\/sos microprocessor,? IEEE Micro, pp. 11?26, August 1982.","DOI":"10.1109\/MM.1982.290992"},{"key":"CR2","volume-title":"A Computational Logic","author":"R.S. Boyer","year":"1979","unstructured":"R.S. Boyer and J.S. Moore, A Computational Logic, Academic Press, New York, NY, 1979."},{"key":"CR3","unstructured":"S. Brock and C. George, The RAISE Method Manual, Computer Resources International A\/S, 1990."},{"key":"CR4","series-title":"Vol. 818 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"Computer-Aided Verification, CAV'94","author":"J.R. Burch","year":"1994","unstructured":"J.R. Burch and D.L. Dill, ?Automatic verification of pipelined microprocessor control,? in David Dill (Ed.), Computer-Aided Verification, CAV'94, Vol. 818 of Lecture Notes in Computer Science, pp. 68?80, Stanford, CA, June 1994, Springer-Verlag."},{"issue":"No. 1","key":"CR5","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1093\/comjnl\/35.1.3","volume":"35","author":"A. Burns","year":"1992","unstructured":"A. Burns, J. McDermid, and J. Dobson, ?On the meaning of safety and security,? Computer Journal, Vol. 35, No. 1, pp. 3?15, 1992.","journal-title":"Computer Journal"},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"Ricky W. Butler, ?NASA Langley's research program in formal methods,? in COMPASS'91, Proceedings of the Sixth Annual Conference on Computer Assurance, Gaithersburg, MD, June 1991, pp. 157?162, IEEE Washington Section.","DOI":"10.1109\/CMPASS.1991.161055"},{"key":"CR7","series-title":"Vol. 818 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/3-540-58179-0_59","volume-title":"Computer-Aided Verification, CAV'94","author":"D. Cyrluk","year":"1994","unstructured":"D. Cyrluk and P. Narendran, ?Ground temproral logic?a logic for hardware verification,? in David Dill (Ed.), Computer-Aided Verification, CAV'94, Vol. 818 of Lecture Notes in Computer Science, pp. 247?259, Stanford, CA, June 1994, Springer-Verlag."},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"D. Cyrluck, S. Rajan, N. Shankar, and M.K. Srivas, ?Effective theorem proving for hardware verification,? in Kumar and Kropf [18], pp. 203?222.","DOI":"10.1007\/3-540-59047-1_50"},{"key":"CR9","volume-title":"Technical Report SRI-CSL-93-12","author":"Cyrluk","year":"1993","unstructured":"Cyrluk, ?Microprocessor verification in PVS: A methodology and simple example,? Technical Report SRI-CSL-93?12, Computer Science Laboratory, SRI International, Menlo Park, CA, December 1993."},{"key":"CR10","volume-title":"NASA Technical Memorandum 102716","author":"Ben L. Vito Di","year":"1990","unstructured":"Ben L.Di Vito, Ricky W. Butler, and James L. Caldwell, ?Formal design and verification of a reliable computing platform for real-time control,? NASA Technical Memorandum 102716, NASA Langley Research Center, Hampton, VA, October 1990."},{"issue":"No. 7","key":"CR11","doi-asserted-by":"crossref","first-page":"744","DOI":"10.1109\/TSE.1986.6312976","volume":"12","author":"M. Fagan","year":"1986","unstructured":"M. Fagan, ?Advances in software inspections,? IEEE Transactions on Software Engineering, Vol. SE-12, No. 7, pp. 744?751, 1986.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"CR12","volume-title":"Technical Report STP-FT-322-91","author":"S. Gerhart","year":"1991","unstructured":"S. Gerhart, M. Bouler, K. Greene, D. Jamsek, T. Ralston, and D. Russinoff, ?Formal methods transition study final report,? Technical Report STP-FT-322?91, Microelectronics and Computer Technology Corporation, Austin, Texas, August 1991."},{"key":"CR13","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1126\/science.267.5196.332","volume":"267","author":"James Glanz","year":"1995","unstructured":"James Glanz, ?Mathematical logic flushes out the bugs in chip designs,? Science, Vol. 267, pp. 332?333, 1995.","journal-title":"Science"},{"key":"CR14","unstructured":"M. Gordon, ?Why higher-order logic is a good formalism for specifying and verifying hardware,? Technical Report 77, University of Cambridge Computer Laboratory, September 1985."},{"key":"CR15","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic","year":"1993","unstructured":"M.J.C. Gordon and T.F. Melham (Eds.), Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic, Cambridge University Press, Cambridge, UK, 1993."},{"key":"CR16","series-title":"Vol. 795 of Lecture Notes in Artificial Intelligence","volume-title":"FM8501: A Verified Microprocessor","author":"Warren A. Hunt Jr.","year":"1994","unstructured":"Warren A. HuntJr., FM8501: A Verified Microprocessor, Vol. 795 of Lecture Notes in Artificial Intelligence, Springer-Verlag, Berlin, 1994."},{"key":"CR17","series-title":"Prentice Hall International Series in Computer Science","volume-title":"Systematic Software Development Using VDM","author":"Cliff 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":"CR18","series-title":"Vol. 910 of Lecture Notes in Computer Science","volume-title":"Theorem Provers in Circuit Design (TPCD'94)","year":"1994","unstructured":"Ramayya Kumar and Thomas Kropf (Eds.), Theorem Provers in Circuit Design (TPCD'94), Vol. 910 of Lecture Notes in Computer Science, Bad Herrenalb, Germany, September 1994, Springer-Verlag."},{"key":"CR19","volume-title":"Technical Report SRI-CSL-95-13","author":"Mandayam Srivas","year":"1995","unstructured":"Mandayam Srivas et al., ?Hardware verification using PVS: A tutorial,? Technical Report SRI-CSL-95?13, Computer Science Laboratory, SRI International, Menlo Park, CA, 1995 (Forthcoming)."},{"key":"CR20","doi-asserted-by":"crossref","unstructured":"Steven P. Miller and Mandayam, Srivas, ?Formal verification of the AAMP5 microprocessor: A case study in the industrial use of formal methods,? in WIFT'95: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, FL, 1995, pp. 2?16, IEEE Computer Society.","DOI":"10.1109\/WIFT.1995.515475"},{"key":"CR21","volume-title":"The PVS Specification Language","author":"S. Owre","year":"1993","unstructured":"S. Owre, N. Shankar, and J.M. Rushby, The PVS Specification Language, Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993 (A new edition for PVS Version 2 is expected in early 1995)."},{"key":"CR22","series-title":"Vol. 939 of Lecture Note in Computer Science","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/3-540-60045-0_42","volume-title":"Computer-Aided Verification, Cag'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 (Ed.), Computer-Aided Verification, Cag'95, Vol. 939 of Lecture Note in Computer Science, pp. 84?97, Liege, Belgium, June 1995, Springer-Verlag."},{"key":"CR23","unstructured":"AAMP2 Advanced Architecture Microprocessor II Reference Manual, Rockwell International, Collins Commercial Avionics, Rockwell International Corporation, Cedar Rapids, Iowa 52498, February 1990."},{"key":"CR24","unstructured":"AAMP5 Microarchitecture (Unreleased Document), Rockwell International Processor and Software Technology Department, Advanced Technology and Engineering, Collins Commercial Avionics, Rockwell International Corporation, Cedar Rapids, Iowa 52498, February 1993."},{"issue":"No. 1","key":"CR25","first-page":"181","volume":"4","author":"James B. Saxe","year":"1994","unstructured":"James B. Saxe, Stephen J. Garland, John V. Guttag, and James J. Horning, ?Using transformations and verification in circuit design,? Formal Methods in System Design, Vol. 4, No. 1, pp. 181?210, 1994.","journal-title":"Formal Methods in System Design"},{"key":"CR26","volume-title":"The PVS Proof Checker: A Refrence Manual","author":"N Shankar","year":"1993","unstructured":"N Shankar, S. Owre, and J.M. Rushby, The PVS Proof Checker: A Refrence Manual, Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993 (A new edition for PVS Version 2 is expected in early 1995)."},{"issue":"No. 5","key":"CR27","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1109\/52.57892","volume":"7","author":"Mandayam Srivas","year":"1990","unstructured":"Mandayam Srivas and Mark Bickford, ?Formal verification of a pipelined microprocessor,? IEEE Software, Vol. 7, No. 5, pp. 52?64, 1990.","journal-title":"IEEE Software"},{"key":"CR28","volume-title":"Technical Report SRI-CSL-95-4","author":"Mandayam Srivas","year":"1995","unstructured":"Mandayam Srivas and Steven P. Miller, ?Formal verification of a commercial microprocessor,? Technical Report SRI-CSL-95?4, Computer Science Laboratory, SRI International, Menlo Park, CA, February 1995."},{"key":"CR29","series-title":"Number 780 in Lecture Notes in Computer Science","first-page":"281","volume-title":"Higher Order Logic Theorem Proving and its Applications (6th International Workshop, HUG'93)","author":"S. Tahar","year":"1993","unstructured":"S. Tahar and R. Kumar, ?Implementing a methodology for formally verifying risc processors in hol,? in Jeffrey J. Joyce and Carl-Johan H. Seger (Eds.), Higher Order Logic Theorem Proving and its Applications (6th International Workshop, HUG'93), Number 780 in Lecture Notes in Computer Science, pp. 281?294, Vancouver, Canada, August 1993, Springer-Verlag."},{"key":"CR30","doi-asserted-by":"crossref","unstructured":"Phillip J. Windley and Michael L. Coe, ?A correctness model for pipelined microprocessors,? in Kumar and Kropf [18], pp. 33?51.","DOI":"10.1007\/3-540-59047-1_41"},{"key":"CR31","doi-asserted-by":"crossref","unstructured":"P.J. Windley, ?Formal modeling and verification of microprocessors,? IEEE Transactions on Computers, Vol. 44, No. 1, 1995.","DOI":"10.1109\/12.368009"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00122419.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00122419\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00122419","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T16:38:35Z","timestamp":1585931915000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00122419"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,3]]},"references-count":31,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1996,3]]}},"alternative-id":["BF00122419"],"URL":"https:\/\/doi.org\/10.1007\/bf00122419","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,3]]}}}