Show simple item record

Code-level model checking in the software development workflow at Amazon Web Services

dc.contributor.authorChong, N
dc.contributor.authorCook, B
dc.contributor.authorEidelman, J
dc.contributor.authorKallas, K
dc.contributor.authorKhazem, K
dc.contributor.authorMonteiro, FR
dc.contributor.authorSchwartz-Narbonne, D
dc.contributor.authorTasiran, S
dc.contributor.authorTautschnig, M
dc.contributor.authorTuttle, MR
dc.date.accessioned2021-03-25T11:30:04Z
dc.date.available2021-03-25T11:30:04Z
dc.date.issued2021-01-20
dc.identifier.citationChong, Nathan et al. "Code‐Level Model Checking In The Software Development Workflow At Amazon Web Services". Software: Practice And Experience, vol 51, no. 4, 2021, pp. 772-797. Wiley, doi:10.1002/spe.2949. Accessed 25 Mar 2021.en_US
dc.identifier.issn0038-0644
dc.identifier.urihttps://qmro.qmul.ac.uk/xmlui/handle/123456789/70863
dc.description.abstractThis article describes a style of applying symbolic model checking developed over the course of four years at Amazon Web Services (AWS). Lessons learned are drawn from proving properties of numerous C‐based systems, for example, custom hypervisors, encryption code, boot loaders, and an IoT operating system. Using our methodology, we find that we can prove the correctness of industrial low‐level C‐based systems with reasonable effort and predictability. Furthermore, AWS developers are increasingly writing their own formal specifications. As part of this effort, we have developed a CI system that allows integration of the proofs into standard development workflows and extended the proof tools to provide better feedback to users. All proofs discussed in this article are publicly available on GitHub.en_US
dc.publisherWileyen_US
dc.relation.ispartofSOFTWARE-PRACTICE & EXPERIENCE
dc.rightsThis is an open access article under the terms of the Creative Commons Attribution‐NonCommercial‐NoDerivs License, which permits use and distribution in any medium, provided the original work is properly cited, the use is non‐commercial and no modifications or adaptations are made.
dc.rightsAttribution-NonCommercial-NoDerivs 3.0 United States*
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/3.0/us/*
dc.subjectcontinuous integrationen_US
dc.subjectmodel checkingen_US
dc.subjectmemory safetyen_US
dc.titleCode-level model checking in the software development workflow at Amazon Web Servicesen_US
dc.typeArticleen_US
dc.rights.holder© 2021 The Authors. Software:Practice and Experience published by John Wiley & Sons, Ltd.
dc.identifier.doi10.1002/spe.2949
pubs.author-urlhttp://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&KeyUT=WOS:000609024500001&DestLinkType=FullRecord&DestApp=ALL_WOS&UsrCustomerID=612ae0d773dcbdba3046f6df545e9f6aen_US
pubs.notesNot knownen_US
pubs.publication-statusPublisheden_US
rioxxterms.funderDefault funderen_US
rioxxterms.identifier.projectDefault projecten_US


Files in this item

Thumbnail
Name:
license_rdf
Size:
811bytes
Format:
application/rdf+xml
View/Open
Thumbnail
Name:
Tautschnig Code‐level model 2021 ...
Size:
3.308Mb
Format:
application/
Description:
Published version
View/Open

This item appears in the following Collection(s)

Show simple item record

This is an open access article under the terms of the Creative Commons Attribution‐NonCommercial‐NoDerivs License, which permits use and distribution in any medium, provided the original work is properly cited, the use is non‐commercial and no modifications or adaptations are made.
Except where otherwise noted, this item's license is described as This is an open access article under the terms of the Creative Commons Attribution‐NonCommercial‐NoDerivs License, which permits use and distribution in any medium, provided the original work is properly cited, the use is non‐commercial and no modifications or adaptations are made.