Bounded Model Checking for C programs in an enterprise environment
Michael Tautschnig
Research Scientist at Amazon Web Services and Lecturer in Theoretical Computer Science at Queen Mary, University of London
Software model checking tools promise to deliver genuine traces to errors, andsometimes even proofs of their absence. As static analysers, they do not requireconcrete execution of programs, which may be even more beneficial when targetingnew platforms. Academic research focusses on improving scalability, yet largelydisregards practical technical challenges to make tools cope with real-worldcode. At Amazon, both scalability requirements as well as real-world constraintsapply. Our prior work analysing more than 25,000 software packages in theDebian/GNU Linux distribution containing more than 400 million lines of C codenot only led to more than 700 public bug reports, but also provided a solidpreparation for the challenges at Amazon.