{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T12:02:44Z","timestamp":1742990564434,"version":"3.40.3"},"publisher-location":"Boston, MA","reference-count":27,"publisher":"Springer US","isbn-type":[{"type":"print","value":"9781441915382"},{"type":"electronic","value":"9781441915399"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-1-4419-1539-9_5","type":"book-chapter","created":{"date-parts":[[2010,3,2]],"date-time":"2010-03-02T00:26:11Z","timestamp":1267489571000},"page":"145-174","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Verifying Pipelines with BAT"],"prefix":"10.1007","author":[{"given":"Panagiotis","family":"Manolios","sequence":"first","affiliation":[]},{"given":"Sudarshan K.","family":"Srinivasan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,1,23]]},"reference":[{"key":"5_CR1_5","unstructured":"Bentley B (2005) Validating a modern microprocessor. See URL http:\/\/www.-cav2005.inf.ed.ac.uk\/bentley_CAV_07_08_2005.ppt"},{"issue":"1\u20132","key":"5_CR2_5","first-page":"115","volume":"59","author":"M Browne","year":"1998","unstructured":"Browne M, Clarke EM, Grumberg O (1998) Characterizing finite Kripke structures in propositional temporal logic. Theor Comput Sci 59(1\u20132):115\u2013131","journal-title":"Theor Comput Sci"},{"key":"5_CR3_5","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"Computer-aided verification (CAV \u201994)","author":"JR Burch","year":"1994","unstructured":"Burch JR, Dill DL (1994) Automatic verification of pipelined microprocessor control. In: Computer-aided verification (CAV \u201994), vol 818 of LNCS. Springer, Berlin, pp 68\u201380"},{"key":"5_CR4_5","first-page":"1590","volume-title":"Design, automation and test in Europe","author":"B Chambers","year":"2009","unstructured":"Chambers B, Manolios P, Vroon D (2009) Faster sat solving with better CNF generation. In: Design, automation and test in Europe. IEEE, New York, pp 1590\u20131595"},{"key":"5_CR5_5","volume-title":"Model checking","author":"EM Clarke","year":"1999","unstructured":"Clarke EM, Grumberg O, Peled D (1999) Model checking. MIT, Cambridge, MA"},{"key":"5_CR6_5","unstructured":"Een N, Sorensson N (2007) The minisat page. See URL http:\/\/minisat.se\/Main.html"},{"key":"5_CR7_5","first-page":"1234","volume-title":"Design, automation and test in Europe, (DATE\u201906)","author":"R Kane","year":"2006","unstructured":"Kane R, Manolios P, Srinivasan SK (2006) Monolithic verification of deep pipelines with collapsed flushing. In: Gielen GGE (ed) Design, automation and test in Europe, (DATE\u201906). European Design and Automation Association, Leuven, Belgium, pp 1234\u20131239"},{"key":"5_CR8_5","volume-title":"Computer-aided reasoning: an approach","author":"M Kaufmann","year":"2000","unstructured":"Kaufmann M, Manolios P, Moore JS (2000) Computer-aided reasoning: an approach. Kluwer, Dordrecht"},{"key":"5_CR9_5","series-title":"of LNCS","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/3-540-40922-X_11","volume-title":"Formal methods in computer-aided design \u2013 FMCAD 2000","author":"P Manolios","year":"2000","unstructured":"Manolios P (2000) Correctness of pipelined machines. In: Hunt WA Jr, Johnson SD (eds) Formal methods in computer-aided design \u2013 FMCAD 2000, vol 1954 of LNCS. Springer, Berlin, pp 161\u2013178"},{"key":"5_CR10_5","unstructured":"Manolios P (2001) Mechanical verification of reactive systems. PhD thesis, University of Texas at Austin. See URL http:\/\/www.ccs.neu.edu\/~pete\/research.html"},{"key":"5_CR11_5","series-title":"LNCS","first-page":"304","volume-title":"12th IFIP WG 10.5 advanced research working conference, CHARME 2003","author":"P Manolios","year":"2003","unstructured":"Manolios P (2003) A compositional theory of refinement for branching time. In: Geist D, Tronci E (eds) 12th IFIP WG 10.5 advanced research working conference, CHARME 2003, vol 2860 of LNCS. Springer, Berlin, pp 304\u2013318"},{"key":"5_CR12_5","series-title":"LNCS Series","volume-title":"hardware verification","author":"P Manolios","year":"2006","unstructured":"Manolios P (2006) Refinement and theorem proving. International school on formal methods for the design of computer, communication, and software systems: hardware verification, LNCS Series. Springer, Berlin"},{"key":"5_CR13_5","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1109\/DATE.2004.1268844","volume-title":"Design, automation and test in Europe conference and exposition (DATE\u201904)","author":"P Manolios","year":"2004","unstructured":"Manolios P, Srinivasan SK (2004) Automatic verification of safety and liveness for xscale-like processor models using web refinements. In: Design, automation and test in Europe conference and exposition (DATE\u201904). IEEE Computer Society, Washington, DC, pp 168\u2013175"},{"key":"5_CR14_5","first-page":"863","volume-title":"International conference on computer-aided design (ICCAD\u201905)","author":"P Manolios","year":"2005","unstructured":"Manolios P, Srinivasan SK (2005a) A complete compositional reasoning framework for the efficient verification of pipelined machines. In: International conference on computer-aided design (ICCAD\u201905). IEEE Computer Society, Washington, DC, pp 863\u2013870"},{"key":"5_CR15_5","first-page":"188","volume-title":"Formal methods and models for co-design (MEMOCODE\u201905)","author":"P Manolios","year":"2005","unstructured":"Manolios P, Srinivasan SK (2005b) A computationally efficient method based on commitment refinement maps for verifying pipelined machines. In: Formal methods and models for co-design (MEMOCODE\u201905). IEEE, New York, pp 188\u2013197"},{"key":"5_CR16_5","doi-asserted-by":"publisher","first-page":"1304","DOI":"10.1109\/DATE.2005.257","volume-title":"Design, automation and test in Europe (DATE\u201905)","author":"P Manolios","year":"2005","unstructured":"Manolios P, Srinivasan SK (2005c) Refinement maps for efficient verification of processor models. In: Design, automation and test in Europe (DATE\u201905). IEEE Computer Society, Washington, DC, pp 1304\u20131309"},{"key":"5_CR17_5","first-page":"855","volume-title":"International conference on computer-aided design (ICCAD\u201905)","author":"P Manolios","year":"2005","unstructured":"Manolios P, Srinivasan SK (2005d) Verification of executable pipelined machines with bit-level interfaces. In: International conference on computer-aided design (ICCAD\u201905). IEEE Computer Society, Washington, DC, pp 855\u2013862"},{"issue":"4","key":"5_CR18_5","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1109\/TVLSI.2008.918120","volume":"16","author":"P Manolios","year":"2008","unstructured":"Manolios P, Srinivasan SK (2008) A refinement-based compositional reasoning framework for pipelined machine verification. IEEE Trans VLSI Syst 16(4):353\u2013364","journal-title":"IEEE Trans VLSI Syst"},{"key":"5_CR19_5","series-title":"of Lecture notes in computer science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-540-72788-0_3","volume-title":"International conference theory and applications of satisfiability testing (SAT\u201907)","author":"P Manolios","year":"2007","unstructured":"Manolios P, Vroon D (2007) Efficient circuit to cnf conversion. In: Marques-Silva J, Sakallah KA (eds) International conference theory and applications of satisfiability testing (SAT\u201907), vol 4501 of Lecture notes in computer science. Springer, Berlin, pp 4\u20139"},{"key":"5_CR20_5","doi-asserted-by":"publisher","first-page":"786","DOI":"10.1109\/ICCAD.2006.320121","volume-title":"International conference on computer-aided design (ICCAD\u201906)","author":"P Manolios","year":"2006","unstructured":"Manolios P, Srinivasan SK, Vroon D (2006a) Automatic memory reductions for RTL model verification. In: Hassoun S (ed) International conference on computer-aided design (ICCAD\u201906). ACM, New York, NY, pp 786\u2013793"},{"key":"5_CR21_5","unstructured":"Manolios P, Srinivasan SK, Vroon D (2006b) BAT: the bit-level analysis tool. Available from http:\/\/www.ccs.neu.edu\/~pete\/bat\/"},{"key":"5_CR22_5","unstructured":"Manolios P, Srinivasan SK, Vroon D (2007a) BAT: the bit-level analysis tool. In: International conference computer aided verification (CAV\u201907)"},{"key":"5_CR23_5","series-title":"Lecture notes in computer science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-540-71209-1_26","volume-title":"Tools and algorithms for the construction and analysis of systems, TACAS","author":"P Manolios","year":"2007","unstructured":"Manolios P, Oms MG, Valls SO (2007b) Checking pedigree consistency with PCS. In: Tools and algorithms for the construction and analysis of systems, TACAS, vol 4424 of Lecture notes in computer science. Springer, Berlin, pp 339\u2013342"},{"key":"5_CR24_5","first-page":"61","volume-title":"Proceedings of the ACM\/SIGSOFT international symposium on software testing and analysis, ISSTA","author":"P Manolios","year":"2007","unstructured":"Manolios P, Vroon D, Subramanian G (2007c) Automating component-based system assembly. In: Proceedings of the ACM\/SIGSOFT international symposium on software testing and analysis, ISSTA. ACM, New York, NY, pp 61\u201372"},{"key":"5_CR25_5","volume-title":"Communication and concurrency","author":"R Milner","year":"1990","unstructured":"Milner R (1990) Communication and concurrency. Prentice-Hall, Upper Saddle River, NJ"},{"key":"5_CR26_5","doi-asserted-by":"crossref","unstructured":"Namjoshi KS (1997) A simple characterization of stuttering bisimulation. In: 17th Conference on foundations of software technology and theoretical computer science, vol 1346 of LNCS, pp 284\u2013296","DOI":"10.1007\/BFb0058037"},{"key":"5_CR27_5","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/978-1-4757-3188-0_9","volume-title":"Computer-aided reasoning: ACL2 case studies","author":"J Sawada","year":"2000","unstructured":"Sawada J (2000) Verification of a simple pipelined machine model. In: Kaufmann M, Manolios P, Moore JS (eds) Computer-aided reasoning: ACL2 case studies. Kluwer, Dordrecht, pp 137\u2013150"}],"container-title":["Design and Verification of Microprocessor Systems for High-Assurance Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-4419-1539-9_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,18]],"date-time":"2023-02-18T03:22:04Z","timestamp":1676690524000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-1-4419-1539-9_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9781441915382","9781441915399"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-1-4419-1539-9_5","relation":{},"subject":[],"published":{"date-parts":[[2010]]},"assertion":[{"value":"23 January 2010","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}