Kiasan: A Verification and Test-Case Generation Framework for Java Based on Symbolic Execution

摘要

Best program practices in software engineering emphasize software components that are loosely coupled and can be independently developed by different vendors. While these approaches improve the process of software development, however, they present a number of challenges involving reasoning about the correctness of individual components as well as their integration. Design-by-contract reasoning offers a promising approach to reason about software components by requiring software contracts that describe the behaviors of the components. This allows one to focus at satisfying the contract of each component, i.e., it allows compositional reasoning. In this paper, we present Kiasan, a technique that combines symbolic execution, model checking, theorem proving, and constraint solving to support design-by-contract reasoning of object-oriented software. There are a number of interesting tradeoffs between Kiasan other approaches such as ESC/Java. While checking in Kiasan is sometime more expensive, Kiasan can check much stronger behavioral properties of object-oriented software including properties/software that makes extensive use of heap-allocated data. In addition, Kiasan naturally generates counter examples, visualization of code effects, and JUnit test cases that are driven by code and user-supplied specifications. We present Kiasan and describe how it is implemented on top of the Bogor framework. Furthermore, we present a case study in which Kiasan is applied to a variety of examples and we discuss insights gained from our experience.