An Introduction to Software Verification with Whiley

摘要

This tutorial introduces the basic ideas of software specification and verification, which are important techniques for assuring the quality of software and eliminating common kinds of errors such as buffer overflow. The tutorial takes a practical hands-on approach using the Whiley language and its verifying compiler. This verifying compiler uses an automated proof engine to try to prove that the code will execute without errors and will satisfy its specifications. Each section of the tutorial includes exercises that can be checked using the online Whiley Labs website.