Research on High-Confidence Software (HCS) intends to develop new cutting-edge technologies and tools that will dramatically improve the dependability of today's computer software. Successful research in HCS requires a deep knowledge and shared expertise of a large number of sub-disciplines in computer science, ranging from formal methods, programming languages, compilers, operating systems, proof assistants, software engineering, computer architecture, to embedded systems.
In October 2008, President Hou Jianguo of USTC and President Richard Levin of Yale University signed an official Memorandum of Understanding for establishing the USTC-Yale Joint Research Center for High-Confidence Software (HCS). The new Center combines the expertise of faculty members from both universities with the facilities and human resources of USTC. The long-term goal of the Center is to support a multidisciplinary research program in HCS in which independent research groups will work within a common facility, sharing resources and expertise. USTC and Yale will work together through the Center to facilitate direct collaborations between research groups in HCS based at each university. They will also enable the periodic exchange of students and researchers between research groups at the two institutions through the Center.
The Joint Research Center will pursue research in all areas of HCS and formal methods. Its current research topics include formal verification of system software, certifying compilers, concurrent and multi-core software, and automatic theorem proving systems, etc. The Center is interested in exploring new software development methods that combine formal program verification techniques with domain-specific languages and logics. The Center also intends to construct a practical infrastructure for building large-scale certified systems software that can be promoted in the industry. If successful, these research work will significantly advance the state-of-the-art in building dependable software systems.