{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:15Z","timestamp":1761611175358,"version":"3.32.0"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"4-5","license":[{"start":{"date-parts":[[2006,5,2]],"date-time":"2006-05-02T00:00:00Z","timestamp":1146528000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2006,8]]},"DOI":"10.1007\/s10009-006-0204-6","type":"journal-article","created":{"date-parts":[[2006,5,1]],"date-time":"2006-05-01T17:18:14Z","timestamp":1146503894000},"page":"411-430","source":"Crossref","is-referenced-by-count":47,"title":["Putting it all together \u2013 Formal verification of the VAMP"],"prefix":"10.1007","volume":"8","author":[{"given":"Sven","family":"Beyer","sequence":"first","affiliation":[]},{"given":"Christian","family":"Jacobi","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Kr\u00f6ning","sequence":"additional","affiliation":[]},{"given":"Dirk","family":"Leinenbach","sequence":"additional","affiliation":[]},{"given":"Wolfgang J.","family":"Paul","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,2]]},"reference":[{"key":"204_CR1","unstructured":"The VAMP project. Website: http:\/\/www-wjp.cs.uni-sb.de\/projects\/verification"},{"key":"204_CR2","doi-asserted-by":"crossref","unstructured":"Berg, C.: Formal verification of an IEEE floating point adder. Master\u2019s Thesis, Saarland University, Germany (2001)","DOI":"10.1007\/3-540-44798-9_26"},{"key":"204_CR3","doi-asserted-by":"crossref","unstructured":"Berg, C., Jacobi, C.: Formal verification of the VAMP floating point unit. In: Proceedings of the 11th CHARME, vol. 2144 of LNCS, pp. 325\u2013339. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-44798-9_26"},{"key":"204_CR4","unstructured":"Berg, C., Jacobi, C., Kr\u00f6ning, D.: Formal verification of a basic circuits library. In: IASTED International Conference on Applied Informatics. ACTA Press (2001)"},{"key":"204_CR5","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/BF00243131","volume":"5","author":"W.R. Bevier","year":"1989","unstructured":"Bevier, W.R., Hunt, W.A., Moore, J.S., Young, W.D.: An approach to systems verification. J. Autom. Reason. 5, 411\u2013428 (1989)","journal-title":"J. Autom. Reason."},{"key":"204_CR6","unstructured":"Beyer, S.: Putting it all together \u2013 Formal verification of the VAMP. PhD Thesis, Saarland University, Germany (2005)"},{"key":"204_CR7","unstructured":"Beyer, S., Jacobi, C., Kr\u00f6ning, D., Leinenbach, D.: Correct hardware by synthesis from PVS. Internal Report, available at http:\/\/www-wjp.cs.uni-sb.de\/publikationen\/BJKL02.pdf (2002)"},{"key":"204_CR8","doi-asserted-by":"crossref","unstructured":"Beyer, S., Jacobi, C., Kr\u00f6ning, D., Leinenbach, D., Paul, W.: Instantiating uninterpreted functional units and memory system: Functional verification of the VAMP. In: Geist, D., Tronci, E. (eds.) CHARME 2003, vol. 2860 of LNCS, pp. 51\u201365. Springer, Heidelberg (2003)","DOI":"10.1007\/978-3-540-39724-3_7"},{"key":"204_CR9","unstructured":"Brock, B., Hunt, W.A., Kaufmann, M.: The FM9001 microprocessor proof. Technical Report Technical Report 86, Computational Logic Inc. (1994)"},{"key":"204_CR10","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1023\/A:1008685826293","volume":"11","author":"B.C. Brock","year":"1997","unstructured":"Brock, B.C., Hunt, W.A.: The DUAL-EVAL hardware description language and its use in the formal specification and verification of the FM9001 microprocessor. Form. Methods Syst. Des. 11, 71\u2013107 (1997)","journal-title":"Form. Methods Syst. Des."},{"key":"204_CR11","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessors control. In: CAV 94, vol. 818, pp. 68\u201380. Springer-Verlag, Standford, CA (1994)","DOI":"10.1007\/3-540-58179-0_44"},{"key":"204_CR12","unstructured":"Butler, R.W., Miner, P.S., Srivas, M.K., Greve, D.A., Miller, S.P.: A bitvectors library for PVS. Technical Report 110274, NASA Langley Research Center (1996)"},{"key":"204_CR13","doi-asserted-by":"crossref","unstructured":"Chen, Y.-A., Clarke, E.M., Ho, P.-H., Hoskote, Y., Kam, T., Khaira, M., O\u2019Leary, J.W., Zhao, X.: Verification of all circuits in a floating-point unit using word-level model checking. In: FMCAD, vol. 1166 of LNCS, pp. 19\u201333. Springer, Heidelberg (1996)","DOI":"10.1007\/BFb0031797"},{"key":"204_CR14","doi-asserted-by":"crossref","unstructured":"Damm, W., Pnueli, A.: Verifying out-of-order executions. In: Charme IFIP WG10.5, pp. 23\u201347. Chapman & Hall, Montreal, Canada (1997)","DOI":"10.1007\/978-0-387-35190-2_3"},{"key":"204_CR15","doi-asserted-by":"crossref","unstructured":"Eiriksson, A.P.: The formal design of 1M-gate ASICs. In: Gopalakrishnan, G., Windley, P. (eds.) FMCAD 98, vol. 1522 of LNCS, pp. 49\u201363. Springer, Heidelberg (1998)","DOI":"10.1007\/3-540-49519-3_5"},{"key":"204_CR16","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: Automata, Languages and Programming, vol. 85 of LNCS. Springer, Heidelberg (1980)","DOI":"10.1007\/3-540-10003-2_69"},{"key":"204_CR17","volume-title":"Computer Architecture: A Quantitative Approach","author":"J.L. Hennessy","year":"1996","unstructured":"Hennessy, J.L., Patterson, D.A.: Computer Architecture: A Quantitative Approach, 2nd edn. Morgan Kaufmann, San Mateo, CA (1996)","edition":"2"},{"key":"204_CR18","unstructured":"Hillebrand, M.: Address spaces and virtual memory: Specification, implementation, and correctnesss. PhD Thesis, Saarland University, Germany (2005)"},{"key":"204_CR19","doi-asserted-by":"crossref","unstructured":"Hosabettu, R., Srivas, M., Gopalakrishnan, G.: Proof of correctness of a processor with reorder buffer using the completion functions approach. In: Computer-Aided Verification, CAV \u201999, vol. 1633, pp. 47\u201359. Springer-Verlag, Trento, Italy (1999)","DOI":"10.1007\/3-540-48683-6_7"},{"key":"204_CR20","doi-asserted-by":"crossref","unstructured":"Hunt, W.A., Sawada, J.: Verifying the FM9801 microarchitecture. IEEE Micro, pp. 47\u201355 (1999)","DOI":"10.1109\/40.768503"},{"key":"204_CR21","unstructured":"Institute of Electrical and Electronics Engineers. ANSI\/IEEE standard 754\u20131985, IEEE Standard for Binary Floating-Point Arithmetic (1985)"},{"key":"204_CR22","unstructured":"Jacobi, C.: A formally verified theory of IEEE rounding. Unpublished, available at http:\/\/www-wjp.cs.uni-sb.de\/~cj\/ieee-lib.ps (2001)"},{"key":"204_CR23","doi-asserted-by":"crossref","unstructured":"Jacobi, C.: Formal verification of complex out-of-order pipelines by combining model-checking and theorem-proving. In: CAV, vol. 2404 of LNCS. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-45657-0_23"},{"key":"204_CR24","unstructured":"Jacobi, C.: Formal verificaton of a fully IEEE compliant floating point unit. PhD Thesis, Saarland University, Germany (2002)"},{"key":"204_CR25","doi-asserted-by":"crossref","unstructured":"Jacobi, C., Berg, C.: Formal verification of the VAMP floating point unit. In: Formal Methods in System Design, pp. 227\u2013266. Springer (May 2005)","DOI":"10.1007\/s10703-005-1613-y"},{"key":"204_CR26","doi-asserted-by":"crossref","unstructured":"Jacobi, C., Weber, K., Paruthi, V., Baumgartner, J.: Automatic formal verification of fused-multiply-add FPUs. In DATE, pp. 1298\u20131303. IEEE Computer Society (2005)","DOI":"10.1109\/DATE.2005.75"},{"key":"204_CR27","unstructured":"Karatsuba, A., Ofman, Y.: Multiplication of multidigit numbers on automata. Sov. Phys. Dokl. 7 (1963)"},{"key":"204_CR28","unstructured":"Kr\u00f6ning, D.: Formal verification of pipelined microprocessors. PhD Thesis, Saarland University, Germany (2001)"},{"key":"204_CR29","unstructured":"Kr\u00f6ning, D., M\u00fcller, S., Paul, W.: Proving the correctness of pipelined micro-architectures. In: 3ITG-\/GI\/GMM-Workshop Methoden und Beschreibungsprachen zur Modellierung und Verifikation von Schaltungen und System, pp. 89\u201398. VDE Verlag (2000)"},{"key":"204_CR30","doi-asserted-by":"crossref","unstructured":"Kr\u00f6ning, D., M\u00fcller, S., Paul, W.: Proving the correctness of processors with delayed branch using delayed PCs. Numbers, Information and Complexity, pp. 579\u2013588 (2000)","DOI":"10.1007\/978-1-4757-6048-4_46"},{"key":"204_CR31","doi-asserted-by":"crossref","unstructured":"Kr\u00f6ning, D., Paul, W.: Automated pipeline design. In: Proceedings of the 38th Design Automation Conference, pp. 810\u2013815. ACM Press, New York (2001)","DOI":"10.1145\/378239.379071"},{"key":"204_CR32","unstructured":"Leinenbach, D.: Implementierung eines maschinell verifizierten Prozessors. Master\u2019s Thesis, Saarland University, Germany (2002)"},{"key":"204_CR33","doi-asserted-by":"crossref","unstructured":"McMillan, K.: Verification of an implementation of Tomasulo\u2019s algorithm by compositional model checking. In: CAV 98, vol. 1427. Springer, Heidelberg (1998)","DOI":"10.1007\/BFb0028738"},{"key":"204_CR34","doi-asserted-by":"crossref","unstructured":"McMillan, K.: Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In: CHARME 2001, vol. 2144 of LNCS. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-44798-9_17"},{"key":"204_CR35","unstructured":"Meyer, C.: Entwicklung einer Laufzeitumgebung f\u00fcr den VAMP-Prozessor. Master\u2019s Thesis, Saarland University, Germany (2002)"},{"key":"204_CR36","unstructured":"Miner, P.S.: Defining the IEEE-854 floating-point standard in PVS. Technical Report TM-110167, NASA Langley Research Center (1995)"},{"key":"204_CR37","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-04267-0","volume-title":"Computer architecture. Complexity and correctness","author":"S.M. M\u00fcller","year":"2000","unstructured":"M\u00fcller, S.M., Paul, W.J.: Computer architecture. Complexity and correctness. Springer, Heidelberg (2000)"},{"key":"204_CR38","unstructured":"O\u2019Leary, J., Zhao, X., Gerth, R., Seger, C.-J.H.: Formally verifying IEEE compliance of floating-point hardware. Intel Technol. J., Q1 (1999)"},{"key":"204_CR39","doi-asserted-by":"crossref","unstructured":"Owre, S., Shankar, N., Rushby, J.M.: PVS: A prototype verification system. In: CADE 11, vol. 607 of LNAI, pp. 748\u2013752. Springer, Heidelberg (1992)","DOI":"10.1007\/3-540-55602-8_217"},{"key":"204_CR40","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1112\/S1461157000000176","volume":"1","author":"D.M. Russinoff","year":"1998","unstructured":"Russinoff, D.M.: A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD-K7 processor. LMS J. Comput. Math. 1, 148\u2013200 (1998)","journal-title":"LMS J. Comput. Math."},{"key":"204_CR41","doi-asserted-by":"crossref","unstructured":"Russinoff, D.M.: A case study in formal verification of register-transfer logic with ACL2: The floating point adder of the AMD Athlon processor. In: FMCAD-00, vol. 1954 of LNCS. Springer, Heidelberg (2000)","DOI":"10.1007\/3-540-40922-X_3"},{"key":"204_CR42","doi-asserted-by":"crossref","unstructured":"Sawada, J., Hunt, W.A.: Trace table based approach for pipelined microprocessor verification. In: CAV 97, vol. 1254 of LNCS. Springer, Heidelberg (1997)","DOI":"10.1007\/3-540-63166-6_36"},{"key":"204_CR43","doi-asserted-by":"crossref","unstructured":"Sawada, J., Hunt, W.A.: Processor verification with precise exceptions and speculative execution. In: CAV 98, vol. 1427 of LNCS. Springer, Heidelberg (1998)","DOI":"10.1007\/BFb0028740"},{"issue":"2","key":"204_CR44","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1023\/A:1014122630277","volume":"20","author":"J. Sawada","year":"2002","unstructured":"Sawada, J., Hunt, W.A.: Verification of the FM9801 microprocessor: An out-of-order microprocessor model with speculative execution, exceptions, and self-modifying code. Form. Methods Syst. Des. 20(2), 187\u2013222 (2002)","journal-title":"Form. Methods Syst. Des."},{"key":"204_CR45","doi-asserted-by":"crossref","unstructured":"Shen, X., Arvind, Rudolph, L.: CACHET: An adaptive cache coherence protocol for distributed shared-memory systems. In: International Conference on Supercomputing (1999)","DOI":"10.1145\/305138.305187"},{"key":"204_CR46","unstructured":"Slobodova, A., Nagalla, K.: Formal verification of floating point multiply add on Itanium processors. In: Workshop on Designing Correct Circuits (2004)"},{"key":"204_CR47","doi-asserted-by":"crossref","unstructured":"Stoy, J., Shen, X., Arvind: Proofs of correctness of cache-coherence protocols. In: FME, vol. 2021 of LNCS. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-45251-6_4"},{"key":"204_CR48","unstructured":"Velev, M.N., Bryant, R.E.: Superscalar processor verification using efficient reductions of the logic of equality with uninterpreted functions to propositional logic. In: CHARME, vol. 1703 of LNCS. Springer, Heidelberg (1999)"},{"key":"204_CR49","doi-asserted-by":"crossref","unstructured":"Velev, M.N., Bryant, R.E.: Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction. In: DAC. ACM (2000)","DOI":"10.1145\/337292.337331"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-006-0204-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-006-0204-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-006-0204-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,8]],"date-time":"2025-01-08T19:46:34Z","timestamp":1736365594000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-006-0204-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,5,2]]},"references-count":49,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2006,8]]}},"alternative-id":["204"],"URL":"https:\/\/doi.org\/10.1007\/s10009-006-0204-6","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2006,5,2]]}}}