Formalising C and C++ for Use in High Integrity Systems

摘要

UK MoD has long been an advocate of the use of mathematically formal verification in software for safety critical applications. In the past this has been focused on the SPARK Ada subset, but it is increasingly becoming difficult to find suppliers willing or capable of delivering Ada programs. Instead, there is a pressure to use more commercially attractive languages, such as C and C++. In order to maintain the high levels of confidence necessary for critical applications, this means being able to formally reason about these 'new' languages.This paper covers two related programmes that are developing formal semantics for restricted subsets of C and C++ respectively. It will also consider how the formal semantics will be exploited in a verification environment.