Synopsis:

ECE 6750 will provide an introduction to the development of formally verified implementations of concurrent (multi-threaded) systems. The approach will follow Hoare's CSP (Communicating Sequential Processes), a notation for describing and reasoning about such systems. Students will learn to rigorously specify the behavior of interacting concurrent processes, to verify that behavior both by hand and with the use of automated tools, and to prove the absence of deadlock and livelock. The verified specifications will be implemented in Java, and in occam-pi, a language designed to support concurrency. The term will conclude with a significant application project.