{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T03:33:36Z","timestamp":1648870416730},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2008,3,4]],"date-time":"2008-03-04T00:00:00Z","timestamp":1204588800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2008,4]]},"DOI":"10.1007\/s11334-008-0045-4","type":"journal-article","created":{"date-parts":[[2008,3,3]],"date-time":"2008-03-03T12:03:04Z","timestamp":1204545784000},"page":"87-105","source":"Crossref","is-referenced-by-count":1,"title":["Approximate verification in an open source world"],"prefix":"10.1007","volume":"4","author":[{"given":"Peter T.","family":"Breuer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simon","family":"Pickin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2008,3,4]]},"reference":[{"key":"45_CR1","unstructured":"American National Standard for Information Systems (1989) Programming language C, ANSI X3.159-1989, American National Standards Institute"},{"key":"45_CR2","first-page":"1","volume":"9","author":"ML Balinski","year":"1961","unstructured":"Balinski ML (1961) An algorithm for finding all vertices of convex polyhedral sets. SIAM J 9: 1","journal-title":"SIAM J"},{"key":"45_CR3","doi-asserted-by":"crossref","unstructured":"Ball T, Rajamani SK (2002) The SLAM project: debugging system software via static analysis. In: Proceedings of POPL\u201902: Proceedings of the ACM SIGPLAN-SIGACT conference on principles of programming languages","DOI":"10.1145\/503272.503274"},{"key":"45_CR4","unstructured":"Barnett M, Rustan K, Leino M, Schulte W (2004) The Spec# programming system: an overview, CASSIS 2004. In: LNCS, vol 3362. Springer, Heidelberg"},{"key":"45_CR5","doi-asserted-by":"crossref","unstructured":"Breuer PT, Garci\u00e1 Valls M (2004) Static deadlock detection in the Linux Kernel, pp 52\u201364. In: Llamos\u00ed A, Strohmeier A (eds) Reliable Software Technologies\u2014Ada-Europe 2004, 9th Ada-Europe international conference on Reliable Software Technologies, Palma de Mallorca, Spain, June 14\u201318, 2004 . ISBN 3-540-22011-9. LNCS, vol 3063. Springer, Heidelberg","DOI":"10.1007\/978-3-540-24841-5_4"},{"key":"45_CR6","doi-asserted-by":"crossref","unstructured":"Breuer PT, Pickin S (2006) One Million (LOC) and counting: static analysis for errors and vulnerabilities in the Linux Kernel Source Code. In: Pinho LM, Gonz\u00e1lez Harbour M (eds) Proceedings of Reliable Software Technologies\u2014Ada-Europe 2006, 11th Ada-Europe international conference on Reliable Software Technologies, pp 56\u201370. Oporto, Portugal. LNCS, vol 4006. Springer, Heidelberg","DOI":"10.1007\/11767077_5"},{"key":"45_CR7","doi-asserted-by":"crossref","unstructured":"Breuer PT, Pickin S (2006) Symbolic approximation: an approach to verification in the large. Innovations in systems and software engineering\u2014a NASA journal. Springer, London","DOI":"10.1007\/s11334-006-0010-z"},{"key":"45_CR8","unstructured":"Breuer PT, Pickin S (2006) Abstract interpretation meets model checking near the 106 LOC mark. In: Bharadwa R, Mukhopadhyay S (eds) Proceedings of the fifth international workshop on automated verification of infinite-state systems (AVIS\u201906), Vienna, Austria. Electronic Notes in TCS. Elsevier, Amsterdam"},{"key":"45_CR9","doi-asserted-by":"crossref","unstructured":"Breuer PT, Pickin S, Larrondo Petrie M (2006) Detecting deadlock, double-free and other abuses in a million lines of Linux Kernel Source. In: Hinchey M (ed) Proceedings of 30th annual IEEE\/NASA software engineering workshop (SEW-30), Loyola College Graduate Center, Columbia, MD, USA, 25\u201327 April. IEEE Press, New York","DOI":"10.1109\/SEW.2006.15"},{"key":"45_CR10","doi-asserted-by":"crossref","unstructured":"Breuer PT, Pickin S (2006) Verification in the light and large: large-scale verification for fast-moving open source C projects. In: Hinchey M (ed) Proceedings of 31st annual IEEE\/NASA software engineering workshop (SEW-31), 25\u201327 April. Loyola College Graduate Center, Columbia, MD, USA","DOI":"10.1109\/SEW.2007.37"},{"key":"45_CR11","doi-asserted-by":"crossref","unstructured":"Breuer PT, Pickin S (2006) Checking for deadlock, double-free and other abuses in the Linux Kernel Source Code. In: Alexandrov VN, Dick van Albada G, Sloot PMA, Dongarra J (eds) Part IV Proceedings of workshop on computational science in software engineering (CSSE\u201906), Reading, UK, 28\u201331 May 2006. LNCS, vol 3994, pp 765\u2013772. Springer, Oxford. ISBN 3-540-34385-7","DOI":"10.1007\/11758549_103"},{"key":"45_CR12","doi-asserted-by":"crossref","unstructured":"Breuer PT, Pickin S (2006) Verification in the large via symbolic approximation. In: Second international symposium on leveraging applications of formal methods, verification and validation (ISOLA 2006), 15-19 November, Paphos, Cyprus","DOI":"10.1109\/ISoLA.2006.20"},{"key":"45_CR13","doi-asserted-by":"crossref","DOI":"10.1002\/9781118033166","volume-title":"Optimization methods for logical inference","author":"V Chandru","year":"1999","unstructured":"Chandru V, Hooker J (1999) Optimization methods for logical inference. Wiley\u2013Interscience, New York"},{"issue":"2","key":"45_CR14","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst 8(2): 244\u2013253","journal-title":"ACM Trans Program Lang Syst"},{"key":"45_CR15","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of fourth ACM symposium on the principles of programming languages, pp 238\u2013252","DOI":"10.1145\/512950.512973"},{"key":"45_CR16","doi-asserted-by":"crossref","unstructured":"Engler D, Chelf B, Chou A, Hallem S (2000) Checking system rules using system-specific, programmer-written compiler extensions. In: Proceedings of fourth symposium on operating system design and implementation (OSDI 2000), pp 1\u201316","DOI":"10.21236\/ADA419626"},{"key":"45_CR17","doi-asserted-by":"crossref","unstructured":"Evans D, Larochelle D (2002) Improving security using extensible lightweight static analysis. IEEE Software","DOI":"10.1109\/52.976940"},{"key":"45_CR18","doi-asserted-by":"crossref","unstructured":"Foster JS, Terauchi T, Aiken A (2002) Flow-sensitive type qualifiers. In: Proceedings of ACM SIGPLAN conference on programming language design and implementation (PLDI\u201902), pp 1\u201312. Berlin, Germany","DOI":"10.1145\/512529.512531"},{"key":"45_CR19","unstructured":"Guttag JV, Horning JJ: Introduction to LCL, a Larch\/C interface language. http:\/\/ftp.digital.com\/pub\/Compaq\/SRC\/research-reports\/abstracts\/src-rr-074.html"},{"key":"45_CR20","unstructured":"ISO\/IEC 9899-1999 (1999) Programming languages\u2014C, International Standards Organisation"},{"key":"45_CR21","unstructured":"Johnson R, Wagner D (2004) Finding user\/kernel pointer bugs with type inference. In: Proceedings of 13th USENIX security symposium, San Diego, CA, USA"},{"key":"45_CR22","volume-title":"The traveling salesman problem: a guided tour of combinatorial optimization","author":"EL Lawler","year":"1985","unstructured":"Lawler EL, Lenstra JK, Rinnooy Kan AHG, Shmoys DB (1985) The traveling salesman problem: a guided tour of combinatorial optimization. Wiley, New York"},{"issue":"2","key":"45_CR23","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1287\/moor.5.2.167","volume":"5","author":"TH Mattheis","year":"1980","unstructured":"Mattheis TH, Rubin DS (1980) A survey and comparison of methods for finding all vertices of convex polyhedral sets. Math Oper Res 5(2): 167\u2013185","journal-title":"Math Oper Res"},{"key":"45_CR24","unstructured":"Pickin S, Breuer PT (2006) Symbolic approximation: a technique and a tool for verification in the large. In: Letia IA, Pres UT, Cluj-Napoca (eds) Proceedings of second international conference on intelligent computer communication and processing engineering (ICCP 2006), vol 2, pp 97\u2013104. TU Cluj-Napoca, Romania"},{"key":"45_CR25","volume-title":"Theory of linear and integer programming","author":"A Schrijver","year":"1986","unstructured":"Schrijver A (1986) Theory of linear and integer programming. Wiley, New York"},{"key":"45_CR26","unstructured":"The U.S. Department of Energy Computer Incident Advisory Center (2001) Linux worm Adore, Information Bulletin Number L-067. http:\/\/ftp.cerias.purdue.edu\/pub\/advisories\/ciac\/l-fy01\/l-067.Linux.worm.Adore.txt"},{"key":"45_CR27","unstructured":"Wagner D, Foster JS, Brewer EA, Aiken A (2000) A first step towards automated detection of buffer overrun vulnerabilities. In: Proceedings of network and distributed system security (NDSS) symposium, San Diego, CA, USA"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-008-0045-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-008-0045-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-008-0045-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T13:47:44Z","timestamp":1559396864000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-008-0045-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,3,4]]},"references-count":27,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2008,4]]}},"alternative-id":["45"],"URL":"https:\/\/doi.org\/10.1007\/s11334-008-0045-4","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,3,4]]}}}