CONIX Publication

Writing software that will be secure and reliable is notoriously difficult, especially when the code must also achieve high performance. Software verification can prove code correct or even secure, but historically, many verified systems have compromised on performance. In recent years, however, we have made steady progress developing systems that are as fast or faster than state-of-the-art unverified systems but that come with mechanically-verified guarantees of correctness and security. Hence, users no longer need to choose between performance and strong guarantees. Indeed, recently we have begun to see verification not as an impediment, but rather as an enabler of best-in-class performance.