{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T17:08:16Z","timestamp":1742404096319},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540223429"},{"type":"electronic","value":"9783540278139"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27813-9_31","type":"book-chapter","created":{"date-parts":[[2010,9,14]],"date-time":"2010-09-14T04:57:57Z","timestamp":1284440277000},"page":"401-413","source":"Crossref","is-referenced-by-count":31,"title":["QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings"],"prefix":"10.1007","author":[{"given":"Ganesh","family":"Gopalakrishnan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yue","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hemanthkumar","family":"Sivaraj","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"12","key":"31_CR1","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"S.V. Adve","year":"1996","unstructured":"Adve, S.V., Gharachorloo, K.: Shared memory consistency models: A tutorial. Computer\u00a029(12), 66\u201376 (1996)","journal-title":"Computer"},{"key":"31_CR2","unstructured":"A Formal Specification of Intel(R) Itanium(R) Processor Family Memory Ordering (2002), http:\/\/www.intel.com\/design\/itanium\/downloads\/251429.htm"},{"issue":"4","key":"31_CR3","doi-asserted-by":"publisher","first-page":"1208","DOI":"10.1137\/S0097539794279614","volume":"26","author":"P.B. Gibbons","year":"1997","unstructured":"Gibbons, P.B., Korach, E.: Testing shared memories. SIAM Journal on Computing\u00a026(4), 1208\u20131244 (1997)","journal-title":"SIAM Journal on Computing"},{"issue":"9","key":"31_CR4","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"28","author":"L. Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Transactions on Computers\u00a0C-28(9), 690\u2013691 (1979)","journal-title":"IEEE Transactions on Computers"},{"key":"31_CR5","doi-asserted-by":"crossref","unstructured":"Cantin, J.F., Lipasti, M.H., Smith, J.E.: The complexity of verifying memory coherence. In: Proceedings of the fifteenth annual ACM symposium on Parallel algorithms and architectures (SPAA), San Diego, pp. 254\u2013255 (2003)","DOI":"10.1145\/777412.777457"},{"key":"31_CR6","unstructured":"Sipser, M.: Introduction to the Theory of Computation. PWS Publishing Company (1997)"},{"key":"31_CR7","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic\u00a05, 56\u201368 (1940)","journal-title":"Journal of Symbolic Logic"},{"key":"31_CR8","unstructured":"Hanna, F.K., Daeche, N.: Specification and verification using higher-order logic. In: 7th International Conference on Computer Hardware Description Languages and their Applications, pp. 418\u2013419 (1985)"},{"key":"31_CR9","unstructured":"Gordon, M.: Why higher-order logic is a good formalism for specifying and verifying hardware. In: Formal aspects of VLSI design (1986)"},{"key":"31_CR10","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: Proceedings of International Conference on Computer Aided Design (November 2002)","DOI":"10.1145\/774572.774637"},{"key":"31_CR11","first-page":"38","volume-title":"Research on Integrated Systems","author":"D.L. Dill","year":"1993","unstructured":"Dill, D.L., Park, S., Nowatzyk, A.: Formal specification of abstract memory models. In: Research on Integrated Systems, pp. 38\u201352. MIT Press, Cambridge (1993)"},{"key":"31_CR12","volume-title":"The SPARC Architecture Manual \u2013 Version 9","author":"D.L. Weaver","year":"1994","unstructured":"Weaver, D.L., Germond, T.: The SPARC Architecture Manual \u2013 Version 9. P T R Prentice-Hall, Englewood Cliffs (1994)"},{"key":"31_CR13","series-title":"Lecture Notes in Computer Science","first-page":"522","volume-title":"Computer Aided Verification","author":"D.L. Dill","year":"1993","unstructured":"Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol.\u00a0663, pp. 522\u2013525. Springer, Heidelberg (1993)"},{"key":"31_CR14","doi-asserted-by":"crossref","unstructured":"Chatterjee, P., Gopalakrishnan, G.: Towards a formal model of shared memory consistency for Intel Itanium. In: ICCD, pp. 515\u2013518 (2001)","DOI":"10.1109\/ICCD.2001.955081"},{"key":"31_CR15","doi-asserted-by":"crossref","unstructured":"Yang, Y., Gopalakrishnan, G., Lindstrom, G., Slind, K.: Nemos: A framework for axiomatic and executable specifications of memory consistency models. In: International Parallel and Distributed Processing Symposium (2004)","DOI":"10.1109\/IPDPS.2004.1302944"},{"key":"31_CR16","unstructured":"Personal Communication with Yuan B. Yu."},{"issue":"2","key":"31_CR17","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"31_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-540-39724-3_9","volume-title":"Correct Hardware Design and Verification Methods","author":"Y. Yang","year":"2003","unstructured":"Yang, Y., Gopalakrishnan, G., Lindstrom, G., Slind, K.: Analyzing the intel itanium memory ordering rules using logic programming and SAT. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 81\u201395. Springer, Heidelberg (2003)"},{"key":"31_CR19","doi-asserted-by":"crossref","unstructured":"Condon, A., Hill, M., Plakal, M., Sorin, D.: Using Lamport Clocks to Reason About Relaxed Memory Models. In: Fifth International Symposium On High Performance Computer Architecture (HPCA-5) (January 1999)","DOI":"10.1109\/HPCA.1999.744379"},{"key":"31_CR20","doi-asserted-by":"crossref","unstructured":"Seshia, S.A., Lahiri, S.K., Bryant, R.E.: A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. In: Design Automation Conference (DAC), pp. 425\u2013430 (2003)","DOI":"10.1145\/775832.775945"},{"key":"31_CR21","volume-title":"Programming Language Theory and Implementation","author":"M. Gordon","year":"1993","unstructured":"Gordon, M.: Programming Language Theory and Implementation. Prentice-Hall, Englewood Cliffs (1993)"},{"key":"31_CR22","unstructured":"http:\/\/www.ocaml.org"},{"key":"31_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. Een","year":"2004","unstructured":"Een, N.: Satzoo Incremental SAT Solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004), http:\/\/www.math.chalmers.se\/~een\/Satzoo\/AnExtensibleSATsolver.ps.gz"},{"key":"31_CR24","unstructured":"http:\/\/www.cs.wisc.edu\/~zandy\/ckpt\/"},{"key":"31_CR25","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: The quest for efficient boolean satisfiability solvers. In: Computer Aided Verification. LNCS, vol.\u00a02402, pp. 17\u201336 (2002)","DOI":"10.1007\/3-540-45657-0_2"},{"key":"31_CR26","unstructured":"http:\/\/www.cs.utah.edu\/formalverification"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27813-9_31.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:22:04Z","timestamp":1605759724000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27813-9_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540223429","9783540278139"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27813-9_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}