Verification of imperative programs.

Building correct, reliable and secure software systems in a timely fashion is a challenging task. The goal of this research project is to develop techniques to assist developers in completing this task successfully. In particular, this project focuses on improving and extending program verification, a form of static analysis where the absence of certain non-trivial programming errors such as data races and illegal memory accesses can be established by the compiler via mathematical proofs.

Keywords:Program verification, Static analysis, Separation logic

Disciplines:Applied mathematics in specific fields, Computer architecture and networks, Distributed computing, Information sciences, Information systems, Programming languages, Scientific computing, Theoretical computer science, Visual computing, Other information and computing sciences