{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T12:10:03Z","timestamp":1737115803001,"version":"3.33.0"},"reference-count":80,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007,6]]},"DOI":"10.1109\/tase.2007.55","type":"proceedings-article","created":{"date-parts":[[2007,6,20]],"date-time":"2007-06-20T14:56:10Z","timestamp":1182351370000},"page":"3-20","source":"Crossref","is-referenced-by-count":30,"title":["Varieties of Static Analyzers: A Comparison with ASTREE"],"prefix":"10.1109","author":[{"given":"Patrick","family":"COUSOT","sequence":"first","affiliation":[]},{"given":"Radhia","family":"COUSOT","sequence":"additional","affiliation":[]},{"given":"Jerome","family":"FERET","sequence":"additional","affiliation":[]},{"given":"Antoine","family":"MINE","sequence":"additional","affiliation":[]},{"given":"Laurent","family":"MAUBORGNE","sequence":"additional","affiliation":[]},{"given":"David","family":"MONNIAUX","sequence":"additional","affiliation":[]},{"given":"Xavier","family":"RIVAL","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"79","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.38"},{"key":"78","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2006.11.004"},{"key":"77","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022920129859"},{"key":"35","article-title":"UNO: Static Source Code Checking for User-Defined Properties","author":"holzmann","year":"2002","journal-title":"6th World Conf on Integrated Design and Process Technology IDPT '02"},{"key":"36","article-title":"The SPIN MODEL CHECKER","author":"holzmann","year":"2003","journal-title":"Primer and Reference Manual"},{"journal-title":"Safer C Developing for High-Integrity and Safety-Critical Systems","year":"1995","author":"hatten","key":"33"},{"key":"34","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"journal-title":"PC-lint?\/ FlexeLint? Value Tracking","year":"0","key":"39"},{"key":"37","doi-asserted-by":"publisher","DOI":"10.1145\/1108792.1108798"},{"journal-title":"SCADE Suite? The Standard for the Development of Safety-Critical Embedded Software in the Avionics Industry","year":"0","key":"38"},{"year":"0","key":"43"},{"journal-title":"Simulink - Simulation and Model- Based Design","year":"0","key":"42"},{"year":"0","key":"41"},{"journal-title":"CodeSonar A code-analysis tool that identifies","year":"0","author":"grammatech","key":"40"},{"key":"80","article-title":"SafeDrive: Safe and Recoverable Extensions Using Language-Based Techniques","author":"zhou","year":"2006","journal-title":"Operating System Design and Implementation OSDI '06"},{"key":"67","doi-asserted-by":"publisher","DOI":"10.1145\/1062455.1062558"},{"key":"66","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_21"},{"key":"69","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250746"},{"key":"68","doi-asserted-by":"publisher","DOI":"10.1145\/1065887.1065892"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1147\/sj.153.0182"},{"key":"23","first-page":"33","article-title":"Static Analysis of Digital Filters","volume":"2986","author":"feret","year":"2004","journal-title":"LNCS"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_3"},{"key":"25","first-page":"15","article-title":"Multi-Prover Verification of C Programs","volume":"3308","author":"fillia?tre","year":"2004","journal-title":"LNCS"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"27","first-page":"175","article-title":"Polymorphic versus Monomorphic Flow-insensitive Points-to Analysis for C","author":"foster","year":"1824","journal-title":"LNCS"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-1489-x"},{"key":"29","first-page":"196","article-title":"Verifying Invariants Using Theorem Proving","volume":"1102","author":"graf","year":"1996","journal-title":"LNCS"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36377-7_5"},{"key":"2","first-page":"2","article-title":"Checking memory safety with BLAST","volume":"3442","author":"beyer","year":"2005","journal-title":"LNCS"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H"},{"key":"30","doi-asserted-by":"publisher","DOI":"10.1080\/00207168908803778"},{"key":"6","article-title":"Value Lattice Static Analysis, A New Approach to Static Analysis","author":"brew","year":"2001","journal-title":"Dr Dobbs J"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.2007.20"},{"year":"0","key":"32"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1145\/781151.781153"},{"key":"31","first-page":"23","article-title":"Cyclone: A Type-safe Dialect of C","author":"grossman","year":"2005","journal-title":"C\/C++ Users J"},{"year":"0","key":"70"},{"key":"71","doi-asserted-by":"publisher","DOI":"10.1145\/183432.183525"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"72","first-page":"1709","article-title":"Applying Formal Proof Techniques to Avionics Software: A Pragmatic Approach","author":"randimbivololona","year":"1798","journal-title":"LNCS"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.22"},{"key":"73","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36384-X_7"},{"key":"74","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964002"},{"key":"75","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2006.34"},{"key":"76","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996869"},{"year":"0","key":"59"},{"key":"58","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"57","first-page":"5","article-title":"Trace Partitioning in Abstract Interpretation Based Static Analyzer","volume":"3444","author":"mauborgne","year":"2005","journal-title":"LNCS"},{"key":"56","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-8157-6_30"},{"key":"19","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"55","first-page":"59","article-title":"An Overview of Semantics for the Validation of Numerical Programs","volume":"3385","author":"martel","year":"2005","journal-title":"LNCS"},{"key":"17","first-page":"21","article-title":"The ASTRE?E analyser","volume":"3444","author":"cousot","year":"2005","journal-title":"LNCS"},{"key":"18","article-title":"Combination of Abstractions in the ASTRE?E Static Analyzer","author":"cousot","year":"2006","journal-title":"LNCS"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55844-6_142"},{"key":"13","first-page":"106","article-title":"Static determination of dynamic properties of programs","author":"cousot","year":"1976","journal-title":"Int Symp on Programming"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"11","first-page":"168","article-title":"A tool for checking ANSI-C programs","volume":"2988","author":"clarke","year":"2004","journal-title":"LNCS"},{"journal-title":"PMD Applied","year":"2005","author":"copeland","key":"12"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1145\/502039.502041"},{"journal-title":"Static Verification Of Dynamic Properties","year":"0","author":"deutsch","key":"20"},{"journal-title":"Guidelines for the use of the C language in vehicle based systems Software","year":"1998","key":"64"},{"key":"65","first-page":"86","article-title":"The Parallel Implementation of the ASTRe?E Static Analyzer","volume":"3780","author":"monniaux","year":"2005","journal-title":"LNCS"},{"key":"62","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1145\/1134650.1134659","article-title":"Field-Sensitive Value Analysis of Embedded C Programs with Union Types and Pointer Arithmetics","author":"mine?","year":"2006","journal-title":"ACM Conf on Languages Compilers and Tools for Embedded Systems LCTES '2006"},{"key":"63","first-page":"348","article-title":"Symbolic Methods to Enhance the Precision of Numerical","volume":"3855","author":"mine?","year":"2006","journal-title":"LNCS"},{"key":"60","first-page":"3","article-title":"Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors","volume":"2986","author":"mine?","year":"2004","journal-title":"LNCS"},{"key":"61","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"49","doi-asserted-by":"publisher","DOI":"10.1145\/1127577.1127589"},{"key":"48","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_16"},{"key":"45","article-title":"International standard - Programming languages - C, 1999","volume":"9899","year":"1999","journal-title":"Standard"},{"key":"44","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-1491-3"},{"year":"0","key":"47"},{"journal-title":"Software Abstractions Logic Language and Analysis","year":"2006","author":"jackson","key":"46"},{"article-title":"ANSI-C Bounded Model Checker User Manual","year":"2006","author":"clarke","key":"10"},{"key":"51","first-page":"302","article-title":"An Extended Static Checker for Modula-3","volume":"1383","author":"leino","year":"1998","journal-title":"LNCS"},{"key":"52","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_5"},{"key":"53","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"54","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-8157-6_28"},{"key":"50","article-title":"Statically Detecting Likely Buffer Overflow Vulnerabilities","author":"larochelle","year":"2001","journal-title":"Proceedings of 2001 USENIX Security Symposium Washington D C"}],"event":{"name":"2007 First Joint IEEE\/IFIP Symposium on Theoretical Aspects of Software Engineering","start":{"date-parts":[[2007,6,6]]},"location":"Shanghai","end":{"date-parts":[[2007,6,8]]}},"container-title":["First Joint IEEE\/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/4239934\/4239935\/04239943.pdf?arnumber=4239943","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T10:59:55Z","timestamp":1737111595000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/4239943\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,6]]},"references-count":80,"URL":"https:\/\/doi.org\/10.1109\/tase.2007.55","relation":{},"subject":[],"published":{"date-parts":[[2007,6]]}}}