{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T04:16:48Z","timestamp":1747196208143,"version":"3.40.5"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319100609"},{"type":"electronic","value":"9783319100616"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10061-6_20","type":"book-chapter","created":{"date-parts":[[2014,11,5]],"date-time":"2014-11-05T11:34:11Z","timestamp":1415187251000},"page":"304-318","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Mechanized Support for Assurance Case Argumentation"],"prefix":"10.1007","author":[{"given":"John","family":"Rushby","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,11,6]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"Bishop, P., Bloomfield, R.: A methodology for safety case development. In: Safety-Critical Systems Symposium, Birmingham, UK (1998)","DOI":"10.1007\/978-1-4471-1534-2_14"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Kelly, T.: arguing safety\u2013a systematic approach to safety case management. Ph.D. thesis, Department of Computer Science, University of York, UK (1998)","DOI":"10.1007\/3-540-48249-0_2"},{"key":"20_CR3","unstructured":"Greenwell, W.S., Knight, J.C., Holloway, C.M., Pease, J.J.: A taxonomy of fallacies in system safety arguments. In: Proceedings of the 24th International System Safety Conference, Albuquerque, NM (2006)"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., et al.: seL4: formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, pp. 207\u2013220. ACM (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-30206-3_13","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"P Miner","year":"2004","unstructured":"Miner, P., Geser, A., Pike, L., Maddalon, J.: A unified fault-tolerance protocol. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 167\u2013182. Springer, Heidelberg (2004)"},{"key":"20_CR6","first-page":"209","volume":"17","author":"A Narkawicz","year":"2012","unstructured":"Narkawicz, A., Mu\u00f1oz, C.: Formal verification of conflict detection algorithms for arbitrary trajectories. Reliable Comput. 17, 209\u2013237 (2012)","journal-title":"Reliable Comput."},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Rushby, J.: Formalism in safety cases. In: Dale, C., Anderson, T. (eds.) Making Systems Safer: Proceedings of the Eighteenth Safety-Critical Systems Symposium, Bristol, UK, pp. 3\u201317. Springer (2010)","DOI":"10.1007\/978-1-84996-086-1_1"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Basir, N., Denney, E., Fischer, B.: Deriving safety cases from automatically constructed proofs. In: 4th IET International Conference on System Safety, London, UK. The Institutions of Engineering and Technology (2009)","DOI":"10.1049\/cp.2009.1535"},{"key":"20_CR9","unstructured":"Takeyama, M., Kido, H., Kinoshita, Y.: Using a proof assistant to construct assurance cases: correctness by construction (fast abstract). In: The International Conference on Dependable Systems and Networks, Boston, MA. IEEE Computer Society (2012)"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Hawkins, R., Kelly, T., Knight, J., Graydon, P.: A new approach to creating clear safety arguments. In: Dale, C., Anderson, T. (eds.) Advances in System Safety: Proceedings of the Nineteenth Safety-Critical Systems Symposium, Southampton, UK. Springer (2011)","DOI":"10.1007\/978-0-85729-133-2_1"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-40793-2_1","volume-title":"Computer Safety, Reliability, and Security","author":"J Rushby","year":"2013","unstructured":"Rushby, J.: Logic and epistemology in safety cases. In: Bitsch, F., Guiochet, J., Ka\u00e2niche, M. (eds.) SAFECOMP 2013. LNCS, vol. 8153, pp. 1\u20137. Springer, Heidelberg (2013)"},{"key":"20_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-2312-5","volume-title":"GSN\u2013The Goal Structuring Notation","author":"J Spriggs","year":"2012","unstructured":"Spriggs, J.: GSN\u2013The Goal Structuring Notation. Springer, London (2012)"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Denney, E., Pai, G., Pohl, J.: AdvoCATE: an assurance case automation toolset. In: Proceedings of the Workshop on Next Generation of System Assurance Approaches for Safety Critical Systems (SASSUR), Magdeburg, Germany (2012)","DOI":"10.1007\/978-3-642-33675-1_2"},{"key":"20_CR14","unstructured":"ASCE: ASCE. http:\/\/www.adelard.com\/web\/hnav\/ASCE\/index.html"},{"key":"20_CR15","unstructured":"SACM: OMG Structured Assurance Case Metamodel (SACM). http:\/\/www.omg.org\/spec\/SACM\/"},{"key":"20_CR16","unstructured":"MACL: OMG Machine-Checkable Assurance Case Language (MACL). http:\/\/www.omg.org\/cgi-bin\/doc?sysa\/2012-9-4\/"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-642-35873-9_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Cruanes","year":"2013","unstructured":"Cruanes, S., Hamon, G., Owre, S., Shankar, N.: Tool integration with the evidential tool bus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 275\u2013294. Springer, Heidelberg (2013)"},{"key":"20_CR18","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/1646353.1646372","volume":"53","author":"SP Miller","year":"2010","unstructured":"Miller, S.P., Whalen, M.W., Cofer, D.D.: Software model checking takes off. Commun. ACM 53, 58\u201364 (2010)","journal-title":"Commun. ACM"},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"Rushby, J.: Harnessing disruptive innovation in formal verification. In: Hung, D.V., Pandya, P. (eds.) Fourth International Conference on Software Engineering and Formal Methods (SEFM), India, Pune, pp. 21\u201328. IEEE Computer Society (2006)","DOI":"10.1109\/SEFM.2006.24"},{"key":"20_CR20","doi-asserted-by":"crossref","unstructured":"Mercier, H., Sperber, D.: Why do humans reason? Arguments for an argumentative theory. Behav. Brain Sci. 34, 57\u2013111 (2011); See also the commentary on page 74 by Baumeister, R.F., Masicampo, E.J., Nathan DeWall, C.: Arguing, Reasoning, and the Interpersonal (Cultural) Functions of Human Consciousness","DOI":"10.1017\/S0140525X10002785"},{"key":"20_CR21","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1145\/371578.371581","volume":"32","author":"CI Ches\u00f1evar","year":"2000","unstructured":"Ches\u00f1evar, C.I., Maguitman, A.G., Loui, R.P.: Logical models of argument. ACM Comput. Surv. 32, 337\u2013383 (2000)","journal-title":"ACM Comput. Surv."},{"key":"20_CR22","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0004-3702(80)90011-9","volume":"13","author":"J McCarthy","year":"1980","unstructured":"McCarthy, J.: Circumscription-a form of non-monotonic reasoning. Artif. Intell. 13, 27\u201339 (1980)","journal-title":"Artif. Intell."},{"key":"20_CR23","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1207\/s15516709cog1104_4","volume":"11","author":"JL Pollock","year":"1987","unstructured":"Pollock, J.L.: Defeasible reasoning. Cogn. Sci. 11, 481\u2013518 (1987)","journal-title":"Cogn. Sci."},{"key":"20_CR24","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/0004-3702(87)90062-2","volume":"32","author":"R Reiter","year":"1987","unstructured":"Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. 32, 57\u201395 (1987)","journal-title":"Artif. Intell."},{"key":"20_CR25","unstructured":"Crow, J., Rushby, J.: Model-based reconfiguration: toward an integration with diagnosis. In: Proceedings of AAAI-91, Anaheim, CA, vol. 2, pp. 836\u2013841 (1991)"},{"key":"20_CR26","unstructured":"Yices: Yices. http:\/\/yices.csl.sri.com\/"},{"key":"20_CR27","doi-asserted-by":"crossref","unstructured":"Holloway, C.M.: Safety case notations: alternatives for the non-graphically inclined? In: 3rd IET International Conference on System Safety, Birmingham, UK. The Institutions of Engineering and Technology (2008)","DOI":"10.1049\/cp:20080710"},{"key":"20_CR28","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S Owre","year":"1995","unstructured":"Owre, S., Rushby, J., Shankar, N., von Henke, F.: Formal verification for fault-tolerant architectures: prolegomena to the design of PVS. IEEE Trans. Softw. Eng. 21, 107\u2013125 (1995)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"20_CR29","unstructured":"PVS: PVS. http:\/\/pvs.csl.sri.com\/"},{"key":"20_CR30","doi-asserted-by":"publisher","first-page":"1178","DOI":"10.1109\/TSE.2011.80","volume":"38","author":"B Littlewood","year":"2012","unstructured":"Littlewood, B., Rushby, J.: Reasoning about the reliability of diverse two-channel systems in which one channel is \u201cpossibly perfect\u201d. IEEE Trans. Softw. Eng. 38, 1178\u20131194 (2012)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"20_CR31","unstructured":"Kinoshita, Y., Takeyama, M.: Assurance case as a proof in a theory: towards formulation of rebuttals. In: Dale, C., Anderson, T. (eds.) Assuring the Safety of Systems: Proceedings of the 21st Safety-Critical Systems Symposium, SCSC, pp. 205\u2013230 (2013)"},{"key":"20_CR32","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/S0004-3702(01)00145-X","volume":"133","author":"JL Pollock","year":"2001","unstructured":"Pollock, J.L.: Defeasible reasoning with variable degrees of justification. Artif. Intell. 133, 233\u2013282 (2001)","journal-title":"Artif. Intell."},{"key":"20_CR33","doi-asserted-by":"crossref","unstructured":"Staples, M.: Critical rationalism and engineering: Ontology. Synthese (to appear, 2014)","DOI":"10.1007\/s11229-014-0396-3"},{"key":"20_CR34","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/j.jal.2006.04.001","volume":"6","author":"MWA Caminada","year":"2008","unstructured":"Caminada, M.W.A.: A formal account of Socratic-style argumentation. J. Appl. Logic 6, 109\u2013132 (2008)","journal-title":"J. Appl. Logic"},{"key":"20_CR35","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0004-3702(94)00041-X","volume":"77","author":"PM Dung","year":"1995","unstructured":"Dung, P.M.: On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and $$n$$-person games. Artif. Intell. 77, 321\u2013357 (1995)","journal-title":"Artif. Intell."},{"key":"20_CR36","doi-asserted-by":"crossref","unstructured":"Steele, P., Knight, J.: Analysis of critical system certication. In: 15th IEEE International Symposium on High Assurance Systems Engineering, Miami, FL (2014)","DOI":"10.1109\/HASE.2014.26"},{"key":"20_CR37","unstructured":"Goodenough, J.B., Weinstock, C.B., Klein, A.Z., Ernst, N.: Analyzing a multi-legged argument using eliminative argumentation. In: Layered Assurance Workshop, New Orleans, LA (2013)"},{"key":"20_CR38","doi-asserted-by":"crossref","unstructured":"Weinstock, C.B., Goodenough, J.B., Klein, A.Z.: Measuring assurance case confidence using Baconian probabilities. In: 1st International Workshop on Assurance Cases for Software-Intensive Systems (ASSURE), San Francisco, CA (2013)","DOI":"10.1109\/ASSURE.2013.6614264"}],"container-title":["Lecture Notes in Computer Science","New Frontiers in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10061-6_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T14:44:51Z","timestamp":1747147491000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-10061-6_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319100609","9783319100616"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10061-6_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"6 November 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}