{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T05:41:06Z","timestamp":1725514866668},"publisher-location":"Berlin, Heidelberg","reference-count":47,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540682356"},{"type":"electronic","value":"9783540682370"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-68237-0_2","type":"book-chapter","created":{"date-parts":[[2008,6,4]],"date-time":"2008-06-04T05:36:00Z","timestamp":1212557760000},"page":"12-32","source":"Crossref","is-referenced-by-count":12,"title":["Getting Formal Verification into Design Flow"],"prefix":"10.1007","author":[{"family":"Arvind","sequence":"first","affiliation":[]},{"given":"Nirav","family":"Dave","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Katelman","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: The Relative Consistency of the Axiom of Choice Mechanized using Isabelle\/ZF. London Mathematical Society Journal of Computation and Mathematics\u00a06 (2003)","DOI":"10.1112\/S1461157000000449"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. PhD thesis, Carnegie Mellon University (1992)","DOI":"10.1007\/978-1-4615-3190-6_3"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. In: 14th International Conference on Computer Aided Verification (CAV), Copenhagen, Denmark (2002)","DOI":"10.1007\/3-540-45657-0_7"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bjorner, N.: Z3: An Efficient SMT Solver. In: 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Budapest, Hungary (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Manolios, P., Srinivasan, S.K., Vroon, D.: BAT: The Bit-Level Analysis Tool. In: Proceedings of the 19th International Conference on Computer Aided Verification (CAV), Berlin, Germany (2007)","DOI":"10.1007\/978-3-540-73368-3_35"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th conference on Design automation (DAC), Las Vegas, NV (2001)","DOI":"10.1145\/378239.379017"},{"key":"2_CR7","unstructured":"Mentor Graphics Corp.: 0-In\u00ae Formal Verification, www.mentor.com\/products\/fv\/abv\/0-in_fv\/"},{"key":"2_CR8","unstructured":"Synopsys, Inc.: Formality\u00ae Equivalence Checker, www.synopsys.com\/products\/verification\/"},{"key":"2_CR9","unstructured":"Mentor Graphics Corp.: FormalPro TM , www.mentor.com\/products\/fv\/ev\/formalpro\/"},{"key":"2_CR10","unstructured":"Cadence Design Systems, Inc.: Cadence\u00ae Encounter\u00ae Conformal\u00ae Equivalence Checker, www.cadence.com\/products\/digital_ic\/conformal\/index.aspx"},{"key":"2_CR11","unstructured":"Jasper Design Automation, Inc.: JasperGold\u00ae Verification System, www.jasper-da.com\/products_jaspergold.htm"},{"key":"2_CR12","unstructured":"Cadence Design Systems, Inc.: Incisive\u00ae Formal Verifier, www.cadence.com\/products\/functional_ver\/incisive_formal_verifier\/index.aspx"},{"issue":"2","key":"2_CR13","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C. Meadows","year":"1996","unstructured":"Meadows, C.: The NRL Protocol Analyzer: An Overview. The Journal of Logic Programming\u00a026(2), 113\u2013131 (1996)","journal-title":"The Journal of Logic Programming"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Sproston, J.: Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol. In: Proceedings of the Second Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM-PROBMIV), Copenhagen, Denmark (2002)","DOI":"10.1007\/3-540-45605-8_11"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Dill, D.L.: Automatic Verification of Pipelined Microprocessor Control. In: Proceedings of the 6th International Conference on Computer Aided Verification (CAV), Stanford, CA (1994)","DOI":"10.1007\/3-540-58179-0_44"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Stoy, J.E., Shen, X., Arvind.: Proofs of Correctness of Cache-Coherence Protocols. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, pp. 47\u201371. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-45251-6_4"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI), San Diego, CA (2002)","DOI":"10.1145\/512529.512558"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Portland, OR (2002)","DOI":"10.1145\/503272.503274"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Russinoff, D.M.: A Case Study in Fomal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD Athlon TM Processor. In: Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design (FMCAD), Austin, TX (2000)","DOI":"10.1007\/3-540-40922-X_3"},{"issue":"9","key":"2_CR20","doi-asserted-by":"publisher","first-page":"1381","DOI":"10.1109\/TCAD.2005.850814","volume":"24","author":"C.J. Seger","year":"2005","unstructured":"Seger, C.J., Jones, R., O\u2019Leary, J., Melham, T., Aagaard, M., Barrett, C., Syme, D.: An Industrially Effective Environment for Formal Hardware Verification. Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on\u00a024(9), 1381\u20131405 (2005)","journal-title":"Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The ASTRE\u00c9 Analyzer. In: Proceedings of the 14th European Symposium on Programming (ESOP), Edinburgh, UK (2005)","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Berry, G.: The Foundations of Esterel, 425\u2013454 (2000)","DOI":"10.7551\/mitpress\/5641.003.0021"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Arvind, N.R.S., Rosenband, D.L., Dave, N.: High-level synthesis: an essential ingredient for designing complex ASICs. In: Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD), San Jose, CA (2004)","DOI":"10.1109\/ICCAD.2004.1382681"},{"key":"2_CR24","unstructured":"IEEE: IEEE standard 802.11a supplement. Wireless LAN Medium Access Control (MAC) and Physical Layer (PHY) Specifications (1999)"},{"key":"2_CR25","unstructured":"International Telecommunication Union: H.264, www.itu.int\/rec\/T-REC-H.264"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Joshi, R., Lamport, L., Matthews, J., Tasiran, S., Tuttle, M., Yu, Y.: Checking Cache-Coherence Protocols with TLA+. Form. Methods Syst. Des.\u00a022(2) (2003)","DOI":"10.1023\/A:1022969405325"},{"issue":"3","key":"2_CR27","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1109\/40.768501","volume":"19","author":"S.X. Arvind","year":"1999","unstructured":"Arvind, S.X.: Using Term Rewriting Systems to Design and Verify Processors. IEEE Micro\u00a019(3), 36\u201346 (1999)","journal-title":"IEEE Micro"},{"issue":"8","key":"2_CR28","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1016\/j.entcs.2006.11.036","volume":"174","author":"S. Krsti\u0107","year":"2007","unstructured":"Krsti\u0107, S., Jones, R.B., O\u2019Leary, J.: Mothers of Pipelines. Electron. Notes Theor. Comput. Sci.\u00a0174(8), 7\u201322 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"2_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/3-540-40922-X_11","volume-title":"Formal Methods in Computer-Aided Design","author":"P. Manolios","year":"2000","unstructured":"Manolios, P.: Correctness of Pipelined Machines. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 161\u2013178. Springer, Heidelberg (2000)"},{"key":"2_CR30","unstructured":"Dave, N., Pellauer, M., Gerding, S., Arvind.: 802.11a Transmitter: A Case Study in Microarchitectural Exploration. In: Proceedings of Formal Methods and Models for Codesign (MEMOCODE), Napa,\u00a0CA (2006)"},{"key":"2_CR31","unstructured":"Bluespec, Inc. Waltham, MA: Bluespec SystemVerilog Ver.\u00a03.8 Reference Guide (November 2004)"},{"key":"2_CR32","volume-title":"Parallel Program Design: A Foundation","author":"K.M. Chandy","year":"1988","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Reading (1988)"},{"key":"2_CR33","unstructured":"Berry, G.: The Esterel v5 Language Primer Version v5_91 (2000)"},{"key":"2_CR34","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1997","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice Hall PTR, Upper Saddle River (1997)"},{"key":"2_CR35","unstructured":"Dave, N., Ng, M.C., Arvind.: Automatic Synthesis of Cache-Coherence Protocol Processors Using Bluespec. In: Proc. of Formal Methods and Models for Codesign, Verona,\u00a0Italy (2005)"},{"key":"2_CR36","unstructured":"Dave, N., Ng, M.C., Arvind.: Standard for SystemVerilog: Unified Hardware Design, Specification and Verification Language (IEEE Std. 1800-2007)"},{"key":"2_CR37","volume-title":"The SPIN MODEL CHECKER: Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN MODEL CHECKER: Primer and Reference Manual. Addison-Wesley, Reading (2003)"},{"key":"2_CR38","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Moore, J.S., Manolios, P.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Norwell (2000)"},{"key":"2_CR39","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J.M., Rushby, J.M., Shankar, N.: PVS: A Prototype Verification System. In: Proceedings of the 11th International Conference on Automated Deduction (CADE), Saratoga Springs, NY (1992)","DOI":"10.1007\/3-540-55602-8_217"},{"key":"2_CR40","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer-Verlag, London (2002)"},{"key":"2_CR41","unstructured":"SRI International: Yices, yices.csl.sri.com\/index.shtml"},{"issue":"2","key":"2_CR42","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D. Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: A Lightweight Object Modelling Notation. ACM Trans. Softw. Eng. Methodol.\u00a011(2), 256\u2013290 (2002)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"2_CR43","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)"},{"key":"2_CR44","doi-asserted-by":"crossref","unstructured":"Lynch, N.A., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. In: Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing (PODC), Vancouver, British Columbia (1987)","DOI":"10.1145\/41840.41852"},{"key":"2_CR45","doi-asserted-by":"crossref","unstructured":"Archer, L.M.H.L., Mitra, N., Umeno, S.: Specifying and Proving Properties of Timed I\/O Automata in the TIOA Toolkit. In: Proceedings. Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE), Napa, CA (2006)","DOI":"10.1109\/MEMCOD.2006.1695916"},{"key":"2_CR46","unstructured":"Shen, X.: Design and Verification of Adaptive Cache Coherence Protocols. PhD thesis, MIT, Cambridge,\u00a0MA (2000)"},{"key":"2_CR47","volume-title":"Proceedings of the 13th ACM SIGARCH International Conference on Supercomputing","author":"X. Shen","year":"1999","unstructured":"Shen, X., Rudolph, L., Arvind,: CACHET: An Adaptive Cache Coherence Protocol for Distributed Shared-Memory Systems. In: Proceedings of the 13th ACM SIGARCH International Conference on Supercomputing, IEEE Computer Society, Los Alamitos (1999)"}],"container-title":["Lecture Notes in Computer Science","FM 2008: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-68237-0_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,27]],"date-time":"2024-02-27T00:57:38Z","timestamp":1708995458000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-68237-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540682356","9783540682370"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-68237-0_2","relation":{},"subject":[]}}