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 and http://matt.might.net/. The principal faculty are Profs. Zvonimir Rakamaric and Gopalakrishnan specializing on concurrency and formal methods, and Prof. Matt Might specializing on
program analysis and synthesis methods, including static analysis and applications to security and HPC. 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.
Prof. Might leads the U Combinator software systems research group. The U Combinator group focuses on improving the performance, parallelism, security and correctness of modern software systems through static analysis. Current emphases include analysis of functional languages such as Racket and platforms such as Android.