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

Presented as part of the 2007 HCSS conference.

Abstract

Best program practices in software engineering emphasize the use of loosely coupled software components. This style of program construction facilitates easy swapping/replacement of component implementations, independent development by different parties, and realization of broader reuse strategies such as software product lines. While a component-oriented approach offers a number of benefits, it presents several quality assurance challenges including validating the correctness of individual components as well as their integration.

The "design-by-contract" paradigm is promising approach to component-based development that emphasizes "software contracts" to specify the behavior of components and to guide implementation, testing, and verification. By abstractly capturing crucial aspects of component behavior at component interface boundaries via contracts, design-by-contract establishes a framework for compositional reasoning of software. Although a variety of contract checking mechanisms have been considered for the design-by-contract paradigm, these approaches often have difficulty dealing with dynamically allocated data, specification and checking efforts are poorly leveraged by other quality assurance tools, and feedback provided to developers regarding the cause of detected faults is quite poor.

In this talk, we present Kiasan, a technique that synergistically combines a number of automated reasoning techniques including symbolic execution, model checking, theorem proving, and constraint solving to support design-by-contract reasoning of object-oriented programs written in languages such as Java and C#. Compared to existing approaches to Java contract verification, Kiasan can check much stronger behavioral properties of object-oriented software including properties/software that makes extensive use of heap-allocated data and provides stronger coverage guarantees. In addition, Kiasan naturally generates counter examples illustrating contract violations, visualization of code effects, and JUnit test cases that are driven by code and user-supplied specifications. Coverage/cost trade-offs are controlled by user-specified bounds on the length of heap-reference chains and number of loop iterations. Kiasan's unit test-case generation facilities compare very favorably with commercially available tools. The talk will include a demonstration of Kiasan and describe how it is implemented on top of the Bogor model checking framework. Furthermore, we present results from case studies in which Kiasan is applied to a variety of examples, and we discuss insights gained from our experience.