Improving Error Discovery of the Slicing and Dicing Technique

by Saint Wesonga for The Java Pathfinder Team

The slicing and dicing verification technique attempts to reduce the state space that needs to be explored to find errors in concurrent programs. New threads are added to the concrete execution using an iterative refinement of the current under-approximation. However, it does not currently handle the case where refinement locations are reachable along more than one path from the start of the program. This project aims to enhance it to verify complex multi-threaded programs such as these.