Formal Methods and Verification
Research on formal methods in the School of Computing is unique in its tight integration with systems research activities at Utah and elsewhere. All our activities including publications and software are listed at http://www.cs.utah.edu/fv. The principal faculty are Profs. Zvonimir Rakamaric and Gopalakrishnan specializing on concurrency and formal methods. In one research thrust, Profs. Gopalakrishnan and Kirby are collaborating to verify the correctness of communication structures in large-scale aggressively optimized parallel simulations written using the Message Passing Interface (MPI). In another research thrust, Prof. Gopalakrishnan’s group has created the first concolic verifier for GPU programs called GKLEE. Our formal analysis efforts have led to the release of dozens of open source software tools that are highlighted in the individual faculty webpages.