Formal Methods and Verification

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.

Static analysis

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.

Faculty

Ganesh Gopalakrishnan
Mike Kirby
Matthew Might
John Regehr
Zvonimir Rakamaric