{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T05:45:43Z","timestamp":1743054343959,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642242694"},{"type":"electronic","value":"9783642242700"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-24270-0_7","type":"book-chapter","created":{"date-parts":[[2011,9,7]],"date-time":"2011-09-07T10:51:44Z","timestamp":1315392704000},"page":"85-98","source":"Crossref","is-referenced-by-count":5,"title":["Rigorous Evidence of Freedom from Concurrency Faults in Industrial Control Software"],"prefix":"10.1007","author":[{"given":"Richard","family":"Bonichon","sequence":"first","affiliation":[]},{"given":"G\u00e9raud","family":"Canet","sequence":"additional","affiliation":[]},{"given":"Lo\u00efc","family":"Correnson","sequence":"additional","affiliation":[]},{"given":"Eric","family":"Goubault","sequence":"additional","affiliation":[]},{"given":"Emmanuel","family":"Haucourt","sequence":"additional","affiliation":[]},{"given":"Michel","family":"Hirschowitz","sequence":"additional","affiliation":[]},{"given":"S\u00e9bastien","family":"Labb\u00e9","sequence":"additional","affiliation":[]},{"given":"Samuel","family":"Mimram","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Aiken, A., Foster, J.S., Kodumal, J., Terauchi, T.: Checking and inferring local non-aliasing. In: PLDI, pp. 128\u2013140 (2003)","DOI":"10.1145\/781131.781146"},{"key":"7_CR2","volume-title":"Principles of Model-Checking","author":"C. Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model-Checking. MIT Press, Cambridge (2008)"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-642-15375-4_10","volume-title":"CONCUR 2010 - Concurrency Theory","author":"T. Balabonski","year":"2010","unstructured":"Balabonski, T., Haucourt, E.: A geometric approach to the problem of unique decomposition of processes. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol.\u00a06269, pp. 132\u2013146. Springer, Heidelberg (2010)"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The slam project: debugging system software via static analysis. In: POPL, pp. 1\u20133 (2002)","DOI":"10.1145\/503272.503274"},{"issue":"5","key":"7_CR5","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/s10009-008-0064-3","volume":"10","author":"S. Bardin","year":"2008","unstructured":"Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: Fast: acceleration from theory to practice. STTT\u00a010(5), 401\u2013424 (2008)","journal-title":"STTT"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G. Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol.\u00a03185, pp. 200\u2013236. Springer, Heidelberg (2004)"},{"issue":"5-6","key":"7_CR7","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker blast. STTT\u00a09(5-6), 505\u2013525 (2007)","journal-title":"STTT"},{"issue":"4","key":"7_CR8","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A. Cimatti","year":"2000","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: Nusmv: A new symbolic model checker. STTT\u00a02(4), 410\u2013425 (2000)","journal-title":"STTT"},{"key":"7_CR9","volume-title":"Model Checking","author":"E.M. Clarke Jr","year":"1999","unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"7_CR10","unstructured":"Cuoq, P., Prevosto, V.: Frama-c\u2019s value analysis plug-in. CEA LIST Technical Report (2010), http:\/\/frama-c.com\/download\/frama-c-value-analysis.pdf"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Cuoq, P., Signoles, J., Baudin, P., Bonichon, R., Canet, G., Correnson, L., Monate, B., Prevosto, V., Puccetti, A.: Experience report: OCaml for an industrial-strength static analysis framework. In: ICFP, pp. 281\u2013286 (2009)","DOI":"10.1145\/1631687.1596591"},{"key":"7_CR12","unstructured":"CWE Common Weakness Enumeration \u2014, http:\/\/cwe.mitre.org\/"},{"key":"7_CR13","first-page":"43","volume-title":"Programming Languages: NATO Advanced Study Institute","author":"E.W. Dijkstra","year":"1968","unstructured":"Dijkstra, E.W.: Cooperating sequential processes. In: Programming Languages: NATO Advanced Study Institute, pp. 43\u2013112. Academic Press, London (1968)"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-642-12002-2_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Dr\u00e4ger","year":"2010","unstructured":"Dr\u00e4ger, K., Kupriyanov, A., Finkbeiner, B., Wehrheim, H.: Slab: A certifying model checker for infinite-state concurrent systems. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 271\u2013274. Springer, Heidelberg (2010)"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Emanuelsson, P., Nilsson, U.: A Comparative Study of Industrial Static Analysis Tools. Link\u00f6pink University Technical Report (2008)","DOI":"10.1016\/j.entcs.2008.06.039"},{"key":"7_CR16","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/j.tcs.2006.03.022","volume":"357","author":"L. Fajstrup","year":"2006","unstructured":"Fajstrup, L., Goubault, E., Rau\u00dfen, M.: Algebraic topology and concurrency. Theoretical Computer Science\u00a0357, 241\u2013278 (2006)","journal-title":"Theoretical Computer Science"},{"key":"7_CR17","unstructured":"Frama-c Software Analyzers \u2014, http:\/\/frama-c.com\/"},{"issue":"4","key":"7_CR18","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1017\/S0960129500003133","volume":"10","author":"E. Goubault","year":"2000","unstructured":"Goubault, E.: Geometry and concurrency: a user\u2019s guide. Mathematical Structures in Computer Science\u00a010(4), 411\u2013425 (2000)","journal-title":"Mathematical Structures in Computer Science"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1007\/11539452_38","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"E. Goubault","year":"2005","unstructured":"Goubault, E., Haucourt, E.: A practical application of geometric semantics to static analysis of concurrent programs. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, pp. 503\u2013517. Springer, Heidelberg (2005)"},{"key":"7_CR20","series-title":"New Mathematical Monographs","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511657474","volume-title":"Directed Algebraic Topology","author":"M. Grandis","year":"2009","unstructured":"Grandis, M.: Directed Algebraic Topology. New Mathematical Monographs. Cambridge University Press, Cambridge (2009)"},{"key":"7_CR21","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley Professional, Reading (2003)"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/11537328_3","volume-title":"Model Checking Software","author":"G.J. Holzmann","year":"2005","unstructured":"Holzmann, G.J., Ruys, T.C.: Effective bug hunting with spin and modex. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol.\u00a03639, p. 24. Springer, Heidelberg (2005)"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Labb\u00e9, S., Sangnier, A.: Formal verification of industrial software with dynamic memory management. In: IEEE PRDC. pp. 77\u201384 (2010)","DOI":"10.1109\/PRDC.2010.19"},{"key":"7_CR24","unstructured":"Labb\u00e9, S., Thuy, N.: Formal verification of freedom from intrinsic software faults in digital control systems. In: ANS NPIC&HMIT, pp. 2191\u20132201 (2010)"},{"key":"7_CR25","unstructured":"Larochelle, D., Evans, D.: Statically detecting likely buffer overflow vulnerabilities. In: USENIX Security Symposium, pp. 177\u2013190 (2001)"},{"key":"7_CR26","series-title":"Mathematical Studies","volume-title":"Topology and Order","author":"L. Nachbin","year":"1965","unstructured":"Nachbin, L.: Topology and Order. Mathematical Studies, vol.\u00a04. Van Nostrand, Princeton (1965)"},{"key":"7_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-69611-7_16","volume-title":"Practical Aspects of Declarative Languages","author":"A. Podelski","year":"2006","unstructured":"Podelski, A., Rybalchenko, A.: Armc: The logical choice for software model checking with abstraction refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol.\u00a04354, pp. 245\u2013259. Springer, Heidelberg (2006)"},{"key":"7_CR28","unstructured":"Thuy, N., Ourghanlian, A.: Dependability assessment of safety-critical system software by static analysis methods. In: DSN, pp. 75\u201379 (2003)"}],"container-title":["Lecture Notes in Computer Science","Computer Safety, Reliability, and Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24270-0_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,14]],"date-time":"2019-06-14T22:50:06Z","timestamp":1560552606000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24270-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642242694","9783642242700"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24270-0_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}