{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,6]],"date-time":"2025-04-06T13:22:23Z","timestamp":1743945743676,"version":"3.28.0"},"reference-count":31,"publisher":"IEEE Comput. Soc","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/secpri.2002.1004369","type":"proceedings-article","created":{"date-parts":[[2005,8,25]],"date-time":"2005-08-25T03:23:34Z","timestamp":1124940214000},"page":"160-173","source":"Crossref","is-referenced-by-count":27,"title":["Improving computer security using extended static checking"],"prefix":"10.1109","author":[{"given":"B.V.","family":"Chess","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"article-title":"Programming Perl","year":"1996","author":"wall","key":"ref31"},{"key":"ref30","article-title":"A first step towards automated detection of buffer overrun vulnerabilities","author":"wagner","year":"2000","journal-title":"Proc Symp Network and Distributed System Security"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/193173.195297"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360220"},{"article-title":"JavaScript: The Definitive Guide","year":"1996","author":"flanagan","key":"ref12"},{"article-title":"C, a Reference Manual","year":"1995","author":"harbison","key":"ref13"},{"key":"ref14","first-page":"125","article-title":"Fast detection of memory leaks and access errors","author":"hastings","year":"1992","journal-title":"Proceedings of the Winter USENIX Conference"},{"journal-title":"The Java security home page On the web as","year":"0","key":"ref15"},{"key":"ref16","article-title":"Backwards-compatible bounds checking for arrays and pointers in c programs","author":"jones","year":"1997","journal-title":"Third International Workshop on Automated Debugging"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/185403.185412"},{"key":"ref18","article-title":"Statically detecting likely buffer overflow vulnerabilities","author":"larochelle","year":"2001","journal-title":"Proceedings of the 2001 USENIX Security Symposium"},{"journal-title":"Toward Reliable Modular Programs","year":"1995","author":"leino","key":"ref19"},{"journal-title":"The Simplify home page Compaq Systems Research Center","year":"0","key":"ref28"},{"volume":"1322","journal-title":"Linux capabilities vulnerability The bugtraq mailing list","year":"0","key":"ref4"},{"key":"ref27","article-title":"Detecting format string vulnerabilities with type qualifiers","author":"shankar","year":"2001","journal-title":"Proceedings of the 10th USENIX Security Symposium"},{"volume":"843","journal-title":"RSAREF buffer overflow The bugtraq mailing list","year":"0","key":"ref3"},{"key":"ref6","article-title":"An overview of the extended static checking system","author":"detlefs","year":"1995","journal-title":"The first Formal Methods in Software Practice workshop collocated with ISSTA 96"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1109\/ACSAC.2000.898880"},{"key":"ref5","article-title":"Formatguard: Automatic protection from printf format string vulnerabilities","author":"cowan","year":"2001","journal-title":"Proceedings of the USENIX Security Symposium"},{"journal-title":"Simplify the ESC theorem prover Unpublished manuscript","year":"1996","author":"detlefs","key":"ref8"},{"key":"ref7","article-title":"Extended static checking","author":"detlefs","year":"1998","journal-title":"Technical Report 159 Compaq Systems Research Center"},{"key":"ref2","first-page":"132","article-title":"Checking for race conditions in file accesses","volume":"9","author":"bishop","year":"1996","journal-title":"Computing Systems"},{"article-title":"A Discipline of Programming","year":"1976","author":"dijkstra","key":"ref9"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"ref20","article-title":"Checking Java programs via guarded commands","author":"leino","year":"1999","journal-title":"Technical Report 1999-02 Compaq Systems Research Center"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"ref21","article-title":"Correct compilation of control structures","author":"manasse","year":"1984","journal-title":"Technical Report AT&T Bell Laboratories"},{"journal-title":"C Formalised in HOL","year":"1998","author":"norrish","key":"ref24"},{"key":"ref23","article-title":"Pointers are bad, records are bad, but record-pointers are good","author":"nelson","year":"1982","journal-title":"Technical Report Xerox Palo Alto Research Center"},{"journal-title":"libformat On the web as","year":"0","author":"robbins","key":"ref26"},{"key":"ref25","first-page":"41","volume":"rhsa 1999","year":"1999","journal-title":"File access problems in lpr\/lpd Redhat Security Advisory"}],"event":{"name":"2002 IEEE Symposium on Security and Privacy","acronym":"SECPRI-02","location":"Berkeley, CA, USA"},"container-title":["Proceedings 2002 IEEE Symposium on Security and Privacy"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/7873\/21681\/01004369.pdf?arnumber=1004369","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,14]],"date-time":"2017-03-14T01:32:13Z","timestamp":1489455133000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1004369\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":31,"URL":"https:\/\/doi.org\/10.1109\/secpri.2002.1004369","relation":{},"subject":[]}}