Code-level model checking in the software development workflow

作者：Nathan Chong, Byron Cook, Κωνσταντίνος Καλλάς, Kareem Khazem, Felipe R. Monteiro, Daniel Schwartz‐Narbonne, Serdar Taşiran, Michael Tautschnig, Mark R. Tuttle · 年份：2020 · DOI：10.1145/3377813.3381347 · 被引用次数：32 · 研究领域：Formal Methods in Verification、Software Testing and Debugging Techniques、Software Engineering Research

This experience report 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, e.g., 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. All proofs discussed in this paper are publicly available on GitHub.