Slicing and dicing bugs in concurrent programs

A lack of scalable verification tools for concurrent programs has not allowed concurrent software development to keep abreast with hardware trends in multi-core technologies. The growing complexity of modern concurrent systems necessitates the use of abstractions in order to verify all the expected behaviors of the system. Current abstraction refinement techniques are restricted to verifying mostly sequential and simpler concurrent programs. In this work, we present a novel incremental underapproximation technique that uses program slicing. Based on a reachability property, an initial backward slice for a single thread is generated. The information in the program slice is coupled with a concrete execution to drive the lone thread; generating an underapproximation of the program behavior space. If the target location is reached in the underapproximation, then we have an actual concrete trace. Otherwise, the initial single-thread slice is refined to include another thread that affects the reachability of the target location. In this case, the concrete execution only considers the two threads in the slice and preemption points between the threads only occur at locations in the slice. This refinement process is repeated until the target location is reached or is shown to be unreachable. Initial results indicate that the incremental technique can potentially allow the discovery of errors in larger systems using fewer resources and produce a better reduction in systems that are correct.