{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:55:23Z","timestamp":1725562523904},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642150562"},{"type":"electronic","value":"9783642150579"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15057-9_1","type":"book-chapter","created":{"date-parts":[[2010,8,11]],"date-time":"2010-08-11T07:01:15Z","timestamp":1281510075000},"page":"1-24","source":"Crossref","is-referenced-by-count":12,"title":["Towards Scalable Modular Checking of User-Defined Properties"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Ball","sequence":"first","affiliation":[]},{"given":"Brian","family":"Hackett","sequence":"additional","affiliation":[]},{"given":"Shuvendu K.","family":"Lahiri","sequence":"additional","affiliation":[]},{"given":"Shaz","family":"Qadeer","sequence":"additional","affiliation":[]},{"given":"Julien","family":"Vanegue","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Aiken, A., Bugrara, S., Dillig, I., Dillig, T., Hackett, B., Hawkins, P.: An overview of the Saturn project. In: Workshop on Program Analysis for Software Tools and Engineering (PASTE 2007), pp. 43\u201348 (2007)","DOI":"10.1145\/1251535.1251543"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/978-3-540-73368-3_41","volume-title":"Computer Aided Verification","author":"D. Babic","year":"2007","unstructured":"Babic, D., Hu, A.J.: Structural abstraction of software verification conditions. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 366\u2013378. Springer, Heidelberg (2007)"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Programming Language Design and Implementation (PLDI 2001), pp. 203\u2013213 (2001)","DOI":"10.1145\/378795.378846"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-540-71209-1_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Chatterjee","year":"2007","unstructured":"Chatterjee, S., Lahiri, S.K., Qadeer, S., Rakamari\u0107, Z.: A reachability predicate for analyzing low-level software. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 19\u201333. Springer, Heidelberg (2007)"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Condit, J., Hackett, B., Lahiri, S.K., Qadeer, S.: Unifying type checking and property checking for low-level code. In: Principles of Programming Languages (POPL 2009), pp. 302\u2013314 (2009)","DOI":"10.1145\/1594834.1480921"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A Unified Lattice Model for the Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Principles of Programming Languages (POPL 1977), pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"P. Cousot","year":"2005","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The ASTRE\u00c9 Analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 21\u201330. Springer, Heidelberg (2005)"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Dahlweid, M., Moskal, M., Santen, T., Tobies, S., Schulte, W.: Vcc: Contract-based modular verification of concurrent c. In: International Conference on Software Engineering (ICSE 2009), Companion Volume, pp. 429\u2013430 (2009)","DOI":"10.1109\/ICSE-COMPANION.2009.5071046"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Das, M., Lerner, S., Seigle, M.: ESP: Path-Sensitive Program Verification in Polynomial Time. In: Programming Language Design and Implementation (PLDI 2002), pp. 57\u201368 (2002)","DOI":"10.1145\/512529.512538"},{"key":"1_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-540-73595-3_13","volume-title":"Automated Deduction \u2013 CADE-21","author":"L. Moura de","year":"2007","unstructured":"de Moura, L., Bjorner, N.: Efficient Incremental E-matching for SMT Solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 183\u2013198. Springer, Heidelberg (2007)"},{"key":"1_CR12","unstructured":"DeLine, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft Research (2005)"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Engler, D.R., Ashcraft, K.: RacerX: effective, static detection of race conditions and deadlocks. In: Symposium on Operating Systems Principles (SOSP 2003), pp. 237\u2013252 (2003)","DOI":"10.1145\/945445.945468"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Engler, D.R., Chelf, B., Chou, A., Hallem, S.: Checking system rules using system-specific, programmer-written compiler extensions. In: Operating Systems Design And Implementation (OSDI 2000), pp. 1\u201316 (2000)","DOI":"10.21236\/ADA419626"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Freund, S.N.: Type-based race detection for java. In: PLDI, pp. 219\u2013232 (2000)","DOI":"10.1145\/349299.349328"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45251-6_29","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"C. Flanagan","year":"2001","unstructured":"Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC\/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, pp. 500\u2013517. Springer, Heidelberg (2001)"},{"key":"1_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: Programming Language Design and Implementation (PLDI 2002), pp. 234\u2013245 (2002)","DOI":"10.1145\/512529.512558"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Hackett, B., Das, M., Wang, D., Yang, Z.: Modular checking for buffer overflows in the large. In: International Conference on Software Engineering (ICSE 2006), pp. 232\u2013241 (2006)","DOI":"10.1145\/1134285.1134319"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Principles of Programming Languages (POPL 2002), pp. 58\u201370 (2002)","DOI":"10.1145\/503272.503279"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Back to the future: revisiting precise program verification using SMT solvers. In: Principles of Programming Languages (POPL 2008), pp. 171\u2013182 (2008)","DOI":"10.1145\/1328438.1328461"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1007\/978-3-642-02658-4_37","volume-title":"CAV 2009","author":"S.K. Lahiri","year":"2009","unstructured":"Lahiri, S.K., Qadeer, S., Galeotti, J.P., Voung, J.W., Wies, T.: Intra-module inference. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 493\u2013508. Springer, Heidelberg (2009)"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Pratikakis, P., Foster, J.S., Hicks, M.W.: LOCKSMITH: context-sensitive correlation analysis for race detection. In: Programming Language Design and Implementation (PLDI 2006), pp. 320\u2013331 (2006)","DOI":"10.1145\/1133981.1134019"},{"key":"1_CR23","unstructured":"Vanegue, J.: Zero-sized heap allocations vulnerability analysis"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Voung, J.W., Jhala, R., Lerner, S.: RELAY: static race detection on millions of lines of code. In: Foundations of Software Engineering (FSE 2007), pp. 205\u2013214 (2007)","DOI":"10.1145\/1287624.1287654"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15057-9_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T03:00:59Z","timestamp":1606186859000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15057-9_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642150562","9783642150579"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15057-9_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}