{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,7]],"date-time":"2026-10-07T22:17:56Z","timestamp":1791411476892,"version":"4.3.3"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540227915","type":"print"},{"value":"9783540278641","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27864-1_2","type":"book-chapter","created":{"date-parts":[[2010,9,16]],"date-time":"2010-09-16T16:35:37Z","timestamp":1284654937000},"page":"2-18","source":"Crossref","is-referenced-by-count":43,"title":["The Blast Query Language for Software Verification"],"prefix":"10.1007","author":[{"given":"Dirk","family":"Beyer","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Adam J.","family":"Chlipala","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ranjit","family":"Jhala","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"2_CR1","first-page":"1","volume-title":"Proc. POPL","author":"T. Ball","year":"2002","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: Debugging system software via static analysis. In: Proc. POPL, pp. 1\u20133. ACM, New York (2002)"},{"key":"2_CR2","unstructured":"Ball, T., Rajamani, S.K.: SLIC: A specification language for interface checking (of C). Technical Report MSR-TR-2001-21, Microsoft Research (2002)"},{"key":"2_CR3","first-page":"216","volume-title":"Proc. WCRE","author":"D. Beyer","year":"2003","unstructured":"Beyer, D., Noack, A., Lewerentz, C.: Simple and efficient relational querying of software structures. In: Proc. WCRE, pp. 216\u2013225. IEEE, Los Alamitos (2003)"},{"key":"2_CR4","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1145\/586110.586142","volume-title":"Proc. CCS","author":"H. Chen","year":"2002","unstructured":"Chen, H., Wagner, D.: MOPS: An infrastructure for examining security properties of software. In: Proc. CCS, pp. 235\u2013244. ACM, New York (2002)"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/10722468_13","volume-title":"SPIN Model Checking and Software Verification","author":"J.C. Corbett","year":"2000","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Robby: A language framework for expressing checkable properties of dynamic software. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 205\u2013223. Springer, Heidelberg (2000)"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Goldsmith, S., O\u2019Callahan, R., Aiken, A.: Lightweight instrumentation from relational queries on program traces. Technical Report CSD-04-1315, UC Berkeley (2004)","DOI":"10.21236\/ADA603315"},{"key":"2_CR7","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1145\/512529.512539","volume-title":"Proc. PLDI","author":"S. Hallem","year":"2002","unstructured":"Hallem, S., Chelf, B., Xie, Y., Engler, D.: A system and language for building system-specific static analyses. In: Proc. PLDI, pp. 69\u201382. ACM, New York (2002)"},{"key":"2_CR8","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1145\/964001.964021","volume-title":"Proc. POPL","author":"T.A. Henzinger","year":"2004","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Proc. POPL, pp. 232\u2013244. ACM, New York (2004)"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/3-540-45657-0_45","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Necula, G.C., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 526\u2013538. Springer, Heidelberg (2002)"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","first-page":"332","volume-title":"Verification: Theory and Practice","author":"T.A. Henzinger","year":"2004","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sanvido, M.A.A.: Extreme model checking. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol.\u00a02772, pp. 332\u2013358. Springer, Heidelberg (2004)"},{"key":"2_CR11","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1145\/503272.503279","volume-title":"Proc. POPL","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. POPL, pp. 58\u201370. ACM, New York (2002)"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/10722468_8","volume-title":"SPIN Model Checking and Software Verification","author":"G.J. Holzmann","year":"2000","unstructured":"Holzmann, G.J.: Logic verification of ANSI-C code with SPIN. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 131\u2013147. Springer, Heidelberg (2000)"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/BFb0053381","volume-title":"ECOOP \u201997 - Object-Oriented Programming","author":"G. Kiczales","year":"1997","unstructured":"Kiczales, G., Lamping, J., Mendhekar, A., Maeda, C., Lopes, C.V., Loingtier, J.-M., Irwin, J.: Aspect-oriented programming. In: Aksit, M., Matsuoka, S. (eds.) ECOOP 1997. LNCS, vol.\u00a01241, pp. 220\u2013242. Springer, Heidelberg (1997)"},{"issue":"1-3","key":"2_CR14","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/S0167-6423(99)00030-1","volume":"37","author":"K.L. McMillan","year":"2000","unstructured":"McMillan, K.L.: A methodology for hardware verification using compositional model checking. Science of Computer Programming\u00a037(1-3), 279\u2013309 (2000)","journal-title":"Science of Computer Programming"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction","author":"G.C. Necula","year":"2002","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate language and tools for analysis and transformation of C programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol.\u00a02304, pp. 213\u2013228. Springer, Heidelberg (2002)"},{"issue":"1","key":"2_CR16","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1109\/TSE.1986.6312929","volume":"12","author":"R.E. Strom","year":"1986","unstructured":"Strom, R.E., Yemini, S.: Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Software Engineering\u00a012(1), 157\u2013171 (1986)","journal-title":"IEEE Trans. Software Engineering"},{"key":"2_CR17","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1145\/996841.996846","volume-title":"Proc. PLDI","author":"E. Yahav","year":"2004","unstructured":"Yahav, E., Ramalingam, G.: Verifying safety properties using separation and heterogeneous abstractions. In: Proc. PLDI, pp. 25\u201334. ACM, New York (2004)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27864-1_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,3]],"date-time":"2023-06-03T10:40:12Z","timestamp":1685788812000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27864-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540227915","9783540278641"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27864-1_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}