Project Name


The slicing and dicing formal verification technique attempts to significantly reduce the state space that needs to be explored to find errors in concurrent programs. It uses information gathered from static analysis to guide program execution. New threads to be considered for execution are then added to the concrete execution system using an iterative refinement of the current under-approximation of the overall system. However, it currently does not handle the case where concurrent programs contain refinement locations reachable along more than one execution path from the start of the program. The aim of the project is to enhance it to verify more complex multithreaded programs such as these.


student: Saint Wesonga

mentor: Eric Mercer

co-mentor: Neha Rungta


Last modified 6 years ago Last modified on 02/16/2012 09:02:22 PM