{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,19]],"date-time":"2023-02-19T23:06:31Z","timestamp":1676847991391},"reference-count":15,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2006,10,28]],"date-time":"2006-10-28T00:00:00Z","timestamp":1161993600000},"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":[[2006,11,14]]},"DOI":"10.1007\/s11334-006-0010-z","type":"journal-article","created":{"date-parts":[[2006,10,27]],"date-time":"2006-10-27T13:44:09Z","timestamp":1161956649000},"page":"147-163","source":"Crossref","is-referenced-by-count":4,"title":["Symbolic approximation: an approach to verification in the large"],"prefix":"10.1007","volume":"2","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":[[2006,10,28]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Ball T, Rajamani SK (2002) The SLAM project: debugging system software via static analysis. In: Proc. POPL \u201902: Proceedings of the ACM SIGPLAN-SIGACT conference on principles of programming languages","DOI":"10.1145\/503272.503274"},{"issue":"11","key":"10_CR2","doi-asserted-by":"crossref","first-page":"1263","DOI":"10.1002\/spe.4380251106","volume":"25","author":"PT Breuer","year":"1995","unstructured":"Breuer PT, Bowen JP (1995) A PREttier compiler\u2013compiler: Generating higher order parsers in C. Softw Pract Exp 25(11):1263\u20131297","journal-title":"Softw Pract Exp"},{"key":"10_CR3","unstructured":"Breuer PT, Pickin S (2006) One million (Loc) and counting: static analysis for errors and vulnerabilites in the Linux kernel source code. In: Pinho LM, Harbour MG (eds) Proceedings of Reliable Software Technologies\u2014Ada-Europe 2006, 11th Ada-Europe international conference on Reliable Software Technologies, Ser. LNCS, PP. 56\u201370"},{"key":"10_CR4","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/978-3-540-24841-5_4","volume-title":"Reliable software technologies \u2013 Ada-Europe 2004, 9th Ada-Europe International Conference on Reliable Software Technologies, Palma de Mallorca, Spain, 14\u201318, June 2004. LNCS vol 3063","author":"PT Breuer","year":"2004","unstructured":"Breuer PT, Garcia Valls M (2004) Static deadlock detection in the Linux kernel. In: Llamos\u00ed A, Strohmeier A (eds) Reliable software technologies \u2013 Ada-Europe 2004, 9th Ada-Europe International Conference on Reliable Software Technologies, Palma de Mallorca, Spain, 14\u201318, June 2004. LNCS vol 3063. Springer, Berlin Heidelberg New York, pp 52\u201364"},{"issue":"4","key":"10_CR5","doi-asserted-by":"crossref","first-page":"586","DOI":"10.1145\/262004.262007","volume":"19","author":"PT Breuer","year":"1997","unstructured":"Breuer PT, Delgado Kloos C, Mart\u00ednez Madrid N, L\u00f3pez Marin A, S\u00e1nchez L (1997) A refinement calculus for the synthesis of verified digital or analog hardware descriptions in VHDL. ACM Trans Program Lang Syst (TOPLAS) 19(4):586\u2013616","journal-title":"ACM Trans Program Lang Syst (TOPLAS)"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Breuer PT, Mart\u00ednez Madrid N, S\u00e1nchez L, Mar\u00edn A, Delgado Kloos C (1996) A formal method for specification and refinement of real-time systems. In: Proceedings of the 8th EuroMicro workshop on real time systems, IEEE, New York, L\u2019aquilla, Italy, pp. 34\u201342","DOI":"10.1109\/EMWRTS.1996.557891"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Chaki S, Clarke E, Groce A, Jha S, Veith H (2003) Modular verification of software components in C. In: Proceedings of the international conference on software engineering, pp. 385\u2013389","DOI":"10.1109\/ICSE.2003.1201217"},{"issue":"5","key":"10_CR8","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E Clarke","year":"1986","unstructured":"Clarke E, Emerson E, Sistla A (1986) Automiatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications. ACM Trans Program alang Syst 16(5):1512\u20131542","journal-title":"ACM Trans Program alang Syst"},{"issue":"5","key":"10_CR9","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E Clarke","year":"1994","unstructured":"Clarke E, Grumberg O, Long D.A (1994) Model Checking and Abstraction. ACM Trans Program Lang Syst 16(5):1512\u20131542","journal-title":"ACM Trans Program Lang Syst"},{"key":"10_CR10","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 the 4th ACM symposium on the principles of programming languages, pp 238\u2013252","DOI":"10.1145\/512950.512973"},{"key":"10_CR11","unstructured":"Chen H, Dean D, Wagner D (2004) Model checking one million lines of C code. In: Proceedings of the 11th annual network and distributed system security symposium, San Diego, CA"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Foster JS, F\u00e4hndrich M, Aiken A (1999) A theory of type qualifiers. In: Proceedings of the ACM SIGPLAN conference on programming language design and implementation (PLDI\u201999), Atlanta, Georgia","DOI":"10.1145\/301618.301665"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Foster JS, Terauchi T, Aiken A (2002) Flow-sensitive type qualifiers. In: Proceedings of the ACM SIGPLAN conference on programming language design and implementation (PLDI\u201902), Berlin, Germany, pp 1\u201312","DOI":"10.1145\/512529.512531"},{"key":"10_CR14","unstructured":"Johnson R, Wagner D (2004) Finding User\/Kernel pointer bugs with type inference. In: Proceedings of the 13th USENIX security symposium, 9\u201313 August 2004, San Diego, CA, USA"},{"key":"10_CR15","unstructured":"Wagner D, Foster JS, Brewer EA, Aiken A (2000) A first step towards automated detection of buffer overrun vulnerabilities. In: Proceedings of the network and distributed system security (NDSS) symposium, 2\u20134 February 2000, 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-006-0010-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-006-0010-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-006-0010-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T13:47:43Z","timestamp":1559396863000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-006-0010-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,10,28]]},"references-count":15,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2006,11,14]]}},"alternative-id":["10"],"URL":"https:\/\/doi.org\/10.1007\/s11334-006-0010-z","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,10,28]]}}}