{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,7]],"date-time":"2023-01-07T15:17:34Z","timestamp":1673104654353},"reference-count":39,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3619,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,9]]},"DOI":"10.1016\/s1571-0661(05)80002-7","type":"journal-article","created":{"date-parts":[[2005,5,20]],"date-time":"2005-05-20T13:21:17Z","timestamp":1116595277000},"page":"378-404","source":"Crossref","is-referenced-by-count":6,"title":["Some Lessons from Using Static Analysis and Software Model Checking for Bug Finding"],"prefix":"10.1016","volume":"89","author":[{"given":"Madanlal","family":"Musuvathi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dawson","family":"Engler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(05)80002-7_BIB1","series-title":"SPIN 2000 Workshop on Model Checking of Software (LNCS 1885, Springer)","article-title":"Bebop: A symbolic model checker for boolean programs","author":"Ball","year":"2000"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB2","series-title":"Proceedings of the SIGPLAN '01 Conference on Programming Language Design and Implementation","article-title":"Automatic predicate abstraction of C programs","author":"Ball","year":"2001"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB3","series-title":"IEEE International Conference on Automated Software Engineering (ASE)","article-title":"Model checking programs","author":"Brat","year":"2000"},{"issue":"7","key":"10.1016\/S1571-0661(05)80002-7_BIB4","first-page":"775","article-title":"A static analyzer for finding dynamic programming errors","volume":"30","author":"Bush","year":"2000","journal-title":"Software: Practice and Experience"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB5","series-title":"Proceedings of International Conference on Software Engineering (ICSE)","article-title":"Software model checking in practice: An industrial case study","author":"Chandra","year":"2002"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB6","series-title":"Invited Paper. PASTE 2002","article-title":"How to write system-specific, static checkers in metal","author":"Chelf","year":"2002"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB7","series-title":"Ninth International Conference on Architecture Support for Programming Languages and Operating Systems","article-title":"Using meta-level compilation to check FLASH protocol code","author":"Chou","year":"2000"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB8","series-title":"SIGPLAN Conference on Programming Language Design and Implementation","first-page":"345","article-title":"Automatically closing open reactive programs","author":"Colby","year":"1998"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB9","series-title":"ICSE 2000","article-title":"Bandera: Extracting finite-state models from Java source code","author":"Corbett","year":"2000"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB10","article-title":"Ad Hoc On Demand Distance Vector (AODV) Routing","author":"Perkins","year":"2002","journal-title":"IETF Draft, http:\/\/www.ietf.org\/internet-drafts\/draft-ietf-manet-aodv-10.txt"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB11","series-title":"Conference on Programming Language Design and Implementation","article-title":"Esp: Path-sensitive program verification in polynomial time","author":"Das","year":"2002"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB12","series-title":"Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation","article-title":"Enforcing high-level protocols in low-level software","author":"DeLine","year":"2001"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB13","first-page":"522","article-title":"Protocol verification as a hardware design aid","author":"Dill","year":"1992","journal-title":"IEEE International Conference on Computer Design: VLSI in Computers and Processors"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB14","series-title":"Proceedings of Operating Systems Design and Implementation (OSDI)","article-title":"Checking system rules using system-specific, programmer-written compiler extensions","author":"Engler","year":"2000"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB15","series-title":"Proceedings of the Eighteenth ACM Symposium on Operating Systems Principles","article-title":"Bugs as deviant behavior: A general approach to inferring errors in systems code","author":"Engler","year":"2001"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB16","unstructured":"Erik Nordstrom et al. AODV-UU Implementation. http:\/\/user.it.uu.se\/henrikl\/aodv\/."},{"key":"10.1016\/S1571-0661(05)80002-7_BIB17","series-title":"2002 Conference on Programming Language Design and Implementation","first-page":"234","article-title":"Extended static checking for Java","author":"Flanagan","year":"2002"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB18","series-title":"Proceedings of the SIGPLAN '99 Conference on Programming Language Design and Implementation","article-title":"A theory of type qualifiers","author":"Foster","year":"1999"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB19","series-title":"Proceedings of the 24th ACM Symposium on Principles of Programming Languages","article-title":"Model Checking for Programming Languages using VeriSoft","author":"Godefroid","year":"1997"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB20","series-title":"SIGPLAN Conference on Programming Language Design and Implementation","article-title":"A system and language for building system-specific, static analyses","author":"Hallem","year":"2002"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB21","series-title":"Invited Paper. Proc. PSTV\/FORTE99 Publ. Kluwer","article-title":"Software model checking: Extracting verification models from source code","author":"Holzmann","year":"1999"},{"issue":"5","key":"10.1016\/S1571-0661(05)80002-7_BIB22","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","article-title":"The model checker SPIN","volume":"23","author":"Holzmann","year":"1997","journal-title":"Software Engineering"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB23","unstructured":"Luke Klein-Berndt and et.al. Kernel AODV Implementation. http:\/\/w3.antd.nist.gov\/wctg\/aodv_kernel\/."},{"key":"10.1016\/S1571-0661(05)80002-7_BIB24","series-title":"Proceedings of the 21st International Symposium on Computer Architecture","article-title":"The Stanford FLASH multiprocessor","author":"Kuskin","year":"1994"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB25","article-title":"ESC\/Java user's manual","author":"Leino","year":"2001","journal-title":"Technical note 2000-002, Compaq Systems Research Center"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB26","series-title":"Proceedings of the 28th Annual International Symposium on Computer Architecture","article-title":"A simple method for extracting models from protocol code","author":"Lie","year":"2001"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB27","unstructured":"F. Lilieblad and et.al. Mad-hoc AODV Implementation. http:\/\/mad-hoc.flyinglinux.net\/."},{"key":"10.1016\/S1571-0661(05)80002-7_BIB28","series-title":"IEEE Wireless Communications and Networking Conference","article-title":"A large-scale testbed for reproducible ad hoc protocol evaluations","author":"Lundgren","year":"2002"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB29","series-title":"Proceedings of the Fifth Symposium on Operating Systems Design and Implementation","article-title":"CMC: A Pragmatic Approach to Model Checking Real Code","author":"Musuvathi","year":"2002"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB30","series-title":"Symposium on Principles of Programming Languages","first-page":"128","article-title":"CCured: type-safe retrofitting of legacy code","author":"Necula","year":"2002"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB31","series-title":"Proceedings of the 8th ACM Symposium on Parallel Algorithsm and Architectures","first-page":"288","article-title":"Verification of FLASH cache coherence protocol by aggregation of distributed transactions","author":"Park","year":"1996"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB32","series-title":"22nd International Conference on Software Engineering (ICSE)","article-title":"Verification of time partitioning in the deos real-time scheduling kernel","author":"Penix","year":"2000"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB33","article-title":"Personal communication","author":"Pincus","year":"2003","journal-title":"PREfix did not target data races because of the user-interface complexities in reporting and diagnosis"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB34","article-title":"Transmission control protocol","author":"Postel","year":"1981","journal-title":"RFC 793, USC\/Information Sciences Institute"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB35","series-title":"USENIX Winter","first-page":"97","article-title":"WARLOCK - a static data race analysis tool","author":"Sterling","year":"1993"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB36","series-title":"IFIP TC6\/WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification","article-title":"A New Scheme for Memory-Efficient Probabilistic Verification","author":"Stern","year":"1996"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB37","unstructured":"The User-mode Linux Kernel. http:\/\/user-mode-linux.sourceforge.net\/."},{"key":"10.1016\/S1571-0661(05)80002-7_BIB38","series-title":"IEEE Symposium on Security and Privacy","article-title":"Intrusion detection via static analysis","author":"Wagner","year":"2001"},{"key":"10.1016\/S1571-0661(05)80002-7_BIB39","series-title":"The 2000 Network and Distributed Systems Security Conference. San Diego, CA","article-title":"A first step towards automated detection of buffer overrun vulnerabilities","author":"Wagner","year":"2000"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105800027?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105800027?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,1,26]],"date-time":"2019-01-26T10:50:28Z","timestamp":1548499828000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105800027"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,9]]},"references-count":39,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,9]]}},"alternative-id":["S1571066105800027"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(05)80002-7","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,9]]}}}