{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T05:52:25Z","timestamp":1649137945407},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2010,1,21]],"date-time":"2010-01-21T00:00:00Z","timestamp":1264032000000},"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":[[2010,12]]},"DOI":"10.1007\/s11334-009-0121-4","type":"journal-article","created":{"date-parts":[[2010,1,20]],"date-time":"2010-01-20T12:25:50Z","timestamp":1263990350000},"page":"255-268","source":"Crossref","is-referenced-by-count":1,"title":["A formal nethod (a networked formal method)"],"prefix":"10.1007","volume":"6","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":[[2010,1,21]]},"reference":[{"key":"121_CR1","doi-asserted-by":"crossref","unstructured":"Abujarad F, Bonakdarpour B, Kulkarni S (2009) Parallelizing deadlock resolution in symbolic synthesis of distributed programs. In: Proceedings of PDMC 2009: 8th international workshop on parallel and distributed methods in verifixation, November 4, 2009, Eindhoven, The Netherlands (with Formal Methods 2009, November 2\u20136, 2009)","DOI":"10.4204\/EPTCS.14.7"},{"key":"121_CR2","unstructured":"American National Standard for Information Systems\u2014Programming Language C, ANSI X3.159-1989. American National Standards Institute (1989)"},{"key":"121_CR3","doi-asserted-by":"crossref","unstructured":"Anderson DP (2004) BOINC: a system for public-resource computing and storage. In: Proceedings of the 5th IEEE\/ACM international workshop on grid computing, November 8, 2004, Pittsburgh, USA","DOI":"10.1109\/GRID.2004.14"},{"key":"121_CR4","doi-asserted-by":"crossref","unstructured":"Anderson DP, Korpela E, Walton R (2005) High-performance task distribution for volunteer computing. In: Proceedings of the first IEEE international conference on e-science and grid technologies, December 5\u20138, 2005, Melbourne, Australia","DOI":"10.1109\/E-SCIENCE.2005.51"},{"key":"121_CR5","doi-asserted-by":"crossref","unstructured":"Ball T, Rajamani SK (2002) The SLAM project: debugging system software via static analysis. In: Proceedings of the POPL \u201902: proceedings of the ACM SIGPLAN-SIGACT conference on principles of programming languages","DOI":"10.1145\/503272.503274"},{"key":"121_CR6","first-page":"51","volume":"27","author":"PK Bobko","year":"2001","unstructured":"Bobko PK (2001) Open-source software and the demise of copyright. Rutgers Comput Technol Law J 27: 51\u201392","journal-title":"Rutgers Comput Technol Law J"},{"key":"121_CR7","unstructured":"Barnett M, Rustan K, Leino M, Schulte W (2004) The Spec# programming system: an overview, CASSIS 2004. Lecture notes in computer science, vol 362. Springer, Berlin"},{"key":"121_CR8","volume-title":"Extreme programming explained: embrace change","author":"K Beck","year":"1999","unstructured":"Beck K (1999) Extreme programming explained: embrace change. Addison-Wesley, Reading"},{"key":"121_CR9","doi-asserted-by":"crossref","unstructured":"Breuer PT, Garc\u00eda Valls M (2004) Static deadlock detection in the Linux Kernel. 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. Lecture notes in computer science, vol 3063. Springer, Berlin, pp 52\u201364","DOI":"10.1007\/978-3-540-24841-5_4"},{"key":"121_CR10","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, Harbour MG (eds) Proceedings of reliable software technologies\u2014Ada-Europe 2006, 11th Ada-Europe international conference on reliable software technologies, June 2006, Oporto, Portugal. Lecture notes in computer science, vol 4006. Springer, Berlin, pp 56\u201370"},{"key":"121_CR11","volume-title":"Symbolic approximation: an approach to verification in the large innovations in systems and software engineering\u2014a NASA journal, October 2006","author":"PT Breuer","year":"2006","unstructured":"Breuer PT, Pickin S (2006) Symbolic approximation: an approach to verification in the large innovations in systems and software engineering\u2014a NASA journal, October 2006. Springer, London"},{"issue":"2","key":"121_CR12","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E Clarke","year":"1986","unstructured":"Clarke E, Emerson E, Sistla A (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":"121_CR13","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":"121_CR14","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 the 4th symposium on operating system design and implementation (OSDI 2000), October 2000, pp 1\u201316","DOI":"10.21236\/ADA419626"},{"key":"121_CR15","doi-asserted-by":"crossref","unstructured":"Evans D, Larochelle D (2002) Improving security using extensible lightweight static analysis. IEEE Software, New York, Jan\/Feb 2002","DOI":"10.1109\/52.976940"},{"key":"121_CR16","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, June 2002, pp 1\u201312","DOI":"10.1145\/512529.512531"},{"key":"121_CR17","first-page":"179","volume":"36","author":"RW Gomulkiewicz","year":"1999","unstructured":"Gomulkiewicz RW (1999) How copyleft uses license rights to succeed in the open source software revolution and the implications for article 2B. Houston Law Rev 36: 179\u2013194","journal-title":"Houston Law Rev"},{"key":"121_CR18","unstructured":"Guttag JV, Horning JJ (1991) A tutorial on Larch and LCL, a Larch\/C interface language. VDM \u201991 Formal Software Development Methods. Lecture notes in computer science, vol 552. Springer, Berlin, pp 1\u201378"},{"key":"121_CR19","volume-title":"GCC: the complete reference","author":"A Griffith","year":"2002","unstructured":"Griffith A (2002) GCC: the complete reference. McGraw-Hill\/ Osborne, New York"},{"issue":"10","key":"121_CR20","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10): 576\u2013580, 583","journal-title":"Commun ACM"},{"key":"121_CR21","volume-title":"The SPIN MODEL CHECKER: primer and reference manual","author":"GJ Holzmann","year":"2003","unstructured":"Holzmann GJ (2003) The SPIN MODEL CHECKER: primer and reference manual. Addison-Wesley, Reading"},{"key":"121_CR22","doi-asserted-by":"crossref","unstructured":"Holzmann GJ, Joshi R, Groce A (2008) Swarm verification. In: Proceedings of the ASE 2008, 23rd IEEE\/ACM international conference on automated software engineering. l\u2019Aquila, Italy, September 2008","DOI":"10.1109\/ASE.2008.9"},{"issue":"3\u20134","key":"121_CR23","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/s10515-008-0033-9","volume":"15","author":"GJ Holzmann","year":"2008","unstructured":"Holzmann GJ, Joshi R, Groce A (2008) Model driven code checking. Autom Softw Eng 15(3\u20134): 283\u2013297","journal-title":"Autom Softw Eng"},{"key":"121_CR24","unstructured":"ISO\/IEC 9899-1999, Programming Languages\u2014C. International Standards Organisation (1999)"},{"key":"121_CR25","unstructured":"Johnson R, Wagner D (2004) Finding user\/kernel pointer bugs with type inference. In: Proceedings of the 13th USENIX security symposium, Aug 9\u201313, 2004, San Diego, CA, USA"},{"key":"121_CR26","volume-title":"The C language","author":"B Kernighan","year":"1988","unstructured":"Kernighan B, Ritchie D (1988) The C language, 2nd edn. Prentice-Hall, Englewood Cliffs","edition":"2"},{"key":"121_CR27","unstructured":"Kroah-Hartman G (2006) Linux kernel development: how fast is it going, who is doing it, what they are doing, and who is sponsoring it. In: Proceedings of the OLS \u201906: the 2006 Ottawa Linux Symposium, July 2006, Ottawa, Canada, pp 239\u2013244"},{"key":"121_CR28","volume-title":"Theory of linear and integer programming","author":"A Schrijver","year":"1998","unstructured":"Schrijver A (1998) Theory of linear and integer programming. Wiley, New York"},{"key":"121_CR29","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 2000, February 2\u20134, San Diego, CA, USA"},{"key":"121_CR30","volume-title":"Solaris ZFS essentials","author":"S Watanabe","year":"2009","unstructured":"Watanabe S (2009) Solaris ZFS essentials. Prentice-Hall, Englewood Cliffs"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-009-0121-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-009-0121-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-009-0121-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T13:47:45Z","timestamp":1559396865000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-009-0121-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,1,21]]},"references-count":30,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2010,12]]}},"alternative-id":["121"],"URL":"https:\/\/doi.org\/10.1007\/s11334-009-0121-4","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,1,21]]}}}