Program Analysis and Formal Methods The School of Computing at the University of Utah has research efforts in algorithms, formal methods and verification.

Research

Algorithms

Algorithms research at the School of Computing explores problems in numerous areas, including topics in massive data sets, data mining, computational geometry, shape analysis and data visualization. One strand of current research being developed by Prof. Venkatasubramanian deals with the computational challenges of doing statistics on large data sets, and how information- theoretic methods can be brought to bear on a variety of problems in data management, with application in general data cleaning scenarios, as well as bioinformatics. Another research effort involves understanding algorithms in non-Euclidean spaces: a particular application of this effort is in the analysis of shape, particularly the shapes extracting from medical imaging modalities like MRI scanning and diffusion tensor imaging. Prof. Venkatasubramanian, together with Profs. Fletcher (CS) and Joshi (Bioengineering), is developing scalable, accurate algorithms for data analysis in non-Euclidean domains.

Verification

Research on formal methods in the School of Computing is unique in its tight integration with systems research activities at Utah and elsewhere. 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). Another effort led by Prof. Gopalakrishnan is aimed at improving the reliability of hardware cache coherence protocols through formal verification.

Faculty