{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,9]],"date-time":"2026-02-09T10:30:23Z","timestamp":1770633023175,"version":"3.49.0"},"publisher-location":"Cham","reference-count":51,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319961446","type":"print"},{"value":"9783319961453","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-96145-3_3","type":"book-chapter","created":{"date-parts":[[2018,7,20]],"date-time":"2018-07-20T18:25:55Z","timestamp":1532111155000},"page":"38-47","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":66,"title":["Formal Reasoning About the Security of Amazon Web Services"],"prefix":"10.1007","author":[{"given":"Byron","family":"Cook","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,18]]},"reference":[{"key":"3_CR1","unstructured":"Boogie program prover. \n                      https:\/\/github.com\/boogie-org\/boogie"},{"key":"3_CR2","unstructured":"CBMC model checker. \n                      https:\/\/github.com\/diffblue\/cbmc"},{"key":"3_CR3","unstructured":"CompCert project. \n                      http:\/\/compcert.inria.fr"},{"key":"3_CR4","unstructured":"Coq theorem prover. \n                      https:\/\/github.com\/coq\/coq"},{"key":"3_CR5","unstructured":"CVC4 decision procedure. \n                      http:\/\/cvc4.cs.stanford.edu"},{"key":"3_CR6","unstructured":"Dafny theorem prover. \n                      https:\/\/github.com\/Microsoft\/dafny"},{"key":"3_CR7","unstructured":"DeepSpec project. \n                      https:\/\/deepspec.org"},{"key":"3_CR8","unstructured":"HOL-light theorem prover. \n                      https:\/\/github.com\/jrh13\/hol-light"},{"key":"3_CR9","unstructured":"Infer program analysis. \n                      https:\/\/github.com\/facebook\/infer"},{"key":"3_CR10","unstructured":"OpenJML program prover. \n                      https:\/\/github.com\/OpenJML"},{"key":"3_CR11","unstructured":"Prover Certifier. \n                      https:\/\/www.prover.com\/software-solutions-rail-control\/prover-certifier"},{"key":"3_CR12","unstructured":"s2n TLS\/SSL implementation. \n                      https:\/\/github.com\/awslabs\/s2n"},{"key":"3_CR13","unstructured":"SAW program prover. \n                      https:\/\/github.com\/GaloisInc\/saw-script"},{"key":"3_CR14","unstructured":"SMACK software verifier. \n                      http:\/\/smackers.github.io\/"},{"key":"3_CR15","unstructured":"TLA+ theorem prover. \n                      https:\/\/github.com\/tlaplus"},{"key":"3_CR16","unstructured":"VCC program prover. \n                      https:\/\/vcc.codeplex.com"},{"key":"3_CR17","unstructured":"Z3 decision procedure. \n                      https:\/\/github.com\/Z3Prover\/z3"},{"issue":"2","key":"3_CR18","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1108\/ICS-05-2016-0037","volume":"25","author":"A Aldini","year":"2017","unstructured":"Aldini, A., Seigneur, J.M., Ballester Lafuente, C., Titi, X., Guislain, J.: Design and validation of a trust-based opportunity-enabled risk management system. Inf. Comput. Secur. 25(2), 2\u201325 (2017)","journal-title":"Inf. Comput. Secur."},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Alglave, J., Cousot, P.: Ogre and Pythia: an invariance proof method for weak consistency models. In: POPL (2017)","DOI":"10.1145\/3009837.3009883"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S.K., Ustuner, A.: Thorough static analysis of device drivers. In: EuroSys, pp. 73\u201385 (2006)","DOI":"10.1145\/1218063.1217943"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correctness witnesses: exchanging verification results between verifiers (2016)","DOI":"10.1145\/2950290.2950351"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/11817963_33","volume-title":"Computer Aided Verification","author":"A Griesmayer","year":"2006","unstructured":"Griesmayer, A., Bloem, R., Cook, B.: Repair of Boolean programs with an application to C. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 358\u2013371. Springer, Heidelberg (2006). \n                      https:\/\/doi.org\/10.1007\/11817963_33"},{"issue":"2","key":"3_CR23","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1145\/2506164.2506167","volume":"47","author":"S Bouchenak","year":"2013","unstructured":"Bouchenak, S., Chockler, G., Chockler, H., Gheorghe, G., Santos, N., Shraer, A.: Verifying cloud services: present and future. ACM SIGOPS Oper. Syst. Rev. 47(2), 6\u201319 (2013)","journal-title":"ACM SIGOPS Oper. Syst. Rev."},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Chudnov, A., Collins, N., Cook, B., Dodds, J., Huffman, B., Magill, S., MacCarthaigh, C., Mertens, E., Mullen, E., Tasiran, S., Tomb, A., Westbrook, E.: Continuous formal verification of Amazon S2N. In: CAV (2018)","DOI":"10.1007\/978-3-319-96142-2_26"},{"key":"3_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-28891-3_13","volume-title":"NASA Formal Methods","author":"D Cofer","year":"2012","unstructured":"Cofer, D., Gacek, A., Miller, S., Whalen, M.W., LaValley, B., Sha, L.: Compositional verification of architectural models. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 126\u2013140. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-28891-3_13"},{"key":"3_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-06200-6_1","volume-title":"NASA Formal Methods","author":"D Cofer","year":"2014","unstructured":"Cofer, D., Miller, S.: DO-333 certification case studies. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 1\u201315. Springer, Cham (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-319-06200-6_1"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Cook, B., Khazem, K., Kroening, D., Tasiran, S., Tautschnig, M., Tuttle, M.R.: Model checking boot code from AWS data centers. In: CAV (2018)","DOI":"10.1007\/978-3-319-96142-2_28"},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Dullien, T.F.: Weird machines, exploitability, and provable unexploitability. IEEE Trans. Emerg. Top. Comput. PP(99) (2017)","DOI":"10.1109\/TETC.2017.2785299"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Eilers, M., M\u00fcller, P.: Nagini: a static verifier for Python. In: CAV (2018)","DOI":"10.1007\/978-3-319-96145-3_33"},{"key":"3_CR30","unstructured":"Ganesh, V., Banescu, S. and Ochoa, M.: The meaning of attack-resistant programs. In: International Workshop on Progamming Languages and Security (2015)"},{"key":"3_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-642-38088-4_31","volume-title":"NASA Formal Methods","author":"AE Goodloe","year":"2013","unstructured":"Goodloe, A.E., Mu\u00f1oz, C., Kirchner, F., Correnson, L.: Verification of numerical programs: from real numbers to floating point numbers. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 441\u2013446. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-38088-4_31"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Polozov, O., Singh, R.: Program synthesis. In: Foundations and Trends in Programming Languages, vol. 4 (2017)","DOI":"10.1561\/2500000010"},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Formal verification of IA-64 division algorithms. In: TPHOLs (2000)","DOI":"10.1007\/3-540-44659-1_15"},{"key":"3_CR34","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S., Zill, B.: IronFleet: proving practical distributed systems correct. In: SOSP (2015)","DOI":"10.1145\/2815400.2815428"},{"key":"3_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-319-40970-2_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"MJH Heule","year":"2016","unstructured":"Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 228\u2013245. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-40970-2_15"},{"key":"3_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-85114-1_11","volume-title":"Model Checking Software","author":"GJ Holzmann","year":"2008","unstructured":"Holzmann, G.J., Joshi, R., Groce, A.: Tackling large verification problems with the swarm tool. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 134\u2013143. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-85114-1_11"},{"key":"3_CR37","unstructured":"Jordan, H., Scholz, B., Subotic, P.: Towards proof synthesis by neural machine translation. In: CAV (2016)"},{"key":"3_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1007\/978-3-319-33693-0_33","volume-title":"Integrated Formal Methods","author":"R Kumar","year":"2016","unstructured":"Kumar, R., Ball, T., Lichtenberg, J., Deisinger, N., Upreti, A., Bansal, C.: CloudSDV enabling static driver verifier using Microsoft azure. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 523\u2013536. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-33693-0_33"},{"key":"3_CR39","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/s11219-013-9208-0","volume":"21","author":"C Goues Le","year":"2013","unstructured":"Le Goues, C., Forrest, S., Weimer, W.: Current challenges in automatic software repair. Softw. Qual. J. 21, 421\u2013443 (2013)","journal-title":"Softw. Qual. J."},{"key":"3_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-642-18275-4_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"NP Lopes","year":"2011","unstructured":"Lopes, N.P., Rybalchenko, A.: Distributed and predictable software model checking. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 340\u2013355. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-18275-4_24"},{"key":"3_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-319-24953-7_2","volume-title":"Automated Technology for Verification and Analysis","author":"JS Moore","year":"2015","unstructured":"Moore, J.S.: Machines reasoning about machines: 2015. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 4\u201313. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-24953-7_2"},{"key":"3_CR42","first-page":"209","volume":"17","author":"A Narkawicz","year":"2012","unstructured":"Narkawicz, A., Mu\u00f1oz, C.A.: Formal verification of conflict detection algorithms for arbitrary trajectories. Reliab. Comput. 17, 209\u2013237 (2012)","journal-title":"Reliab. Comput."},{"issue":"4","key":"3_CR43","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/2699417","volume":"58","author":"C Newcombe","year":"2004","unstructured":"Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How Amazon web services uses formal methods. Commun. ACM 58(4), 66\u201373 (2004)","journal-title":"Commun. ACM"},{"key":"3_CR44","doi-asserted-by":"crossref","unstructured":"Ochoa, M., Banescu, S., Disenfeld, C., Barthe, G., Ganesh, V.: Reasoning about probabilistic defense mechanisms against remote attacks. In: IEEE European Symposium on Security and Privacy (2017)","DOI":"10.1109\/EuroSP.2017.30"},{"key":"3_CR45","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.: Continuous reasoning: scaling the impact of formal methods. In: LICS (2018)","DOI":"10.1145\/3209108.3209109"},{"key":"3_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-319-41540-6_3","volume-title":"Computer Aided Verification","author":"A Reid","year":"2016","unstructured":"Reid, A., Chen, R., Deligiannis, A., Gilday, D., Hoyes, D., Keen, W., Pathirane, A., Shepherd, O., Vrabel, P., Zaidi, A.: End-to-end verification of processors with ISA-formal. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 42\u201358. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-41540-6_3"},{"key":"3_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/978-3-642-21437-0_31","volume-title":"FM 2011: Formal Methods","author":"KY Rozier","year":"2011","unstructured":"Rozier, K.Y., Vardi, M.Y.: A Multi-encoding approach for LTL symbolic satisfiability checking. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 417\u2013431. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-21437-0_31"},{"key":"3_CR48","doi-asserted-by":"crossref","unstructured":"Rushby, J.: Software verification and system assurance. In: IEEE International Conference on Software Engineering and Formal Methods, pp. 3\u201310 (2009)","DOI":"10.1109\/SEFM.2009.39"},{"key":"3_CR49","unstructured":"Santos, J.F., Maksimovi\u0107, P., Naud\u017ei\u016bnien\u0117, D., Wood, T., Gardner, P.: JaVerT: JavaScript verification toolchain. In: POPL (2017)"},{"issue":"9","key":"3_CR50","doi-asserted-by":"publisher","first-page":"1381","DOI":"10.1109\/TCAD.2005.850814","volume":"24","author":"C-JH Seger","year":"2005","unstructured":"Seger, C.-J.H., Jones, R.B., O\u2019Leary, J.W., Melham, T., Aagaard, M.D., Barrett, C., Syme, D.: An industrially effective environment for formal hardware verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 24(9), 1381\u20131405 (2005)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"3_CR51","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-1539-9_6","volume-title":"Design and Verification of Microprocessor Systems for High-Assurance Applications","author":"MM Wilding","year":"2010","unstructured":"Wilding, M.M., Greve, D.A., Richards, R.J., Hardin, D.S.: Formal verification of partition management for the AAMP7G microprocessor. In: Hardin, D. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications. Springer, Boston (2010). \n                      https:\/\/doi.org\/10.1007\/978-1-4419-1539-9_6"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96145-3_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T04:15:33Z","timestamp":1558325733000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96145-3_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319961446","9783319961453"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96145-3_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"18 July 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Oxford","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 July 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cavconference.org\/2018\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}