Towards Agile Verification

Advances in software verification techniques have been impressive in the past decade. Formal verification of large production software is now increasingly feasible and this is paving the way to transferring these techniques from research to practice. We argue, however, that there is still a serious mismatch between verification and modern development processes, which highly focus on agility and incremental, iterative development. To address this issue, verification has to become agile, and seamless introduction into agile processes has to become feasible. We envision new approaches that will support verification-driven development in the same way as test-driven development is possible today, for example through JUnit within an IDE like Eclipse. In this paper we discuss how agile verification can be achieved, and we show some promising initial steps in this direction.